%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN067-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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:04 PM UTC 2026
% Result : Unsatisfiable 1.80s 1.17s
% Output : CNFRefutation 1.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 41
% Syntax : Number of formulae : 272 ( 1 unt; 0 def)
% Number of atoms : 1138 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1479 ( 613 ~; 866 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 17 usr; 16 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-1 aty)
% Number of variables : 293 ( 0 sgn 293 !; 0 ?; 182 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(sk2(X0),sk1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_1) ).
fof(f2,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(X0,sk2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_2) ).
fof(f3,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk6(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_3) ).
fof(f4,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_r(X0,sk6(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_4) ).
fof(f5,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_p(sk1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_5) ).
fof(f6,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk6(X1))
| big_p(sk1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_6) ).
fof(f7,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_p(sk5(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_7) ).
fof(f8,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_p(sk5(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_8) ).
fof(f9,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_p(sk5(X1))
| big_p(sk1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_9) ).
fof(f18,negated_conjecture,
! [X2,X0,X1] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_18) ).
fof(f19,negated_conjecture,
! [X2,X0,X1] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_r(X0,sk4(X0))
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_19) ).
fof(f21,negated_conjecture,
! [X2,X0,X1] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_21) ).
fof(f24,negated_conjecture,
! [X2,X0,X1] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_24) ).
fof(f25,negated_conjecture,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_r(sk2(X1),sk1(X1))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_25) ).
fof(f26,negated_conjecture,
! [X0,X1] :
( big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_26) ).
fof(f27,negated_conjecture,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_r(X1,sk2(X1))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_27) ).
fof(f28,negated_conjecture,
! [X0,X1] :
( big_r(X1,sk2(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_28) ).
fof(f29,negated_conjecture,
! [X0,X1] :
( big_r(sk2(X1),sk1(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_29) ).
fof(f30,negated_conjecture,
! [X0,X1] :
( big_r(X1,sk2(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_30) ).
fof(f31,negated_conjecture,
! [X2,X0,X1] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_p(sk1(X0))
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_31) ).
fof(f34,negated_conjecture,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_34) ).
fof(f35,negated_conjecture,
! [X0,X1] :
( big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_35) ).
fof(f36,negated_conjecture,
! [X0,X1] :
( big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_36) ).
fof(f38,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_p(sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_38) ).
fof(f39,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk10,sk11)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_39) ).
fof(f40,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_40) ).
fof(f41,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_p(sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_41) ).
fof(f42,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk10,sk11)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_42) ).
fof(f43,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(sk9,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_p(X0)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_43) ).
fof(f44,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_44) ).
fof(f45,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_45) ).
fof(f46,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_46) ).
fof(f47,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_47) ).
fof(f48,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_48) ).
fof(f49,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(sk9,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_p(X0)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_49) ).
fof(f50,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_50) ).
fof(f51,negated_conjecture,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_51) ).
fof(f52,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(sk7,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk9)
| ~ big_p(X1)
| ~ big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_52) ).
fof(f53,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(sk9,X2)
| ~ big_r(sk7,X3)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(X1)
| ~ big_p(X0)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_53) ).
fof(f54,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(sk9,X2)
| ~ big_r(sk7,X3)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(X1)
| ~ big_p(X0)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_54) ).
fof(f55,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( ~ big_r(sk9,X4)
| ~ big_r(sk7,X5)
| ~ big_r(sk10,X3)
| ~ big_r(X5,X2)
| ~ big_r(X4,X1)
| ~ big_r(X3,X0)
| ~ big_p(X2)
| ~ big_p(X1)
| ~ big_p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel38_55) ).
tcf(c_104,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(sk6(X2),sk5(X2))
| big_r(sk2(X0),sk1(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_105,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X0,sk2(X0))
| big_r(sk6(X2),sk5(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_106,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X0,sk6(X0))
| big_r(sk2(X2),sk1(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_107,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,sk2(X2))
| big_r(X0,sk6(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_108,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk1(X0))
| big_r(sk6(X2),sk5(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_109,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk1(X0))
| big_r(X2,sk6(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_110,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk5(X0))
| big_r(sk2(X2),sk1(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_111,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk5(X0))
| big_r(X2,sk2(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_112,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk5(X2))
| big_p(sk1(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_121,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,sk4(X2))
| big_r(sk2(X0),sk1(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_122,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,sk4(X2))
| big_r(X0,sk2(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_124,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(sk1(X0))
| big_r(X2,sk4(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_127,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(sk3(X2))
| big_p(sk1(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_128,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(sk4(X1),sk3(X1))
| big_r(sk2(X0),sk1(X0)) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_129,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,sk4(X1))
| big_r(sk2(X0),sk1(X0)) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_130,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,sk2(X1))
| big_r(sk4(X0),sk3(X0)) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_131,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,sk2(X1))
| big_r(X0,sk4(X0)) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_132,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(sk3(X1))
| big_r(sk2(X0),sk1(X0)) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_133,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(sk3(X1))
| big_r(X0,sk2(X0)) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_134,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(sk1(X2))
| big_r(sk6(X0),sk5(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_137,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(sk1(X1))
| big_r(sk4(X0),sk3(X0)) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_138,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(sk1(X1))
| big_r(X0,sk4(X0)) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_139,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(sk3(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_141,negated_conjecture,
( big_p(sk8)
| big_p(sk11)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_142,negated_conjecture,
( big_p(sk8)
| big_r(sk10,sk11)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_143,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk8)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_144,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk8)
| big_p(sk11)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_145,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk8)
| big_r(sk10,sk11)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_146,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk8)
| ~ big_p(sk7)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(sk9,X2)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_147,negated_conjecture,
( big_p(sk11)
| big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_148,negated_conjecture,
( big_r(sk10,sk11)
| big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_149,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_150,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_151,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(sk10,sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_152,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(sk7,sk8)
| ~ big_p(sk7)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(sk9,X2)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_153,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk11)
| ~ big_p(sk9)
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_154,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(sk10,sk11)
| ~ big_p(sk9)
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_155,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ big_p(sk9)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(sk7,X2)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(sk11)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(sk7,X2)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_157,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(sk10,sk11)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(sk7,X2)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_158,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ big_p(X5)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(sk9,X2)
| ~ big_r(sk7,X4)
| ~ big_r(X4,X5)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_163,plain,
( big_p(sk7)
| big_p(sk3(sk7))
| big_r(sk2(sk7),sk1(sk7)) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_769,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_158]) ).
tcf(c_770,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_158]) ).
tcf(c_771,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_158]) ).
tcf(c_772,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_158]) ).
tcf(c_773,negated_conjecture,
( iPr_def_11
| iPr_def_10
| big_r(sk10,sk11) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_157]) ).
tcf(c_774,negated_conjecture,
( iPr_def_11
| iPr_def_10
| big_p(sk11) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_775,negated_conjecture,
( iPr_def_12
| iPr_def_10
| ~ big_p(sk9) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_155]) ).
tcf(c_776,negated_conjecture,
( iPr_def_10
| big_r(sk10,sk11)
| ~ big_p(sk9) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_154]) ).
tcf(c_777,negated_conjecture,
( iPr_def_10
| big_p(sk11)
| ~ big_p(sk9) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_153]) ).
tcf(c_778,negated_conjecture,
( iPr_def_12
| iPr_def_11
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_152]) ).
tcf(c_779,negated_conjecture,
( iPr_def_11
| big_r(sk10,sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_151]) ).
tcf(c_780,negated_conjecture,
( iPr_def_11
| big_p(sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_150]) ).
tcf(c_781,negated_conjecture,
( iPr_def_12
| big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_149]) ).
tcf(c_782,negated_conjecture,
( iPr_def_12
| iPr_def_11
| big_p(sk8)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_146]) ).
tcf(c_783,negated_conjecture,
( iPr_def_11
| big_p(sk8)
| big_r(sk10,sk11)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_145]) ).
tcf(c_784,negated_conjecture,
( iPr_def_11
| big_p(sk8)
| big_p(sk11)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_144]) ).
tcf(c_785,negated_conjecture,
( iPr_def_12
| big_p(sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_143]) ).
tcf(c_786,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ~ big_p(X1)
| big_r(X0,sk2(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_111]) ).
tcf(c_787,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| big_p(sk5(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_111]) ).
tcf(c_788,negated_conjecture,
( iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_111]) ).
tcf(c_789,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_15
| ~ big_p(X1)
| big_r(sk2(X0),sk1(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_110]) ).
tcf(c_790,negated_conjecture,
( iPr_def_15
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_110]) ).
tcf(c_791,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_16
| ~ big_p(X1)
| big_r(X0,sk6(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_107]) ).
tcf(c_792,negated_conjecture,
( iPr_def_16
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_107]) ).
tcf(c_793,negated_conjecture,
( iPr_def_16
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_106]) ).
tcf(c_794,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| big_p(sk3(X0))
| big_p(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_139]) ).
tcf(c_795,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| big_p(sk1(X0))
| big_p(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_139]) ).
tcf(c_796,negated_conjecture,
( iPr_def_18
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_139]) ).
tcf(c_797,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| big_p(X0)
| big_r(X0,sk4(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_138]) ).
tcf(c_798,negated_conjecture,
( iPr_def_19
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_138]) ).
tcf(c_799,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| big_p(X0)
| big_r(sk4(X0),sk3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_137]) ).
tcf(c_800,negated_conjecture,
( iPr_def_20
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_137]) ).
tcf(c_803,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_21
| ~ big_p(X1)
| big_r(sk6(X0),sk5(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_134]) ).
tcf(c_805,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| big_p(X0)
| big_r(X0,sk2(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_133]) ).
tcf(c_806,negated_conjecture,
( iPr_def_22
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_133]) ).
tcf(c_807,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| big_p(X0)
| big_r(sk2(X0),sk1(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_132]) ).
tcf(c_808,negated_conjecture,
( iPr_def_23
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_132]) ).
tcf(c_809,negated_conjecture,
( iPr_def_22
| iPr_def_19 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_131]) ).
tcf(c_810,negated_conjecture,
( iPr_def_22
| iPr_def_20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_130]) ).
tcf(c_811,negated_conjecture,
( iPr_def_23
| iPr_def_19 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_129]) ).
tcf(c_812,negated_conjecture,
( iPr_def_23
| iPr_def_20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_128]) ).
tcf(c_813,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_24
| big_p(sk1(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_127]) ).
tcf(c_817,negated_conjecture,
( iPr_def_24
| iPr_def_19 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_124]) ).
tcf(c_819,negated_conjecture,
( iPr_def_19
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_122]) ).
tcf(c_820,negated_conjecture,
( iPr_def_19
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_121]) ).
tcf(c_829,negated_conjecture,
( iPr_def_24
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_112]) ).
tcf(c_830,negated_conjecture,
( iPr_def_24
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_109]) ).
tcf(c_831,negated_conjecture,
( iPr_def_24
| iPr_def_21 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_108]) ).
tcf(c_832,negated_conjecture,
( iPr_def_21
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_105]) ).
tcf(c_833,negated_conjecture,
( iPr_def_21
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_104]) ).
tcf(c_834,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_772]) ).
tcf(c_838,negated_conjecture,
( iPr_def_11
| iPr_def_10
| big_r(sk10,sk11) ),
inference(demodulation,[status(thm)],[c_773]) ).
tcf(c_841,negated_conjecture,
( iPr_def_11
| iPr_def_10
| big_p(sk11) ),
inference(demodulation,[status(thm)],[c_774]) ).
tcf(c_844,negated_conjecture,
( iPr_def_12
| iPr_def_10
| ~ big_p(sk9) ),
inference(demodulation,[status(thm)],[c_775]) ).
tcf(c_847,negated_conjecture,
( iPr_def_10
| big_r(sk10,sk11)
| ~ big_p(sk9) ),
inference(demodulation,[status(thm)],[c_776]) ).
tcf(c_849,negated_conjecture,
( iPr_def_10
| big_p(sk11)
| ~ big_p(sk9) ),
inference(demodulation,[status(thm)],[c_777]) ).
tcf(c_850,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ big_p(X1)
| ~ big_r(sk7,X0)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_769]) ).
tcf(c_851,negated_conjecture,
( iPr_def_12
| iPr_def_11
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_778]) ).
tcf(c_854,negated_conjecture,
( iPr_def_11
| big_r(sk10,sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_779]) ).
tcf(c_856,negated_conjecture,
( iPr_def_11
| big_p(sk11)
| big_r(sk7,sk8)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_780]) ).
tcf(c_858,negated_conjecture,
( iPr_def_12
| big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_781]) ).
tcf(c_860,negated_conjecture,
( big_r(sk10,sk11)
| big_r(sk7,sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_148]) ).
tcf(c_862,negated_conjecture,
( iPr_def_12
| iPr_def_11
| big_p(sk8)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_782]) ).
tcf(c_865,negated_conjecture,
( iPr_def_11
| big_p(sk8)
| big_r(sk10,sk11)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_783]) ).
tcf(c_867,negated_conjecture,
( iPr_def_11
| big_p(sk8)
| big_p(sk11)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_784]) ).
tcf(c_868,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ big_p(X1)
| ~ big_r(sk9,X0)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_770]) ).
tcf(c_869,negated_conjecture,
( iPr_def_12
| big_p(sk8)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_785]) ).
tcf(c_870,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ big_p(X1)
| ~ big_r(sk10,X0)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_771]) ).
tcf(c_871,negated_conjecture,
( big_p(sk8)
| big_r(sk10,sk11)
| ~ big_p(sk9)
| ~ big_p(sk7) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_873,negated_conjecture,
( iPr_def_14
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_788]) ).
tcf(c_876,negated_conjecture,
( iPr_def_15
| iPr_def_14 ),
inference(demodulation,[status(thm)],[c_790]) ).
tcf(c_879,negated_conjecture,
( iPr_def_16
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_792]) ).
tcf(c_882,negated_conjecture,
( iPr_def_16
| iPr_def_15 ),
inference(demodulation,[status(thm)],[c_793]) ).
tcf(c_886,negated_conjecture,
( iPr_def_18
| iPr_def_17 ),
inference(demodulation,[status(thm)],[c_796]) ).
tcf(c_889,negated_conjecture,
( iPr_def_19
| iPr_def_18 ),
inference(demodulation,[status(thm)],[c_798]) ).
tcf(c_892,negated_conjecture,
( iPr_def_20
| iPr_def_18 ),
inference(demodulation,[status(thm)],[c_800]) ).
tcf(c_903,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_p(sk1(X0))
| ~ iPr_def_18 ),
inference(demodulation,[status(thm)],[c_795]) ).
tcf(c_904,negated_conjecture,
( iPr_def_22
| iPr_def_17 ),
inference(demodulation,[status(thm)],[c_806]) ).
tcf(c_907,negated_conjecture,
( iPr_def_23
| iPr_def_17 ),
inference(demodulation,[status(thm)],[c_808]) ).
tcf(c_910,negated_conjecture,
( iPr_def_22
| iPr_def_19 ),
inference(demodulation,[status(thm)],[c_809]) ).
tcf(c_913,negated_conjecture,
( iPr_def_22
| iPr_def_20 ),
inference(demodulation,[status(thm)],[c_810]) ).
tcf(c_916,negated_conjecture,
( iPr_def_23
| iPr_def_19 ),
inference(demodulation,[status(thm)],[c_811]) ).
tcf(c_919,negated_conjecture,
( iPr_def_23
| iPr_def_20 ),
inference(demodulation,[status(thm)],[c_812]) ).
tcf(c_930,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_p(sk3(X0))
| ~ iPr_def_17 ),
inference(demodulation,[status(thm)],[c_794]) ).
tcf(c_931,negated_conjecture,
( iPr_def_24
| iPr_def_19 ),
inference(demodulation,[status(thm)],[c_817]) ).
tcf(c_937,negated_conjecture,
( iPr_def_19
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_819]) ).
tcf(c_940,negated_conjecture,
( iPr_def_19
| iPr_def_15 ),
inference(demodulation,[status(thm)],[c_820]) ).
tcf(c_942,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_r(X0,sk4(X0))
| ~ iPr_def_19 ),
inference(demodulation,[status(thm)],[c_797]) ).
tcf(c_948,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_r(sk4(X0),sk3(X0))
| ~ iPr_def_20 ),
inference(demodulation,[status(thm)],[c_799]) ).
tcf(c_960,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_r(X0,sk2(X0))
| ~ iPr_def_22 ),
inference(demodulation,[status(thm)],[c_805]) ).
tcf(c_966,negated_conjecture,
! [X0: $i] :
( big_p(X0)
| big_r(sk2(X0),sk1(X0))
| ~ iPr_def_23 ),
inference(demodulation,[status(thm)],[c_807]) ).
tcf(c_967,negated_conjecture,
( iPr_def_24
| iPr_def_14 ),
inference(demodulation,[status(thm)],[c_829]) ).
tcf(c_969,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk5(X0))
| ~ iPr_def_14
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_787]) ).
tcf(c_970,negated_conjecture,
( iPr_def_24
| iPr_def_16 ),
inference(demodulation,[status(thm)],[c_830]) ).
tcf(c_972,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(X0,sk6(X0))
| ~ iPr_def_16
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_791]) ).
tcf(c_973,negated_conjecture,
( iPr_def_24
| iPr_def_21 ),
inference(demodulation,[status(thm)],[c_831]) ).
tcf(c_974,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(sk1(X0))
| ~ iPr_def_24
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_813]) ).
tcf(c_976,negated_conjecture,
( iPr_def_21
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_832]) ).
tcf(c_977,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(X0,sk2(X0))
| ~ iPr_def_13
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_786]) ).
tcf(c_979,negated_conjecture,
( iPr_def_21
| iPr_def_15 ),
inference(demodulation,[status(thm)],[c_833]) ).
tcf(c_980,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(sk2(X0),sk1(X0))
| ~ iPr_def_15
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_789]) ).
tcf(c_981,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(sk6(X0),sk5(X0))
| ~ iPr_def_21
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(demodulation,[status(thm)],[c_803]) ).
tcf(c_982,plain,
( big_p(sk7)
| big_p(sk1(sk7))
| ~ iPr_def_18 ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_983,plain,
( big_p(sk7)
| big_p(sk3(sk7))
| ~ iPr_def_17 ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_984,plain,
( big_p(sk7)
| big_r(sk7,sk4(sk7))
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_942]) ).
tcf(c_985,plain,
( big_p(sk7)
| big_r(sk7,sk2(sk7))
| ~ iPr_def_22 ),
inference(instantiation,[status(thm)],[c_960]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ big_p(sk1(X1))
| ~ big_r(sk7,X0)
| ~ big_r(X0,sk1(X1)) ),
inference(instantiation,[status(thm)],[c_850]) ).
tcf(c_1054,plain,
! [X0: $i] :
( big_r(sk7,sk2(sk7))
| ~ iPr_def_13
| ~ big_p(X0)
| ~ big_r(sk7,X0) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_1066,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ big_p(sk1(X0))
| ~ big_r(sk7,sk2(sk7))
| ~ big_r(sk2(sk7),sk1(X0)) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_1067,plain,
( ~ iPr_def_10
| ~ big_p(sk1(sk7))
| ~ big_r(sk7,sk2(sk7))
| ~ big_r(sk2(sk7),sk1(sk7)) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ big_p(sk1(X1))
| ~ big_r(sk9,X0)
| ~ big_r(X0,sk1(X1)) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_1070,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ big_p(sk3(X1))
| ~ big_r(sk9,X0)
| ~ big_r(X0,sk3(X1)) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_1074,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ big_p(sk1(X0))
| ~ big_r(sk9,sk2(sk9))
| ~ big_r(sk2(sk9),sk1(X0)) ),
inference(instantiation,[status(thm)],[c_1068]) ).
tcf(c_1076,plain,
( big_p(sk9)
| big_r(sk9,sk2(sk9))
| ~ iPr_def_22 ),
inference(instantiation,[status(thm)],[c_960]) ).
tcf(c_1085,plain,
( ~ iPr_def_11
| ~ big_p(sk1(sk9))
| ~ big_r(sk9,sk2(sk9))
| ~ big_r(sk2(sk9),sk1(sk9)) ),
inference(instantiation,[status(thm)],[c_1074]) ).
tcf(c_1087,plain,
( big_p(sk9)
| big_r(sk2(sk9),sk1(sk9))
| ~ iPr_def_23 ),
inference(instantiation,[status(thm)],[c_966]) ).
tcf(c_1092,plain,
( big_p(sk9)
| big_p(sk1(sk9))
| ~ iPr_def_18 ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_1107,plain,
! [X0: $i] :
( big_r(sk6(X0),sk5(X0))
| ~ iPr_def_21
| ~ big_p(sk11)
| ~ big_r(X0,sk11) ),
inference(instantiation,[status(thm)],[c_981]) ).
tcf(c_1108,plain,
! [X0: $i] :
( big_r(X0,sk6(X0))
| ~ iPr_def_16
| ~ big_p(sk11)
| ~ big_r(X0,sk11) ),
inference(instantiation,[status(thm)],[c_972]) ).
tcf(c_1109,plain,
! [X0: $i] :
( big_p(sk5(X0))
| ~ iPr_def_14
| ~ big_p(sk11)
| ~ big_r(X0,sk11) ),
inference(instantiation,[status(thm)],[c_969]) ).
tcf(c_1116,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ big_p(sk1(X1))
| ~ big_r(sk10,X0)
| ~ big_r(X0,sk1(X1)) ),
inference(instantiation,[status(thm)],[c_870]) ).
tcf(c_1150,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ big_p(sk1(X0))
| ~ big_r(sk10,sk2(sk10))
| ~ big_r(sk2(sk10),sk1(X0)) ),
inference(instantiation,[status(thm)],[c_1116]) ).
tcf(c_1151,plain,
! [X0: $i] :
( big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(X0)
| ~ big_r(sk10,X0) ),
inference(instantiation,[status(thm)],[c_977]) ).
tcf(c_1182,plain,
( big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1151]) ).
tcf(c_1191,plain,
( ~ iPr_def_12
| ~ big_p(sk1(sk10))
| ~ big_r(sk10,sk2(sk10))
| ~ big_r(sk2(sk10),sk1(sk10)) ),
inference(instantiation,[status(thm)],[c_1150]) ).
tcf(c_1192,plain,
! [X0: $i] :
( big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(X0)
| ~ big_r(sk10,X0) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1203,plain,
! [X0: $i] :
( big_p(sk1(sk10))
| ~ iPr_def_24
| ~ big_p(X0)
| ~ big_r(sk10,X0) ),
inference(instantiation,[status(thm)],[c_974]) ).
tcf(c_1219,plain,
( big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1192]) ).
tcf(c_1238,plain,
( big_p(sk1(sk10))
| ~ iPr_def_24
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1203]) ).
tcf(c_1263,plain,
( big_p(sk9)
| big_r(sk9,sk4(sk9))
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_942]) ).
tcf(c_1264,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ big_p(sk3(X0))
| ~ big_r(sk9,sk4(sk9))
| ~ big_r(sk4(sk9),sk3(X0)) ),
inference(instantiation,[status(thm)],[c_1070]) ).
tcf(c_1275,plain,
( big_p(sk5(sk10))
| ~ iPr_def_14
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1109]) ).
tcf(c_1296,plain,
( big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1107]) ).
tcf(c_1297,plain,
( big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk11)
| ~ big_r(sk10,sk11) ),
inference(instantiation,[status(thm)],[c_1108]) ).
tcf(c_1372,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ big_p(sk5(sk10))
| ~ big_r(sk10,X0)
| ~ big_r(X0,sk5(sk10)) ),
inference(instantiation,[status(thm)],[c_870]) ).
tcf(c_1470,plain,
( ~ iPr_def_12
| ~ big_p(sk5(sk10))
| ~ big_r(sk10,sk6(sk10))
| ~ big_r(sk6(sk10),sk5(sk10)) ),
inference(instantiation,[status(thm)],[c_1372]) ).
tcf(c_1490,plain,
( big_p(sk5(sk7))
| ~ iPr_def_14
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_969]) ).
tcf(c_1505,plain,
( big_r(sk7,sk6(sk7))
| ~ iPr_def_16
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_972]) ).
tcf(c_1535,plain,
( big_r(sk7,sk2(sk7))
| ~ iPr_def_13
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_1054]) ).
tcf(c_1589,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ big_p(X0)
| ~ big_r(sk7,sk6(sk7))
| ~ big_r(sk6(sk7),X0) ),
inference(instantiation,[status(thm)],[c_850]) ).
tcf(c_1647,plain,
( big_r(sk2(sk7),sk1(sk7))
| ~ iPr_def_15
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1846,plain,
( big_p(sk1(sk7))
| ~ iPr_def_24
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_974]) ).
tcf(c_2477,plain,
! [X0: $i] :
( big_p(X0)
| ~ iPr_def_23
| ~ iPr_def_10
| ~ big_p(sk1(X0))
| ~ big_r(sk7,sk2(X0)) ),
inference(superposition,[status(thm)],[c_966,c_850]) ).
tcf(c_2479,plain,
! [X0: $i] :
( big_p(X0)
| ~ iPr_def_20
| ~ iPr_def_10
| ~ big_p(sk3(X0))
| ~ big_r(sk7,sk4(X0)) ),
inference(superposition,[status(thm)],[c_948,c_850]) ).
tcf(c_2547,plain,
( big_p(sk7)
| ~ iPr_def_20
| ~ iPr_def_10
| ~ big_p(sk3(sk7))
| ~ big_r(sk7,sk4(sk7)) ),
inference(instantiation,[status(thm)],[c_2479]) ).
tcf(c_2548,plain,
( big_p(sk7)
| ~ iPr_def_23
| ~ iPr_def_10
| ~ big_p(sk1(sk7))
| ~ big_r(sk7,sk2(sk7)) ),
inference(instantiation,[status(thm)],[c_2477]) ).
tcf(c_2726,plain,
( big_r(sk6(sk7),sk5(sk7))
| ~ iPr_def_21
| ~ big_p(sk8)
| ~ big_r(sk7,sk8) ),
inference(instantiation,[status(thm)],[c_981]) ).
tcf(c_2860,plain,
( iPr_def_11
| big_p(sk5(sk10))
| big_r(sk7,sk8)
| ~ iPr_def_14
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_969]) ).
tcf(c_2861,plain,
( iPr_def_11
| big_p(sk8)
| big_p(sk5(sk10))
| ~ iPr_def_14
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_969]) ).
tcf(c_2862,plain,
( iPr_def_10
| big_p(sk5(sk10))
| ~ iPr_def_14
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_969]) ).
tcf(c_2863,plain,
( big_p(sk5(sk10))
| big_r(sk7,sk8)
| ~ iPr_def_14
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_969]) ).
tcf(c_2864,plain,
( big_p(sk8)
| big_p(sk5(sk10))
| ~ iPr_def_14
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_871,c_969]) ).
tcf(c_2865,plain,
( iPr_def_11
| iPr_def_10
| big_p(sk5(sk10))
| ~ iPr_def_14
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_969]) ).
tcf(c_3275,plain,
( iPr_def_11
| big_p(sk1(sk10))
| big_r(sk7,sk8)
| ~ iPr_def_24
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_974]) ).
tcf(c_3276,plain,
( iPr_def_11
| big_p(sk8)
| big_p(sk1(sk10))
| ~ iPr_def_24
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_974]) ).
tcf(c_3277,plain,
( iPr_def_10
| big_p(sk1(sk10))
| ~ iPr_def_24
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_974]) ).
tcf(c_3278,plain,
( big_p(sk1(sk10))
| big_r(sk7,sk8)
| ~ iPr_def_24
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_974]) ).
tcf(c_3280,plain,
( iPr_def_11
| iPr_def_10
| big_p(sk1(sk10))
| ~ iPr_def_24
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_974]) ).
tcf(c_3505,plain,
( ~ iPr_def_10
| ~ big_p(sk5(sk7))
| ~ big_r(sk7,sk6(sk7))
| ~ big_r(sk6(sk7),sk5(sk7)) ),
inference(instantiation,[status(thm)],[c_1589]) ).
tcf(c_3841,plain,
( iPr_def_11
| iPr_def_10
| big_p(sk5(sk10)) ),
inference(global_subsumption_just,[status(thm)],[c_2865,c_873,c_876,c_967,c_834,c_841,c_838,c_1182,c_1191,c_1219,c_2865,c_3280]) ).
tcf(c_3869,plain,
( iPr_def_11
| iPr_def_10
| big_p(sk1(sk10)) ),
inference(global_subsumption_just,[status(thm)],[c_3280,c_970,c_973,c_834,c_841,c_838,c_1296,c_1297,c_1470,c_3280,c_3841]) ).
tcf(c_3897,plain,
( iPr_def_10
| big_p(sk5(sk10))
| ~ big_p(sk9) ),
inference(global_subsumption_just,[status(thm)],[c_2862,c_873,c_876,c_967,c_844,c_849,c_847,c_1182,c_1191,c_1219,c_1238,c_1275]) ).
tcf(c_3925,plain,
( iPr_def_10
| big_p(sk1(sk10))
| ~ big_p(sk9) ),
inference(global_subsumption_just,[status(thm)],[c_3277,c_970,c_973,c_844,c_849,c_847,c_1238,c_1296,c_1297,c_1470,c_3897]) ).
tcf(c_4598,plain,
( ~ iPr_def_11
| ~ big_p(sk3(sk9))
| ~ big_r(sk9,sk4(sk9))
| ~ big_r(sk4(sk9),sk3(sk9)) ),
inference(instantiation,[status(thm)],[c_1264]) ).
tcf(c_4599,plain,
( big_p(sk9)
| big_r(sk4(sk9),sk3(sk9))
| ~ iPr_def_20 ),
inference(instantiation,[status(thm)],[c_948]) ).
tcf(c_4662,plain,
( iPr_def_11
| big_r(sk7,sk8)
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_972]) ).
tcf(c_4663,plain,
( iPr_def_11
| big_p(sk8)
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_972]) ).
tcf(c_4664,plain,
( iPr_def_10
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_972]) ).
tcf(c_4665,plain,
( big_r(sk7,sk8)
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_972]) ).
tcf(c_4666,plain,
( big_p(sk8)
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_871,c_972]) ).
tcf(c_4667,plain,
( iPr_def_11
| iPr_def_10
| big_r(sk10,sk6(sk10))
| ~ iPr_def_16
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_972]) ).
tcf(c_5249,plain,
( iPr_def_11
| big_r(sk7,sk8)
| big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_977]) ).
tcf(c_5250,plain,
( iPr_def_11
| big_p(sk8)
| big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_977]) ).
tcf(c_5251,plain,
( iPr_def_10
| big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_977]) ).
tcf(c_5252,plain,
( big_r(sk7,sk8)
| big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_977]) ).
tcf(c_5254,plain,
( iPr_def_11
| iPr_def_10
| big_r(sk10,sk2(sk10))
| ~ iPr_def_13
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_977]) ).
tcf(c_5476,plain,
( big_p(sk9)
| big_p(sk3(sk9))
| ~ iPr_def_17 ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_5579,plain,
( iPr_def_11
| big_r(sk7,sk8)
| big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_980]) ).
tcf(c_5580,plain,
( iPr_def_11
| big_p(sk8)
| big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_980]) ).
tcf(c_5581,plain,
( iPr_def_10
| big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_980]) ).
tcf(c_5582,plain,
( big_r(sk7,sk8)
| big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_980]) ).
tcf(c_5584,plain,
( iPr_def_11
| iPr_def_10
| big_r(sk2(sk10),sk1(sk10))
| ~ iPr_def_15
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_980]) ).
tcf(c_5977,plain,
( iPr_def_11
| big_r(sk7,sk8)
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_854,c_981]) ).
tcf(c_5978,plain,
( iPr_def_11
| big_p(sk8)
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_865,c_981]) ).
tcf(c_5979,plain,
( iPr_def_10
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk9)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_847,c_981]) ).
tcf(c_5980,plain,
( big_r(sk7,sk8)
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_860,c_981]) ).
tcf(c_5981,plain,
( big_p(sk8)
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_871,c_981]) ).
tcf(c_5982,plain,
( iPr_def_11
| iPr_def_10
| big_r(sk6(sk10),sk5(sk10))
| ~ iPr_def_21
| ~ big_p(sk11) ),
inference(superposition,[status(thm)],[c_838,c_981]) ).
tcf(c_6299,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5980,c_5981,c_5977,c_5978,c_5979,c_5982,c_5582,c_5579,c_5580,c_5581,c_5584,c_5476,c_5252,c_5249,c_5250,c_5251,c_5254,c_4665,c_4666,c_4662,c_4663,c_4664,c_4667,c_4599,c_4598,c_3925,c_3897,c_3869,c_3841,c_3505,c_3278,c_3275,c_3276,c_2863,c_2864,c_2860,c_2861,c_2726,c_2548,c_2547,c_1846,c_1647,c_1535,c_1505,c_1490,c_1470,c_1297,c_1296,c_1263,c_1238,c_1219,c_1191,c_1182,c_1092,c_1087,c_1085,c_1076,c_1067,c_858,c_869,c_856,c_985,c_984,c_867,c_851,c_983,c_982,c_862,c_847,c_849,c_844,c_838,c_841,c_834,c_979,c_976,c_973,c_970,c_967,c_940,c_937,c_931,c_919,c_916,c_913,c_910,c_907,c_904,c_892,c_889,c_886,c_882,c_879,c_876,c_873,c_163,c_142,c_147,c_141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN067-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 00:05:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 1.80/1.17 % SZS status Started for theBenchmark.p
% 1.80/1.17 % SZS status Unsatisfiable for theBenchmark.p
% 1.80/1.17
% 1.80/1.17 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.80/1.17
% 1.80/1.17 % ------ iProver source info
% 1.80/1.17
% 1.80/1.17 % git: date: 2026-07-19 20:42:38 +0200
% 1.80/1.17 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.80/1.17 % git: non_committed_changes: false
% 1.80/1.17
% 1.80/1.17 % ------ Parsing...% successful
% 1.80/1.17
% 1.80/1.17
% 1.80/1.17 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.80/1.17
% 1.80/1.17 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 1.80/1.17
% 1.80/1.17 % ------ Preprocessing... gs_s sp: 93 0s gs_e snvd_s sp: 0 0s snvd_e
% 1.80/1.17 % ------ Proving...
% 1.80/1.17 % ------ Problem Properties
% 1.80/1.17
% 1.80/1.17 %
% 1.80/1.17 % clauses 70
% 1.80/1.17 % conjectures 70
% 1.80/1.17 % EPR 58
% 1.80/1.17 % Horn 10
% 1.80/1.17 % unary 1
% 1.80/1.17 % binary 36
% 1.80/1.17 % lits 193
% 1.80/1.17 % lits eq 0
% 1.80/1.17 % fd_pure 0
% 1.80/1.17 % fd_pseudo 0
% 1.80/1.17 % fd_cond 0
% 1.80/1.17 % fd_pseudo_cond 0
% 1.80/1.17 % AC symbols 0
% 1.80/1.17
% 1.80/1.17 % ------ Schedule dynamic 5 is on
% 1.80/1.17
% 1.80/1.17 % ------ no equalities: superposition off
% 1.80/1.17
% 1.80/1.17 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.80/1.17
% 1.80/1.17
% 1.80/1.17 % ------
% 1.80/1.17 % Current options:
% 1.80/1.17 % ------
% 1.80/1.17
% 1.80/1.17
% 1.80/1.17 %
% 1.80/1.17
% 1.80/1.17 % ------ Proving...
% 1.80/1.17 %
% 1.80/1.17
% 1.80/1.17 % SZS status Unsatisfiable for theBenchmark.p
% 1.80/1.17
% 1.80/1.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.80/1.18
% 1.80/1.18
%------------------------------------------------------------------------------