%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:39:19 PM UTC 2026
% Result : Unsatisfiable 0.69s 1.06s
% Output : CNFRefutation 2.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 60
% Syntax : Number of formulae : 217 ( 44 unt; 0 def)
% Number of atoms : 542 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 659 ( 334 ~; 325 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 48 ( 47 usr; 16 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 242 ( 0 sgn 242 !; 0 ?; 152 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_1) ).
fof(f2,axiom,
q0(e,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_2) ).
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_5) ).
fof(f6,axiom,
q0(b,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_6) ).
fof(f7,axiom,
n0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_7) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
fof(f13,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_13) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_18) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_27) ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
fof(f29,axiom,
q0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_29) ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
fof(f32,axiom,
k0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_32) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
fof(f37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
fof(f39,axiom,
! [X0,X1] :
( ~ n0(X1,X0)
| k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_001) ).
fof(f40,axiom,
! [X0,X1] :
( ~ n0(X1,X0)
| l1(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_002) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( ~ m0(X1,X0,X2)
| ~ r0(X3)
| ~ p0(X2,X0)
| l1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_003) ).
fof(f59,axiom,
! [X0,X1] :
( ~ k0(X1)
| ~ l0(X0)
| m1(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_021) ).
fof(f88,axiom,
! [X0,X1] :
( ~ p0(b,X1)
| ~ l0(X0)
| ~ s0(b)
| n1(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_050) ).
fof(f92,axiom,
! [X2,X0,X1] :
( ~ n1(X0,X1,X0)
| ~ l1(X2,X0)
| ~ l0(X2)
| n1(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_054) ).
fof(f106,axiom,
! [X0] :
( ~ k0(X0)
| p1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_068) ).
fof(f126,axiom,
( ~ l0(a)
| p1(a,a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_088) ).
fof(f128,axiom,
( ~ k0(e)
| ~ r0(e)
| p1(e,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_090) ).
fof(f138,axiom,
! [X0,X1] :
( ~ n0(X1,X0)
| q1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_100) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ m1(X0,X1,X1)
| ~ r0(X2)
| q1(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_113) ).
fof(f155,axiom,
( ~ s0(d)
| ~ k0(e)
| q1(d,d,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_117) ).
fof(f162,axiom,
! [X0,X1] :
( ~ q1(d,X1,d)
| ~ s0(d)
| ~ q0(X0,X1)
| r1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_124) ).
fof(f163,axiom,
! [X0] :
( ~ p0(X0,X0)
| s1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_125) ).
fof(f164,axiom,
! [X2,X0,X1] :
( ~ s1(X2)
| ~ q0(X0,X1)
| s1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_126) ).
fof(f171,axiom,
! [X2,X3,X0,X1] :
( ~ m0(X3,X2,X0)
| ~ s1(X2)
| ~ p0(X1,X1)
| l2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_133) ).
fof(f175,axiom,
! [X2,X0,X1] :
( ~ p1(X1,X2,X0)
| n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_137) ).
fof(f183,axiom,
! [X0,X1] :
( ~ p1(X0,X1,e)
| ~ r0(e)
| p2(e,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_145) ).
fof(f193,axiom,
! [X2,X0,X1] :
( ~ p2(e,X0,X1)
| ~ k1(X2)
| p2(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_155) ).
fof(f214,axiom,
! [X0,X1] :
( ~ m1(X1,X0,X1)
| p2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_176) ).
fof(f215,axiom,
! [X0,X1] :
( ~ p1(X0,X0,X0)
| ~ k0(X1)
| q2(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_177) ).
fof(f219,axiom,
! [X0] :
( ~ p1(X0,X0,X0)
| q2(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_181) ).
fof(f220,axiom,
! [X2,X0,X1] :
( ~ q2(X1,X2,X0)
| ~ n1(X1,X0,X2)
| ~ p1(X0,X0,X2)
| q2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_182) ).
fof(f224,axiom,
! [X0,X1] :
( ~ l1(X1,X0)
| q2(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_186) ).
fof(f226,axiom,
! [X0] :
( ~ l0(X0)
| ~ r1(X0)
| r2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_188) ).
fof(f227,axiom,
! [X0] :
( ~ s1(b)
| ~ q2(b,X0,b)
| s2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_189) ).
fof(f248,axiom,
! [X0] :
( ~ n2(X0)
| k3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_210) ).
fof(f265,axiom,
! [X2,X3,X0,X1] :
( ~ r2(X0)
| ~ s2(X2)
| ~ s0(X3)
| ~ q0(X1,X2)
| m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_227) ).
fof(f274,axiom,
! [X0] :
( ~ n2(X0)
| m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_236) ).
fof(f278,axiom,
! [X2,X0,X1] :
( ~ p2(X1,X2,X0)
| n3(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_240) ).
fof(f293,axiom,
! [X2,X0,X1] :
( ~ n0(X2,X0)
| ~ q2(X2,X0,X1)
| q3(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_255) ).
fof(f296,axiom,
! [X2,X0,X1] :
( ~ l2(X2,X2)
| ~ s1(X1)
| ~ r2(X0)
| q3(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_258) ).
fof(f305,axiom,
! [X2,X0,X1] :
( ~ p2(X0,X2,X1)
| r3(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_267) ).
fof(f312,axiom,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_274) ).
fof(f314,axiom,
! [X0,X1] :
( ~ r3(X0,e,X1)
| ~ q1(a,a,X1)
| ~ q3(X0,X0)
| k4(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_276) ).
fof(f322,axiom,
! [X0,X1] :
( ~ m3(X0,X0,X0)
| ~ k4(X1)
| n4(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_284) ).
fof(f323,axiom,
! [X0,X1] :
( ~ r3(X1,X0,X1)
| ~ r0(X0)
| p4(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_285) ).
fof(f333,axiom,
! [X2,X3,X0,X1,X4] :
( ~ m3(X3,X4,X3)
| ~ q2(X3,X1,X0)
| ~ k3(X2,X2,X0)
| q4(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_295) ).
fof(f345,axiom,
! [X2,X3,X0,X1,X4] :
( ~ n5(X4,X1)
| ~ p4(X4,X4,X1)
| ~ n4(X0,X3)
| ~ q4(X2,X3)
| n5(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_307) ).
fof(f353,axiom,
! [X0] :
( ~ k4(X0)
| ~ s1(X0)
| n5(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_315) ).
fof(f369,negated_conjecture,
~ n5(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
tcf(c_418,negated_conjecture,
~ n5(a,e),
inference(cnf_transformation,[],[f369]) ).
tcf(c_428,plain,
m0(e,b,c),
inference(cnf_transformation,[],[f27]) ).
tcf(c_447,plain,
! [X0: $i] :
( n5(X0,X0)
| ~ k4(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( n5(X2,X1)
| ~ q4(X4,X3)
| ~ n4(X2,X3)
| ~ n5(X0,X1)
| ~ p4(X0,X0,X1) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_455,plain,
! [X0: $i,X1: $i] :
( p2(e,X0,X1)
| ~ r0(e)
| ~ p1(X0,X1,e) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i] :
( p2(X1,X0,X1)
| ~ m1(X0,X1,X0) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_485,plain,
p0(c,b),
inference(cnf_transformation,[],[f18]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i,X2: $i] :
( q1(X0,X0,X1)
| ~ r0(X2)
| ~ m1(X0,X1,X1) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i] : m0(X0,d,X1),
inference(cnf_transformation,[],[f19]) ).
tcf(c_515,plain,
( p1(e,e,e)
| ~ k0(e)
| ~ r0(e) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_524,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( l1(X1,X0)
| ~ r0(X3)
| ~ p0(X2,X1)
| ~ m0(X0,X1,X2) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_525,plain,
r0(e),
inference(cnf_transformation,[],[f13]) ).
tcf(c_526,plain,
r0(b),
inference(cnf_transformation,[],[f9]) ).
tcf(c_531,plain,
! [X0: $i,X1: $i] :
( n1(X1,X0,X1)
| ~ s0(b)
| ~ l0(X1)
| ~ p0(b,X0) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_536,plain,
! [X0: $i] : p0(b,X0),
inference(cnf_transformation,[],[f14]) ).
tcf(c_548,plain,
q0(d,b),
inference(cnf_transformation,[],[f29]) ).
tcf(c_551,plain,
! [X0: $i] : q0(X0,d),
inference(cnf_transformation,[],[f17]) ).
tcf(c_552,plain,
q0(b,b),
inference(cnf_transformation,[],[f6]) ).
tcf(c_553,plain,
q0(e,d),
inference(cnf_transformation,[],[f2]) ).
tcf(c_559,plain,
! [X0: $i,X1: $i] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_569,plain,
! [X0: $i] :
( s2(X0)
| ~ s1(b)
| ~ q2(b,X0,b) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( l2(X2,X2)
| ~ s1(X1)
| ~ p0(X3,X3)
| ~ m0(X0,X1,X2) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_575,plain,
! [X0: $i,X1: $i,X2: $i] :
( s1(X0)
| ~ s1(X2)
| ~ q0(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_576,plain,
! [X0: $i] :
( s1(X0)
| ~ p0(X0,X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_581,plain,
! [X0: $i,X1: $i] :
( p4(X1,X1,X0)
| ~ r0(X1)
| ~ r3(X0,X1,X0) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_582,plain,
! [X0: $i,X1: $i] :
( k4(e)
| ~ q3(X0,X0)
| ~ q1(a,a,X1)
| ~ r3(X0,e,X1) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_583,plain,
( k4(c)
| ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_586,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( q4(X2,X1)
| ~ m3(X0,X4,X0)
| ~ k3(X3,X3,X2)
| ~ q2(X0,X1,X2) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_592,plain,
! [X0: $i,X1: $i,X2: $i] :
( r3(X0,X2,X0)
| ~ p2(X0,X1,X2) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_601,plain,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_609,plain,
s0(b),
inference(cnf_transformation,[],[f5]) ).
tcf(c_610,plain,
s0(d),
inference(cnf_transformation,[],[f1]) ).
tcf(c_615,plain,
( p1(a,a,a)
| ~ l0(a) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_620,plain,
! [X0: $i,X1: $i,X2: $i] :
( n1(X0,X1,X1)
| ~ l0(X2)
| ~ l1(X2,X0)
| ~ n1(X0,X1,X0) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_623,plain,
! [X0: $i,X1: $i] :
( m1(X0,X1,X0)
| ~ k0(X1)
| ~ l0(X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_629,plain,
l0(a),
inference(cnf_transformation,[],[f20]) ).
tcf(c_630,plain,
! [X0: $i,X1: $i] :
( q2(X0,X1,X1)
| ~ k0(X1)
| ~ p1(X0,X0,X0) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_635,plain,
! [X0: $i] :
( p1(X0,X0,X0)
| ~ k0(X0) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_639,plain,
k0(b),
inference(cnf_transformation,[],[f32]) ).
tcf(c_640,plain,
k0(e),
inference(cnf_transformation,[],[f28]) ).
tcf(c_642,plain,
! [X0: $i,X1: $i] :
( q1(X1,X1,X1)
| ~ n0(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_645,plain,
! [X0: $i,X1: $i] :
( l1(X1,X1)
| ~ n0(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_646,plain,
! [X0: $i,X1: $i] :
( k1(X1)
| ~ n0(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_647,plain,
n0(b,a),
inference(cnf_transformation,[],[f37]) ).
tcf(c_648,plain,
n0(c,d),
inference(cnf_transformation,[],[f34]) ).
tcf(c_649,plain,
n0(e,e),
inference(cnf_transformation,[],[f30]) ).
tcf(c_653,plain,
n0(d,b),
inference(cnf_transformation,[],[f7]) ).
tcf(c_655,plain,
! [X0: $i,X1: $i] :
( q2(X1,X1,X0)
| ~ l1(X0,X1) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_665,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X0,X1,X1)
| ~ k1(X2)
| ~ p2(e,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_671,plain,
! [X0: $i,X1: $i,X2: $i] :
( q2(X1,X0,X1)
| ~ q2(X0,X2,X1)
| ~ p1(X1,X1,X2)
| ~ n1(X0,X1,X2) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_672,plain,
! [X0: $i] :
( q2(X0,X0,X0)
| ~ p1(X0,X0,X0) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_692,plain,
! [X0: $i,X1: $i,X2: $i] :
( q3(X2,X2)
| ~ r2(X2)
| ~ s1(X1)
| ~ l2(X0,X0) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_695,plain,
! [X0: $i,X1: $i,X2: $i] :
( q3(X1,X2)
| ~ n0(X0,X1)
| ~ q2(X0,X1,X2) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_698,plain,
! [X0: $i] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_709,plain,
! [X0: $i] :
( k3(X0,X0,X0)
| ~ n2(X0) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i,X2: $i] :
( n2(X2)
| ~ p1(X0,X1,X2) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_716,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m3(X3,X3,X3)
| ~ s2(X1)
| ~ r2(X3)
| ~ s0(X2)
| ~ q0(X0,X1) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_721,plain,
! [X0: $i] :
( r2(X0)
| ~ r1(X0)
| ~ l0(X0) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_728,plain,
! [X0: $i,X1: $i] :
( r1(X1)
| ~ s0(d)
| ~ q0(X1,X0)
| ~ q1(d,X0,d) ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_732,plain,
! [X0: $i,X1: $i,X2: $i] :
( n3(X2)
| ~ p2(X0,X1,X2) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_758,plain,
p0(b,b),
inference(instantiation,[status(thm)],[c_536]) ).
tcf(c_759,plain,
m0(b,d,b),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_764,plain,
( s1(b)
| ~ p0(b,b) ),
inference(instantiation,[status(thm)],[c_576]) ).
tcf(c_768,plain,
( n2(b)
| ~ p1(b,b,b) ),
inference(instantiation,[status(thm)],[c_714]) ).
tcf(c_769,plain,
( k3(b,b,b)
| ~ n2(b) ),
inference(instantiation,[status(thm)],[c_709]) ).
tcf(c_771,plain,
( m3(b,b,b)
| ~ n2(b) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_774,plain,
( p1(b,b,b)
| ~ k0(b) ),
inference(instantiation,[status(thm)],[c_635]) ).
tcf(c_801,plain,
( q2(b,b,b)
| ~ p1(b,b,b) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_823,plain,
( s2(b)
| ~ s1(b)
| ~ q2(b,b,b) ),
inference(instantiation,[status(thm)],[c_569]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i] :
( p2(e,X0,X1)
| ~ p1(X0,X1,e) ),
inference(global_subsumption_just,[status(thm)],[c_455,c_525,c_455]) ).
tcf(c_995,plain,
( k4(c)
| ~ n3(e)
| ~ q3(e,b) ),
inference(global_subsumption_just,[status(thm)],[c_583,c_648,c_583]) ).
tcf(c_999,plain,
! [X0: $i,X1: $i] :
( r1(X1)
| ~ q1(d,X0,d)
| ~ q0(X1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_728,c_610,c_728]) ).
tcf(c_1000,plain,
! [X0: $i,X1: $i] :
( r1(X1)
| ~ q0(X1,X0)
| ~ q1(d,X0,d) ),
inference(renaming,[status(thm)],[c_999]) ).
tcf(c_1007,plain,
! [X0: $i,X1: $i] :
( n1(X1,X0,X1)
| ~ l0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_531,c_609,c_536,c_531]) ).
tcf(c_1008,plain,
! [X0: $i,X1: $i] :
( n1(X0,X1,X0)
| ~ l0(X0) ),
inference(renaming,[status(thm)],[c_1007]) ).
tcf(c_1064,plain,
! [X0: $i] :
( ~ iPr_def_28
| ~ r2(X0)
| m3(X0,X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_716]) ).
tcf(c_1065,plain,
! [X0: $i] :
( ~ iPr_def_29
| ~ s0(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_716]) ).
tcf(c_1066,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_30
| ~ s2(X1)
| ~ q0(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_716]) ).
tcf(c_1067,plain,
( iPr_def_30
| iPr_def_29
| iPr_def_28 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_716]) ).
tcf(c_1073,plain,
! [X0: $i] :
( ~ iPr_def_34
| ~ s1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_692]) ).
tcf(c_1074,plain,
! [X0: $i] :
( ~ iPr_def_35
| ~ r2(X0)
| q3(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_692]) ).
tcf(c_1075,plain,
! [X0: $i] :
( ~ iPr_def_36
| ~ l2(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_692]) ).
tcf(c_1076,plain,
( iPr_def_36
| iPr_def_35
| iPr_def_34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_692]) ).
tcf(c_1087,plain,
! [X0: $i] :
( ~ iPr_def_43
| ~ k1(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_43])],[c_665]) ).
tcf(c_1088,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_44
| ~ p2(e,X0,X1)
| p2(X0,X1,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_44])],[c_665]) ).
tcf(c_1089,plain,
( iPr_def_44
| iPr_def_43 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_665]) ).
tcf(c_1110,plain,
! [X0: $i] :
( ~ iPr_def_58
| ~ k4(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_58])],[c_559]) ).
tcf(c_1111,plain,
! [X0: $i] :
( ~ iPr_def_59
| n4(X0,X0)
| ~ m3(X0,X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_59])],[c_559]) ).
tcf(c_1112,plain,
( iPr_def_59
| iPr_def_58 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_559]) ).
tcf(c_1136,plain,
! [X0: $i] :
( ~ iPr_def_75
| ~ p0(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_75])],[c_573]) ).
tcf(c_1137,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_76
| ~ s1(X1)
| l2(X2,X2)
| ~ m0(X0,X1,X2) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_76])],[c_573]) ).
tcf(c_1138,plain,
( iPr_def_76
| iPr_def_75 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_573]) ).
tcf(c_1139,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_77
| s1(X0)
| ~ q0(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_77])],[c_575]) ).
tcf(c_1140,plain,
( iPr_def_77
| iPr_def_34 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_575]) ).
tcf(c_1141,plain,
! [X0: $i] :
( ~ iPr_def_78
| ~ r0(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_78])],[c_492]) ).
tcf(c_1182,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_103
| ~ p0(X2,X1)
| l1(X1,X0)
| ~ m0(X0,X1,X2) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_103])],[c_524]) ).
tcf(c_1183,plain,
( iPr_def_103
| iPr_def_78 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_524]) ).
tcf(c_1186,plain,
( ~ iPr_def_29
| ~ s0(b) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1187,plain,
( ~ iPr_def_34
| ~ s1(b) ),
inference(instantiation,[status(thm)],[c_1073]) ).
tcf(c_1190,plain,
( ~ iPr_def_43
| ~ k1(b) ),
inference(instantiation,[status(thm)],[c_1087]) ).
tcf(c_1192,plain,
( ~ iPr_def_78
| ~ r0(b) ),
inference(instantiation,[status(thm)],[c_1141]) ).
tcf(c_1196,plain,
( ~ iPr_def_36
| ~ l2(b,b) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1200,plain,
( ~ iPr_def_75
| ~ p0(b,b) ),
inference(instantiation,[status(thm)],[c_1136]) ).
tcf(c_1220,plain,
( ~ iPr_def_30
| ~ s2(b)
| ~ q0(b,b) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1261,plain,
( p2(e,e,e)
| ~ p1(e,e,e) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1278,plain,
( k1(b)
| ~ n0(d,b) ),
inference(instantiation,[status(thm)],[c_646]) ).
tcf(c_1308,plain,
! [X0: $i] :
( s1(d)
| ~ iPr_def_77
| ~ q0(d,X0) ),
inference(instantiation,[status(thm)],[c_1139]) ).
tcf(c_1309,plain,
( s1(d)
| ~ iPr_def_77
| ~ q0(d,b) ),
inference(instantiation,[status(thm)],[c_1308]) ).
tcf(c_1332,plain,
( l1(a,a)
| ~ n0(b,a) ),
inference(instantiation,[status(thm)],[c_645]) ).
tcf(c_1342,plain,
! [X0: $i] :
( r1(X0)
| ~ q0(X0,d)
| ~ q1(d,d,d) ),
inference(instantiation,[status(thm)],[c_1000]) ).
tcf(c_1344,plain,
! [X0: $i] :
( n1(a,X0,a)
| ~ l0(a) ),
inference(instantiation,[status(thm)],[c_1008]) ).
tcf(c_1345,plain,
( n1(a,b,a)
| ~ l0(a) ),
inference(instantiation,[status(thm)],[c_1344]) ).
tcf(c_1415,plain,
! [X0: $i] :
( m1(a,X0,a)
| ~ l0(a)
| ~ k0(X0) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1433,plain,
( q1(a,a,a)
| ~ n0(b,a) ),
inference(instantiation,[status(thm)],[c_642]) ).
tcf(c_1457,plain,
! [X0: $i] :
( p2(e,X0,e)
| ~ m1(X0,e,X0) ),
inference(instantiation,[status(thm)],[c_463]) ).
tcf(c_1515,plain,
! [X0: $i,X1: $i] :
( r3(X0,e,X0)
| ~ p2(X0,X1,e) ),
inference(instantiation,[status(thm)],[c_592]) ).
tcf(c_1532,plain,
! [X0: $i,X1: $i] :
( l2(X1,X1)
| ~ iPr_def_76
| ~ s1(d)
| ~ m0(X0,d,X1) ),
inference(instantiation,[status(thm)],[c_1137]) ).
tcf(c_1533,plain,
( l2(b,b)
| ~ iPr_def_76
| ~ s1(d)
| ~ m0(b,d,b) ),
inference(instantiation,[status(thm)],[c_1532]) ).
tcf(c_1594,plain,
! [X0: $i] :
( q3(e,X0)
| ~ n0(e,e)
| ~ q2(e,e,X0) ),
inference(instantiation,[status(thm)],[c_695]) ).
tcf(c_1595,plain,
( q3(e,b)
| ~ n0(e,e)
| ~ q2(e,e,b) ),
inference(instantiation,[status(thm)],[c_1594]) ).
tcf(c_1608,plain,
( l1(b,e)
| ~ iPr_def_103
| ~ p0(c,b)
| ~ m0(e,b,c) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_1791,plain,
( q2(e,e,b)
| ~ l1(b,e) ),
inference(instantiation,[status(thm)],[c_655]) ).
tcf(c_1811,plain,
( q2(a,b,b)
| ~ k0(b)
| ~ p1(a,a,a) ),
inference(instantiation,[status(thm)],[c_630]) ).
tcf(c_1824,plain,
! [X0: $i] :
( q2(b,a,b)
| ~ q2(a,X0,b)
| ~ p1(b,b,X0)
| ~ n1(a,b,X0) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_1825,plain,
( q2(b,a,b)
| ~ q2(a,b,b)
| ~ p1(b,b,b)
| ~ n1(a,b,b) ),
inference(instantiation,[status(thm)],[c_1824]) ).
tcf(c_1846,plain,
( p2(e,a,e)
| ~ m1(a,e,a) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_1847,plain,
( m1(a,e,a)
| ~ k0(e)
| ~ l0(a) ),
inference(instantiation,[status(thm)],[c_1415]) ).
tcf(c_1883,plain,
! [X0: $i] :
( s1(e)
| ~ iPr_def_77
| ~ q0(e,X0) ),
inference(instantiation,[status(thm)],[c_1139]) ).
tcf(c_1886,plain,
( r3(e,e,e)
| ~ p2(e,a,e) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_1996,plain,
! [X0: $i] :
( p2(X0,e,e)
| ~ iPr_def_44
| ~ p2(e,X0,e) ),
inference(instantiation,[status(thm)],[c_1088]) ).
tcf(c_2118,plain,
( r2(a)
| ~ r1(a)
| ~ l0(a) ),
inference(instantiation,[status(thm)],[c_721]) ).
tcf(c_2343,plain,
! [X0: $i,X1: $i] :
( n1(X0,X1,X1)
| ~ l0(a)
| ~ l1(a,X0)
| ~ n1(X0,X1,X0) ),
inference(instantiation,[status(thm)],[c_620]) ).
tcf(c_2359,plain,
! [X0: $i] :
( r3(X0,e,X0)
| ~ p2(X0,e,e) ),
inference(instantiation,[status(thm)],[c_1515]) ).
tcf(c_2394,plain,
( r1(a)
| ~ q0(a,d)
| ~ q1(d,d,d) ),
inference(instantiation,[status(thm)],[c_1342]) ).
tcf(c_2414,plain,
! [X0: $i,X1: $i] :
( n3(e)
| ~ p2(X0,X1,e) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_2441,plain,
q0(a,d),
inference(instantiation,[status(thm)],[c_551]) ).
tcf(c_2471,plain,
( s1(e)
| ~ iPr_def_77
| ~ q0(e,d) ),
inference(instantiation,[status(thm)],[c_1883]) ).
tcf(c_2493,plain,
! [X0: $i] :
( k4(e)
| ~ q3(X0,X0)
| ~ q1(a,a,a)
| ~ r3(X0,e,a) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_2519,plain,
( q3(a,a)
| ~ iPr_def_35
| ~ r2(a) ),
inference(instantiation,[status(thm)],[c_1074]) ).
tcf(c_2523,plain,
( m3(a,a,a)
| ~ iPr_def_28
| ~ r2(a) ),
inference(instantiation,[status(thm)],[c_1064]) ).
tcf(c_2745,plain,
! [X0: $i] :
( n1(a,X0,X0)
| ~ l0(a)
| ~ l1(a,a)
| ~ n1(a,X0,a) ),
inference(instantiation,[status(thm)],[c_2343]) ).
tcf(c_2747,plain,
( n1(a,b,b)
| ~ l0(a)
| ~ l1(a,a)
| ~ n1(a,b,a) ),
inference(instantiation,[status(thm)],[c_2745]) ).
tcf(c_3033,plain,
( n3(e)
| ~ p2(e,e,e) ),
inference(instantiation,[status(thm)],[c_2414]) ).
tcf(c_3355,plain,
( k4(e)
| ~ q3(a,a)
| ~ r3(a,e,a)
| ~ q1(a,a,a) ),
inference(instantiation,[status(thm)],[c_2493]) ).
tcf(c_3356,plain,
( r3(a,e,a)
| ~ p2(a,e,e) ),
inference(instantiation,[status(thm)],[c_2359]) ).
tcf(c_3788,plain,
( ~ iPr_def_58
| ~ k4(c) ),
inference(instantiation,[status(thm)],[c_1110]) ).
tcf(c_3873,plain,
( p2(a,e,e)
| ~ iPr_def_44
| ~ p2(e,a,e) ),
inference(instantiation,[status(thm)],[c_1996]) ).
tcf(c_4149,plain,
! [X0: $i,X1: $i,X2: $i] :
( n5(a,e)
| ~ n4(a,X2)
| ~ n5(X0,e)
| ~ q4(X1,X2)
| ~ p4(X0,X0,e) ),
inference(instantiation,[status(thm)],[c_453]) ).
tcf(c_4363,plain,
! [X0: $i,X1: $i] :
( n5(a,e)
| ~ n5(e,e)
| ~ n4(a,X1)
| ~ q4(X0,X1)
| ~ p4(e,e,e) ),
inference(instantiation,[status(thm)],[c_4149]) ).
tcf(c_4400,plain,
( n5(e,e)
| ~ k4(e)
| ~ s1(e) ),
inference(instantiation,[status(thm)],[c_447]) ).
tcf(c_4712,plain,
( p4(e,e,e)
| ~ r0(e)
| ~ r3(e,e,e) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_4723,plain,
! [X0: $i] :
( n5(a,e)
| ~ n4(a,a)
| ~ n5(e,e)
| ~ q4(X0,a)
| ~ p4(e,e,e) ),
inference(instantiation,[status(thm)],[c_4363]) ).
tcf(c_4724,plain,
( n4(a,a)
| ~ iPr_def_59
| ~ m3(a,a,a) ),
inference(instantiation,[status(thm)],[c_1111]) ).
tcf(c_4725,plain,
( n5(a,e)
| ~ q4(b,a)
| ~ n4(a,a)
| ~ n5(e,e)
| ~ p4(e,e,e) ),
inference(instantiation,[status(thm)],[c_4723]) ).
tcf(c_4922,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( q4(X1,a)
| ~ q2(X2,a,X1)
| ~ m3(X2,X3,X2)
| ~ k3(X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_586]) ).
tcf(c_4923,plain,
( q4(b,a)
| ~ m3(b,b,b)
| ~ k3(b,b,b)
| ~ q2(b,a,b) ),
inference(instantiation,[status(thm)],[c_4922]) ).
tcf(c_4924,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4923,c_4724,c_4725,c_4712,c_4400,c_3873,c_3788,c_3356,c_3355,c_3033,c_2747,c_2519,c_2523,c_2471,c_2441,c_2394,c_2118,c_1886,c_1847,c_1846,c_1825,c_1811,c_1791,c_1608,c_1595,c_1533,c_1433,c_1345,c_1332,c_1309,c_1278,c_1261,c_1220,c_1200,c_1196,c_1192,c_1190,c_1187,c_1186,c_1076,c_1067,c_1183,c_1140,c_1138,c_1112,c_1089,c_995,c_515,c_823,c_601,c_801,c_615,c_774,c_771,c_769,c_768,c_764,c_428,c_759,c_418,c_485,c_758,c_548,c_552,c_553,c_647,c_649,c_653,c_525,c_526,c_609,c_610,c_629,c_639,c_640]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.38 % Computer : n008.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 00:21:42 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running EPR theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 0.69/1.06 % SZS status Started for theBenchmark.p
% 0.69/1.06 % SZS status Unsatisfiable for theBenchmark.p
% 0.69/1.06
% 0.69/1.06 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.69/1.06
% 0.69/1.06 % ------ iProver source info
% 0.69/1.06
% 0.69/1.06 % git: date: 2026-07-19 20:42:38 +0200
% 0.69/1.06 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.69/1.06 % git: non_committed_changes: false
% 0.69/1.06
% 0.69/1.06 % ------ Parsing...% successful
% 0.69/1.06
% 0.69/1.06
% 0.69/1.06 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_horn
% 0.69/1.06 %
% 0.69/1.06
% 0.69/1.06 % ------ Preprocessing... sf_s rm: 14 0s sf_e sf_s rm: 0 0s sf_e %
% 0.69/1.06
% 0.69/1.06 % ------ Preprocessing...% ------ preprocesses with Option_epr_horn
% 0.69/1.06 gs_s sp: 108 0s gs_e snvd_s sp: 0 0s snvd_e
% 0.69/1.06 % ------ Proving...
% 0.69/1.06 % ------ Problem Properties
% 0.69/1.06
% 0.69/1.06 %
% 0.69/1.06 % clauses 399
% 0.69/1.06 % conjectures 1
% 0.69/1.06 % EPR 399
% 0.69/1.06 % Horn 346
% 0.69/1.06 % unary 52
% 0.69/1.06 % binary 162
% 0.69/1.06 % lits 1000
% 0.69/1.06 % lits eq 0
% 0.69/1.06 % fd_pure 0
% 0.69/1.06 % fd_pseudo 0
% 0.69/1.06 % fd_cond 0
% 0.69/1.06 % fd_pseudo_cond 0
% 0.69/1.06 % AC symbols 0
% 0.69/1.06
% 0.69/1.06 % ------ Schedule EPR non Horn non eq is on
% 0.69/1.06
% 0.69/1.06 % ------ no equalities: superposition off
% 0.69/1.06
% 0.69/1.06 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 0.69/1.06
% 0.69/1.06
% 0.69/1.06 % ------
% 0.69/1.06 % Current options:
% 0.69/1.06 % ------
% 0.69/1.06
% 0.69/1.06
% 0.69/1.06 %
% 0.69/1.06
% 0.69/1.06 % ------ Proving...
% 0.69/1.06 %
% 0.69/1.06
% 0.69/1.06 % SZS status Unsatisfiable for theBenchmark.p
% 0.69/1.06
% 0.69/1.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.85/1.06
% 2.85/1.06
%------------------------------------------------------------------------------