set(auto).set(build_proof_object_2).clear(sigint_interact).assign(max_seconds, 10).initial_proof_object(junk).
((1 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (NOT (S V2 (SK1 V2 V3))) (NOT (Q V3 (SK1 V2 V3))))))
 (2 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (NOT (S V2 (SK1 V2 V3))) (Q (SK1 V2 V3) V6))))
 (3 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (NOT (S V2 (SK1 V2 V3))) (NOT (S V3 V3)))))
 (4 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (S (SK1 V2 V3) V5) (NOT (Q V3 (SK1 V2 V3))))))
 (5 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (S (SK1 V2 V3) V5) (Q (SK1 V2 V3) V6))))
 (6 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (S (SK1 V2 V3) V5) (NOT (S V3 V3)))))
 (7 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (NOT (Q V6 V6)) (NOT (Q V3 (SK1 V2 V3))))))
 (8 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3))
      (OR (NOT (Q V6 V6)) (Q (SK1 V2 V3) V6))))
 (9 (INPUT)
  (OR (P (SK1 V2 V3) (SK1 V2 V3)) (OR (NOT (Q V6 V6)) (NOT (S V3 V3)))))
 (10 (INPUT)
  (OR (NOT (P V2 V2))
      (OR (NOT (S V2 (SK1 V2 V3))) (NOT (Q V3 (SK1 V2 V3))))))
 (11 (INPUT)
  (OR (NOT (P V2 V2)) (OR (NOT (S V2 (SK1 V2 V3))) (Q (SK1 V2 V3) V6))))
 (12 (INPUT)
  (OR (NOT (P V2 V2)) (OR (NOT (S V2 (SK1 V2 V3))) (NOT (S V3 V3)))))
 (13 (INPUT)
  (OR (NOT (P V2 V2)) (OR (S (SK1 V2 V3) V5) (NOT (Q V3 (SK1 V2 V3))))))
 (14 (INPUT)
  (OR (NOT (P V2 V2)) (OR (S (SK1 V2 V3) V5) (Q (SK1 V2 V3) V6))))
 (15 (INPUT)
  (OR (NOT (P V2 V2)) (OR (S (SK1 V2 V3) V5) (NOT (S V3 V3)))))
 (16 (INPUT)
  (OR (NOT (P V2 V2)) (OR (NOT (Q V6 V6)) (NOT (Q V3 (SK1 V2 V3))))))
 (17 (INPUT)
  (OR (NOT (P V2 V2)) (OR (NOT (Q V6 V6)) (Q (SK1 V2 V3) V6))))
 (18 (INPUT) (OR (NOT (P V2 V2)) (OR (NOT (Q V6 V6)) (NOT (S V3 V3)))))
 (19 (INPUT)
  (OR (S V5 V2) (OR (NOT (S V2 (SK1 V2 V3))) (NOT (Q V3 (SK1 V2 V3))))))
 (20 (INPUT)
  (OR (S V5 V2) (OR (NOT (S V2 (SK1 V2 V3))) (Q (SK1 V2 V3) V6))))
 (21 (INPUT)
  (OR (S V5 V2) (OR (NOT (S V2 (SK1 V2 V3))) (NOT (S V3 V3)))))
 (22 (INPUT)
  (OR (S V5 V2) (OR (S (SK1 V2 V3) V5) (NOT (Q V3 (SK1 V2 V3))))))
 (23 (INPUT) (OR (S V5 V2) (OR (S (SK1 V2 V3) V5) (Q (SK1 V2 V3) V6))))
 (24 (INPUT) (OR (S V5 V2) (OR (S (SK1 V2 V3) V5) (NOT (S V3 V3)))))
 (25 (INPUT)
  (OR (S V5 V2) (OR (NOT (Q V6 V6)) (NOT (Q V3 (SK1 V2 V3))))))
 (26 (INPUT) (OR (S V5 V2) (OR (NOT (Q V6 V6)) (Q (SK1 V2 V3) V6))))
 (27 (INPUT) (OR (S V5 V2) (OR (NOT (Q V6 V6)) (NOT (S V3 V3))))))