%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO186+3 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:04:18 EDT 2024
% Result : Theorem 58.73s 58.77s
% Output : CNFRefutation 58.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO186+3 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 21 06:04:39 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.58 start to proof:theBenchmark
% 58.64/58.75 %-------------------------------------------
% 58.64/58.75 % File :CSE---1.7
% 58.64/58.75 % Problem :theBenchmark
% 58.64/58.75 % Transform :cnf
% 58.64/58.75 % Format :tptp:raw
% 58.64/58.75 % Command :java -jar mcs_scs.jar %d %s
% 58.64/58.75
% 58.64/58.75 % Result :Theorem 58.130000s
% 58.64/58.75 % Output :CNFRefutation 58.130000s
% 58.64/58.75 %-------------------------------------------
% 58.73/58.76 %------------------------------------------------------------------------------
% 58.73/58.76 % File : GEO186+3 : TPTP v8.2.0. Released v4.0.0.
% 58.73/58.76 % Domain : Geometry (Constructive)
% 58.73/58.76 % Problem : Lemma on symmetry and apartness
% 58.73/58.76 % Version : [vPl95] axioms.
% 58.73/58.76 % English : If the lines U and V are convergent, then the point that is
% 58.73/58.76 % incident with both lines is equal to the intersection point
% 58.73/58.76 % of both lines.
% 58.73/58.76
% 58.73/58.76 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 58.73/58.76 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.73/58.76 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.73/58.76 % Source : [Rat07]
% 58.73/58.76 % Names : Lemma 4.5.ii [vPl95]
% 58.73/58.76
% 58.73/58.76 % Status : Theorem
% 58.73/58.76 % Rating : 0.00 v6.1.0, 0.08 v6.0.0, 0.00 v5.5.0, 0.17 v5.4.0, 0.22 v5.3.0, 0.26 v5.2.0, 0.29 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.21 v4.0.0
% 58.73/58.76 % Syntax : Number of formulae : 36 ( 7 unt; 0 def)
% 58.73/58.76 % Number of atoms : 98 ( 0 equ)
% 58.73/58.76 % Maximal formula atoms : 6 ( 2 avg)
% 58.73/58.76 % Number of connectives : 90 ( 28 ~; 19 |; 16 &)
% 58.73/58.76 % ( 5 <=>; 22 =>; 0 <=; 0 <~>)
% 58.73/58.76 % Maximal formula depth : 9 ( 6 avg)
% 58.73/58.76 % Maximal term depth : 2 ( 1 avg)
% 58.73/58.76 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 58.73/58.77 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 58.73/58.77 % Number of variables : 85 ( 85 !; 0 ?)
% 58.73/58.77 % SPC : FOF_THM_RFO_NEQ
% 58.73/58.77
% 58.73/58.77 % Comments :
% 58.73/58.77 %------------------------------------------------------------------------------
% 58.73/58.77 include('Axioms/GEO006+0.ax').
% 58.73/58.77 include('Axioms/GEO006+1.ax').
% 58.73/58.77 include('Axioms/GEO006+2.ax').
% 58.73/58.77 include('Axioms/GEO006+3.ax').
% 58.73/58.77 include('Axioms/GEO006+4.ax').
% 58.73/58.77 include('Axioms/GEO006+5.ax').
% 58.73/58.77 include('Axioms/GEO006+6.ax').
% 58.73/58.77 %------------------------------------------------------------------------------
% 58.73/58.77 fof(con,conjecture,
% 58.73/58.77 ! [X,Y,U,V] :
% 58.73/58.77 ( ( distinct_points(X,Y)
% 58.73/58.77 & convergent_lines(U,V)
% 58.73/58.77 & incident_point_and_line(X,U)
% 58.73/58.77 & incident_point_and_line(X,V) )
% 58.73/58.77 => equal_points(X,intersection_point(U,V)) ) ).
% 58.73/58.77
% 58.73/58.77 %------------------------------------------------------------------------------
% 58.73/58.77 %-------------------------------------------
% 58.73/58.77 % Proof found
% 58.73/58.77 % SZS status Theorem for theBenchmark
% 58.73/58.77 % SZS output start Proof
% 58.73/58.77 %ClaNum:51(EqnAxiom:0)
% 58.73/58.77 %VarNum:218(SingletonVarNum:98)
% 58.73/58.77 %MaxLitNum:6
% 58.73/58.77 %MaxfuncDepth:1
% 58.73/58.77 %SharedTerms:10
% 58.73/58.77 %goalClause: 1 2 3 4 8
% 58.73/58.77 %singleGoalClaCount:5
% 58.73/58.77 [1]P1(a1,a2)
% 58.73/58.77 [2]P2(a3,a4)
% 58.73/58.77 [3]P5(a1,a3)
% 58.73/58.77 [4]P5(a1,a4)
% 58.73/58.77 [8]~P6(a1,f5(a3,a4))
% 58.73/58.77 [5]~P1(x51,x51)
% 58.73/58.77 [6]~P4(x61,x61)
% 58.73/58.77 [7]~P2(x71,x71)
% 58.73/58.77 [9]~P3(x91,f6(x92,x91))
% 58.73/58.77 [10]~P3(x101,f7(x102,x101))
% 58.73/58.77 [11]~P2(f6(x111,x112),x111)
% 58.73/58.77 [12]~P8(f7(x121,x122),x121)
% 58.73/58.77 [13]P6(x131,x132)+P1(x131,x132)
% 58.73/58.77 [14]P7(x141,x142)+P4(x141,x142)
% 58.73/58.78 [16]P8(x161,x162)+P2(x161,x162)
% 58.73/58.78 [17]P9(x171,x172)+P2(x171,x172)
% 58.73/58.78 [18]P5(x181,x182)+P3(x181,x182)
% 58.73/58.78 [19]P10(x191,x192)+P8(x191,x192)
% 58.73/58.78 [20]~P4(x201,x202)+P2(x201,x202)
% 58.73/58.78 [23]~P6(x231,x232)+~P1(x231,x232)
% 58.73/58.78 [24]~P7(x241,x242)+~P4(x241,x242)
% 58.73/58.78 [25]~P9(x251,x252)+~P2(x251,x252)
% 58.73/58.78 [26]~P5(x261,x262)+~P3(x261,x262)
% 58.73/58.78 [27]~P10(x271,x272)+~P8(x271,x272)
% 58.73/58.78 [47]~P1(x471,x472)+~P3(x472,f8(x471,x472))
% 58.73/58.78 [48]~P1(x481,x482)+~P3(x481,f8(x481,x482))
% 58.73/58.78 [49]~P2(x491,x492)+~P3(f5(x491,x492),x492)
% 58.73/58.78 [50]~P2(x501,x502)+~P3(f5(x501,x502),x501)
% 58.73/58.78 [21]~P12(x212)+~P11(x211)+P11(f6(x211,x212))
% 58.73/58.78 [22]~P12(x222)+~P11(x221)+P11(f7(x221,x222))
% 58.73/58.78 [28]~P1(x283,x281)+P1(x281,x282)+P1(x283,x282)
% 58.73/58.78 [29]~P3(x291,x293)+P1(x291,x292)+P3(x292,x293)
% 58.73/58.78 [30]~P4(x303,x301)+P4(x301,x302)+P4(x303,x302)
% 58.73/58.78 [31]~P2(x313,x311)+P4(x311,x312)+P2(x313,x312)
% 58.73/58.78 [32]~P3(x323,x321)+P4(x321,x322)+P3(x323,x322)
% 58.73/58.78 [33]~P2(x333,x331)+P2(x331,x332)+P2(x333,x332)
% 58.73/58.78 [34]~P2(x343,x342)+P8(x341,x342)+P8(x341,x343)
% 58.73/58.78 [36]~P11(x362)+~P11(x361)+~P2(x361,x362)+P12(f5(x361,x362))
% 58.73/58.78 [37]~P12(x372)+~P12(x371)+~P1(x371,x372)+P11(f8(x371,x372))
% 58.73/58.78 [39]~P2(x391,x393)+~P8(x391,x393)+P2(x391,x392)+P8(x393,x392)
% 58.73/58.78 [40]~P2(x402,x403)+~P8(x402,x403)+P2(x401,x402)+P2(x401,x403)
% 58.73/58.78 [41]~P2(x412,x413)+~P8(x412,x413)+P2(x411,x412)+P8(x411,x413)
% 58.73/58.78 [42]~P2(x423,x421)+~P8(x423,x421)+P2(x421,x422)+P8(x423,x422)
% 58.73/58.78 [43]~P2(x433,x432)+~P8(x433,x432)+P2(x431,x432)+P8(x431,x433)
% 58.73/58.78 [44]~P2(x441,x443)+~P8(x441,x443)+P8(x441,x442)+P8(x443,x442)
% 58.73/58.78 [46]P8(x463,x464)+~P4(x463,x462)+P3(x461,x462)+P3(x461,x463)+P8(x462,x464)
% 58.73/58.78 [51]P3(x514,x513)+~P1(x514,x511)+~P4(x513,x512)+P3(x511,x512)+P3(x511,x513)+P3(x514,x512)
% 58.73/58.78 %EqnAxiom
% 58.73/58.78
% 58.73/58.78 %-------------------------------------------
% 58.79/58.79 cnf(68,plain,
% 58.79/58.79 (~P4(f6(x681,x682),x681)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,9,11,12,23,25,13,14,16,17,18,19,20])).
% 58.79/58.79 cnf(72,plain,
% 58.79/58.79 (P1(a2,a1)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,9,11,12,23,25,13,14,16,17,18,19,20,27,28])).
% 58.79/58.79 cnf(75,plain,
% 58.79/58.79 (P4(a4,a3)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,9,11,12,23,25,13,14,16,17,18,19,20,27,28,31])).
% 58.79/58.79 cnf(76,plain,
% 58.79/58.79 (~P2(x761,x761)),
% 58.79/58.79 inference(rename_variables,[],[7])).
% 58.79/58.79 cnf(78,plain,
% 58.79/58.79 (P2(a4,a3)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,76,9,11,12,23,25,13,14,16,17,18,19,20,27,28,31,33])).
% 58.79/58.79 cnf(81,plain,
% 58.79/58.79 (P8(f7(a3,x811),a4)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,76,9,11,12,23,25,13,14,16,17,18,19,20,27,28,31,33,34])).
% 58.79/58.79 cnf(84,plain,
% 58.79/58.79 (P4(a3,a4)),
% 58.79/58.79 inference(scs_inference,[],[1,2,5,6,7,76,9,11,12,23,25,13,14,16,17,18,19,20,27,28,31,33,34,30])).
% 58.79/58.79 cnf(104,plain,
% 58.79/58.79 (~P6(a2,a1)),
% 58.79/58.79 inference(scs_inference,[],[72,84,24,23])).
% 58.79/58.79 cnf(106,plain,
% 58.79/58.79 (P8(f6(x1061,x1062),x1061)),
% 58.79/58.79 inference(scs_inference,[],[72,84,11,24,23,16])).
% 58.79/58.79 cnf(118,plain,
% 58.79/58.79 (~P3(x1181,f6(f7(x1182,x1181),x1183))),
% 58.79/58.79 inference(scs_inference,[],[78,81,72,10,68,84,11,24,23,16,27,14,25,18,17,32])).
% 58.79/58.79 cnf(119,plain,
% 58.79/58.79 (~P4(f6(x1191,x1192),x1191)),
% 58.79/58.79 inference(rename_variables,[],[68])).
% 58.79/58.79 cnf(121,plain,
% 58.79/58.79 (~P2(f6(x1211,x1212),f6(x1211,x1213))),
% 58.79/58.79 inference(scs_inference,[],[78,81,72,10,68,119,84,11,24,23,16,27,14,25,18,17,32,31])).
% 58.79/58.79 cnf(124,plain,
% 58.79/58.79 (~P4(f6(x1241,x1242),f6(x1241,x1243))),
% 58.79/58.79 inference(scs_inference,[],[78,81,72,10,68,119,84,11,24,23,16,27,14,25,18,17,32,31,20])).
% 58.79/58.79 cnf(126,plain,
% 58.79/58.79 (P8(a4,a3)+~P2(f7(a3,x1261),a4)),
% 58.79/58.79 inference(scs_inference,[],[78,81,72,10,68,119,84,11,12,24,23,16,27,14,25,18,17,32,31,20,44])).
% 58.79/58.79 cnf(170,plain,
% 58.79/58.79 (P8(f6(x1701,x1702),x1703)+~P4(f6(x1701,x1702),f7(x1703,x1702))),
% 58.79/58.79 inference(scs_inference,[],[121,10,9,106,124,118,12,11,14,16,27,18,17,33,20,46])).
% 58.79/58.79 cnf(273,plain,
% 58.79/58.79 (~P3(a1,a3)),
% 58.79/58.79 inference(scs_inference,[],[3,5,26,29])).
% 58.79/58.79 cnf(274,plain,
% 58.79/58.79 (P8(a3,x2741)+~P4(a3,f7(x2741,a1))),
% 58.79/58.79 inference(scs_inference,[],[10,273,12,46])).
% 58.79/58.79 cnf(278,plain,
% 58.79/58.79 (~P10(a3,x2781)+~P4(a3,f7(x2781,a1))),
% 58.79/58.79 inference(scs_inference,[],[10,273,12,46,27])).
% 58.79/58.79 cnf(444,plain,
% 58.79/58.79 (~P3(a2,f8(a2,a1))),
% 58.79/58.79 inference(scs_inference,[],[104,48,13])).
% 58.79/58.79 cnf(848,plain,
% 58.79/58.79 (P4(a4,f7(x8481,a1))+~P10(a3,x8481)),
% 58.79/58.79 inference(scs_inference,[],[84,278,30])).
% 58.79/58.79 cnf(999,plain,
% 58.79/58.79 (P8(a3,x9991)+P4(a4,f7(x9991,a1))),
% 58.79/58.79 inference(scs_inference,[],[848,19])).
% 58.79/58.79 cnf(1539,plain,
% 58.79/58.79 (P8(f6(x15391,x15392),x15393)+P7(f6(x15391,x15392),f7(x15393,x15392))),
% 58.79/58.79 inference(scs_inference,[],[170,14])).
% 58.79/58.79 cnf(1759,plain,
% 58.79/58.79 (P7(f6(x17591,x17592),f7(x17593,x17592))+~P10(f6(x17591,x17592),x17593)),
% 58.79/58.79 inference(scs_inference,[],[1539,27])).
% 58.79/58.79 cnf(1839,plain,
% 58.79/58.79 (~P4(f6(x18391,x18392),f7(x18393,x18392))+~P10(f6(x18391,x18392),x18393)),
% 58.79/58.79 inference(scs_inference,[],[1759,24])).
% 58.79/58.79 cnf(1887,plain,
% 58.79/58.79 (~P10(f6(x18871,x18872),x18873)+~P2(f7(x18873,x18872),f6(x18871,x18872))),
% 58.79/58.79 inference(scs_inference,[],[7,1839,31])).
% 58.79/58.79 cnf(2022,plain,
% 58.79/58.79 (~P10(f6(x20221,x20222),x20223)+~P4(f7(x20223,x20222),f6(x20221,x20222))),
% 58.79/58.79 inference(scs_inference,[],[1887,20])).
% 58.79/58.79 cnf(2199,plain,
% 58.79/58.79 (~P10(f6(x21991,x21992),x21993)+P7(f7(x21993,x21992),f6(x21991,x21992))),
% 58.79/58.79 inference(scs_inference,[],[2022,14])).
% 58.79/58.79 cnf(2286,plain,
% 58.79/58.79 (P8(f6(x22861,x22862),x22863)+P7(f7(x22863,x22862),f6(x22861,x22862))),
% 58.79/58.79 inference(scs_inference,[],[2199,19])).
% 58.79/58.79 cnf(2371,plain,
% 58.79/58.79 (~P4(f7(x23711,x23712),f6(x23713,x23712))+P8(f6(x23713,x23712),x23711)),
% 58.79/58.79 inference(scs_inference,[],[2286,24])).
% 58.79/58.79 cnf(6431,plain,
% 58.79/58.79 (~P4(f6(x64311,x64312),x64311)),
% 58.79/58.79 inference(rename_variables,[],[68])).
% 58.79/58.79 cnf(6433,plain,
% 58.79/58.79 (~P2(x64331,f6(x64331,x64332))),
% 58.79/58.79 inference(scs_inference,[],[68,6431,444,7,32,31])).
% 58.79/58.79 cnf(6436,plain,
% 58.79/58.79 (P2(a4,f6(a3,x64361))),
% 58.79/58.79 inference(scs_inference,[],[68,6431,2,444,7,32,31,33])).
% 58.79/58.79 cnf(6448,plain,
% 58.79/58.79 (P4(a4,f6(a3,x64481))),
% 58.79/58.79 inference(scs_inference,[],[68,6431,2,444,7,84,32,31,33,25,18,17,20,16,30])).
% 58.79/58.79 cnf(6469,plain,
% 58.79/58.79 (~P4(x64691,f6(x64691,x64692))),
% 58.79/58.79 inference(scs_inference,[],[6433,17,20])).
% 58.79/58.79 cnf(6595,plain,
% 58.79/58.79 (~P10(f6(a3,x65951),x65952)+~P4(f6(a3,x65951),f7(x65952,a1))),
% 58.79/58.79 inference(scs_inference,[],[68,10,273,12,32,18,46,27])).
% 58.79/58.79 cnf(6667,plain,
% 58.79/58.79 (P7(f6(a3,x66671),f7(x66672,a1))+~P10(f6(a3,x66671),x66672)),
% 58.79/58.79 inference(scs_inference,[],[6595,14])).
% 58.79/58.79 cnf(6699,plain,
% 58.79/58.79 (P8(f6(a3,x66991),x66992)+P7(f6(a3,x66991),f7(x66992,a1))),
% 58.79/58.79 inference(scs_inference,[],[6667,19])).
% 58.79/58.79 cnf(7125,plain,
% 58.79/58.79 (P8(f7(a4,x71251),a3)),
% 58.79/58.79 inference(scs_inference,[],[78,12,34])).
% 58.79/58.79 cnf(7128,plain,
% 58.79/58.79 (P2(a3,f6(a4,x71281))),
% 58.79/58.79 inference(scs_inference,[],[78,6433,12,34,33])).
% 58.79/58.79 cnf(7189,plain,
% 58.79/58.79 (P7(f7(a4,x71891),a3)+P2(f6(a3,x71892),f7(a4,x71891))),
% 58.79/58.79 inference(scs_inference,[],[7125,11,40,17,20,14])).
% 58.79/58.79 cnf(7203,plain,
% 58.79/58.79 (P8(a4,a3)+~P2(f7(a4,x72031),a3)),
% 58.79/58.79 inference(scs_inference,[],[2,7125,7,12,44,43])).
% 58.79/58.79 cnf(7316,plain,
% 58.79/58.79 (~P10(a4,a3)+~P2(f7(a4,x73161),a3)),
% 58.79/58.79 inference(scs_inference,[],[7203,27])).
% 58.79/58.79 cnf(7408,plain,
% 58.79/58.79 (~P4(f7(a4,x74081),a3)+~P10(a4,a3)),
% 58.79/58.79 inference(scs_inference,[],[7316,20])).
% 58.79/58.79 cnf(9114,plain,
% 58.79/58.79 (~P3(a1,a4)),
% 58.79/58.79 inference(scs_inference,[],[4,26])).
% 58.79/58.79 cnf(9116,plain,
% 58.79/58.79 (P8(a4,x91161)+~P4(a4,f7(x91161,a1))),
% 58.79/58.79 inference(scs_inference,[],[4,10,12,26,46])).
% 58.79/58.79 cnf(9120,plain,
% 58.79/58.79 (~P10(a4,x91201)+~P4(a4,f7(x91201,a1))),
% 58.79/58.79 inference(scs_inference,[],[4,10,12,26,46,27])).
% 58.79/58.79 cnf(9240,plain,
% 58.79/58.79 (P4(a3,f7(x92401,a1))+~P10(a4,x92401)),
% 58.79/58.79 inference(scs_inference,[],[75,9120,30])).
% 58.79/58.79 cnf(12559,plain,
% 58.79/58.79 (P2(f7(x125591,x125592),x125591)),
% 58.79/58.79 inference(scs_inference,[],[78,12,49,50,16])).
% 58.79/58.79 cnf(12561,plain,
% 58.79/58.79 (P4(f6(a4,x125611),f6(a3,x125612))),
% 58.79/58.79 inference(scs_inference,[],[7128,78,6433,12,49,50,16,31])).
% 58.79/58.79 cnf(12562,plain,
% 58.79/58.79 (~P2(x125621,f6(x125621,x125622))),
% 58.79/58.79 inference(rename_variables,[],[6433])).
% 58.79/58.79 cnf(12568,plain,
% 58.79/58.79 (~P3(x125681,x125682)),
% 58.79/58.80 inference(scs_inference,[],[7128,6469,78,6433,9,12,49,50,16,31,25,24,32])).
% 58.79/58.80 cnf(12569,plain,
% 58.79/58.80 (~P3(x125691,f6(x125692,x125691))),
% 58.79/58.80 inference(rename_variables,[],[9])).
% 58.79/58.80 cnf(12572,plain,
% 58.79/58.80 (~P2(x125721,f6(x125721,x125722))),
% 58.79/58.80 inference(rename_variables,[],[6433])).
% 58.79/58.80 cnf(12575,plain,
% 58.79/58.80 (P2(a4,f6(a3,x125751))),
% 58.79/58.80 inference(rename_variables,[],[6436])).
% 58.79/58.80 cnf(12579,plain,
% 58.79/58.80 (P2(a4,f6(a3,x125791))),
% 58.79/58.80 inference(rename_variables,[],[6436])).
% 58.79/58.80 cnf(12586,plain,
% 58.79/58.80 (P3(a2,f6(a3,a1))+~P8(a4,a3)),
% 58.79/58.80 inference(scs_inference,[],[1,7128,6436,12575,12579,6448,9114,6469,78,6433,12562,12572,11,9,12569,12,49,50,16,31,25,24,32,42,43,39,41,51])).
% 58.79/58.80 cnf(12595,plain,
% 58.79/58.80 (~P8(a4,a3)),
% 58.79/58.80 inference(scs_inference,[],[12568,12586])).
% 58.79/58.80 cnf(12600,plain,
% 58.79/58.80 (P2(f7(x126001,x126002),x126001)),
% 58.79/58.80 inference(rename_variables,[],[12559])).
% 58.79/58.80 cnf(12602,plain,
% 58.79/58.80 (P4(f6(a4,x126021),a3)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12561,68,12,12586,19,34,30])).
% 58.79/58.80 cnf(12605,plain,
% 58.79/58.80 (P2(f7(x126051,x126052),f6(x126051,x126053))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,68,6433,12,12586,19,34,30,33])).
% 58.79/58.80 cnf(12606,plain,
% 58.79/58.80 (~P2(x126061,f6(x126061,x126062))),
% 58.79/58.80 inference(rename_variables,[],[6433])).
% 58.79/58.80 cnf(12608,plain,
% 58.79/58.80 (P4(f6(a3,x126081),f6(a4,x126082))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,68,6433,12606,12,12586,19,34,30,33,31])).
% 58.79/58.80 cnf(12609,plain,
% 58.79/58.80 (~P2(x126091,f6(x126091,x126092))),
% 58.79/58.80 inference(rename_variables,[],[6433])).
% 58.79/58.80 cnf(12611,plain,
% 58.79/58.80 (~P8(f7(x126111,x126112),f6(x126111,x126113))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,68,6433,12606,11,12,12586,19,34,30,33,31,42])).
% 58.79/58.80 cnf(12612,plain,
% 58.79/58.80 (~P2(f6(x126121,x126122),x126121)),
% 58.79/58.80 inference(rename_variables,[],[11])).
% 58.79/58.80 cnf(12613,plain,
% 58.79/58.80 (~P8(f7(x126131,x126132),x126131)),
% 58.79/58.80 inference(rename_variables,[],[12])).
% 58.79/58.80 cnf(12615,plain,
% 58.79/58.80 (~P8(a3,f6(a4,x126151))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43])).
% 58.79/58.80 cnf(12618,plain,
% 58.79/58.80 (~P4(a4,f7(a3,a1))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43,9116])).
% 58.79/58.80 cnf(12620,plain,
% 58.79/58.80 (P4(a3,f7(a3,a1))),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43,9116,9240])).
% 58.79/58.80 cnf(12622,plain,
% 58.79/58.80 (~P2(f7(a3,x126221),a4)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43,9116,9240,126])).
% 58.79/58.80 cnf(12623,plain,
% 58.79/58.80 (~P2(f7(a4,x126231),a3)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43,9116,9240,126,7203])).
% 58.79/58.80 cnf(12624,plain,
% 58.79/58.80 (~P4(f7(a4,x126241),a3)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12,12586,19,34,30,33,31,42,43,9116,9240,126,7203,7408])).
% 58.79/58.80 cnf(12633,plain,
% 58.79/58.80 (~P8(f6(a3,x126331),a4)+~P2(f6(a3,x126331),a4)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,6433,12606,12609,11,12612,12,12586,19,34,30,33,31,42,43,9116,9240,126,7203,7408,25,17,24,20,39])).
% 58.79/58.80 cnf(12636,plain,
% 58.79/58.80 (~P8(a3,a4)),
% 58.79/58.80 inference(scs_inference,[],[12568,12559,12600,12561,6436,7128,68,2,6433,12606,12609,11,12612,12,12613,12586,19,34,30,33,31,42,43,9116,9240,126,7203,7408,25,17,24,20,39,41])).
% 58.79/58.80 cnf(12644,plain,
% 58.79/58.80 (~P4(a3,f7(a4,a1))),
% 58.79/58.80 inference(scs_inference,[],[12636,274])).
% 58.79/58.80 cnf(12646,plain,
% 58.79/58.80 (P4(a4,f7(a4,a1))),
% 58.79/58.80 inference(scs_inference,[],[12636,274,999])).
% 58.79/58.80 cnf(12655,plain,
% 58.79/58.80 (P4(f6(a3,x126551),a4)),
% 58.79/58.80 inference(scs_inference,[],[12595,12636,12605,12620,12622,12559,274,999,19,24,34,31])).
% 58.79/58.80 cnf(12656,plain,
% 58.79/58.80 (~P2(f7(a3,x126561),a4)),
% 58.79/58.80 inference(rename_variables,[],[12622])).
% 58.79/58.80 cnf(12659,plain,
% 58.79/58.80 (~P8(a4,f6(a3,x126591))),
% 58.79/58.80 inference(scs_inference,[],[12595,12636,12605,12620,12622,12559,6436,11,274,999,19,24,34,31,42])).
% 58.79/58.80 cnf(12663,plain,
% 58.79/58.80 (P4(f6(a3,x126631),f7(a3,a1))),
% 58.79/58.80 inference(scs_inference,[],[12595,12636,12605,12620,12618,12622,12559,6436,11,274,999,19,24,34,31,42,30])).
% 58.79/58.80 cnf(12665,plain,
% 58.79/58.80 (~P2(a4,f7(a3,x126651))),
% 58.79/58.80 inference(scs_inference,[],[12595,12636,12605,12620,12618,12622,12656,12559,6436,11,7,274,999,19,24,34,31,42,30,40])).
% 58.79/58.80 cnf(12674,plain,
% 58.79/58.80 (~P4(a4,f7(a3,x126741))),
% 58.79/58.80 inference(scs_inference,[],[12595,12636,12605,12611,12620,12618,12622,12656,12559,6436,11,121,7,274,999,19,24,34,31,42,30,40,39,17,20])).
% 58.79/58.80 cnf(12683,plain,
% 58.79/58.80 (P4(f6(a4,x126831),f7(a4,a1))),
% 58.79/58.80 inference(scs_inference,[],[12663,12644,12602,12659,19,24,30])).
% 58.79/58.80 cnf(12685,plain,
% 58.79/58.80 (P2(f7(a4,x126851),f7(a3,x126852))),
% 58.79/58.80 inference(scs_inference,[],[12663,12644,12602,12659,12665,12559,19,24,30,33])).
% 58.79/58.80 cnf(12690,plain,
% 58.79/58.80 (~P8(f7(a4,x126901),f7(a3,x126902))),
% 58.79/58.80 inference(scs_inference,[],[12663,12644,12602,12659,12665,12622,12559,6436,12,19,24,30,33,31,42])).
% 58.79/58.80 cnf(12695,plain,
% 58.79/58.80 (P8(a3,f7(a4,x126951))),
% 58.79/58.80 inference(scs_inference,[],[12663,12644,12602,12659,12665,12615,12605,12622,12559,6436,12,19,24,30,33,31,42,25,34])).
% 58.79/58.80 cnf(12713,plain,
% 58.79/58.80 (P4(f7(a3,x127131),a3)),
% 58.79/58.80 inference(scs_inference,[],[12646,12685,12690,12674,12623,84,19,24,30,31])).
% 58.79/58.80 cnf(12730,plain,
% 58.79/58.80 (P4(f7(a3,x127301),f7(a4,a1))),
% 58.79/58.80 inference(scs_inference,[],[12683,12713,12644,12615,12665,2,19,24,33,30])).
% 58.79/58.80 cnf(12732,plain,
% 58.79/58.80 (P4(f7(a3,x127321),f6(a3,x127322))),
% 58.79/58.80 inference(scs_inference,[],[12683,12713,12644,12615,12665,2,6433,19,24,33,30,31])).
% 58.79/58.80 cnf(12733,plain,
% 58.79/58.80 (~P2(x127331,f6(x127331,x127332))),
% 58.79/58.80 inference(rename_variables,[],[6433])).
% 58.79/58.80 cnf(12735,plain,
% 58.79/58.80 (~P8(a3,f7(a3,x127351))),
% 58.79/58.80 inference(scs_inference,[],[12683,12713,12644,12615,12611,12665,2,6433,12733,19,24,33,30,31,39])).
% 58.79/58.80 cnf(12741,plain,
% 58.79/58.80 (~P8(f7(a3,x127411),f7(a4,x127412))+~P2(f7(a3,x127411),f7(a4,x127412))),
% 58.79/58.80 inference(scs_inference,[],[12683,12713,12644,12690,12615,12611,12665,2,6433,12733,7,19,24,33,30,31,39,25,43])).
% 58.79/58.80 cnf(12754,plain,
% 58.79/58.80 (~P2(f6(a3,x127541),f7(a4,x127542))),
% 58.79/58.80 inference(scs_inference,[],[12730,12624,12735,11,19,24,31])).
% 58.79/58.80 cnf(12761,plain,
% 58.79/58.80 (~P4(f6(a3,x127611),f7(a4,x127612))),
% 58.79/58.80 inference(scs_inference,[],[12730,12624,12735,11,19,24,31,7189,17,20])).
% 58.79/58.80 cnf(12763,plain,
% 58.79/58.80 (P2(f7(a3,x127631),f7(a4,x127632))),
% 58.79/58.80 inference(scs_inference,[],[12730,12624,12735,12605,11,19,24,31,7189,17,20,33])).
% 58.79/58.80 cnf(12772,plain,
% 58.79/58.80 (~P8(f7(a3,x127721),f7(a4,x127722))),
% 58.79/58.80 inference(scs_inference,[],[12763,12741])).
% 58.79/58.80 cnf(12778,plain,
% 58.79/58.80 (P4(f7(a3,x127781),f7(a4,x127782))),
% 58.79/58.80 inference(scs_inference,[],[12608,12732,12761,12763,12611,12741,19,24,30])).
% 58.79/58.80 cnf(12784,plain,
% 58.79/58.80 (P4(f7(a4,x127841),a4)),
% 58.79/58.80 inference(scs_inference,[],[12608,12732,12754,12761,12763,12622,12611,6436,12741,19,24,30,33,31])).
% 58.79/58.80 cnf(12787,plain,
% 58.79/58.80 (~P8(a4,f7(a4,x127871))),
% 58.79/58.80 inference(scs_inference,[],[12608,12732,12754,12761,12763,12690,12622,12611,12665,6436,12741,19,24,30,33,31,39])).
% 58.79/58.80 cnf(12798,plain,
% 58.79/58.80 (~P4(a3,f7(a4,x127981))),
% 58.79/58.80 inference(scs_inference,[],[12608,12732,12754,12761,12763,12695,12690,12622,12611,12665,6436,11,12741,19,24,30,33,31,39,40,25,17,20])).
% 58.79/58.80 cnf(12806,plain,
% 58.79/58.80 (~P8(f6(a3,x128061),a4)),
% 58.79/58.80 inference(scs_inference,[],[12655,12633,20])).
% 58.79/58.80 cnf(12816,plain,
% 58.79/58.80 (P2(f6(a3,x128161),a4)),
% 58.79/58.80 inference(scs_inference,[],[12806,1539,2286,2371,6699,16])).
% 58.79/58.80 cnf(12827,plain,
% 58.79/58.80 (P4(f6(a4,x128271),f7(a4,x128272))),
% 58.79/58.80 inference(scs_inference,[],[12772,12778,12798,12806,12602,12559,1539,2286,2371,6699,16,25,19,24,34,30])).
% 58.79/58.80 cnf(12832,plain,
% 58.79/58.80 (P2(f6(a3,x128321),f7(a3,x128322))),
% 58.79/58.80 inference(scs_inference,[],[12772,12778,12798,12806,12602,12754,12559,12665,1539,2286,2371,6699,16,25,19,24,34,30,31,33])).
% 58.79/58.80 cnf(12834,plain,
% 58.79/58.80 (~P8(f6(a3,x128341),f7(a3,x128342))),
% 58.79/58.80 inference(scs_inference,[],[12772,12778,12798,12806,12602,12659,12754,12559,12665,1539,2286,2371,6699,16,25,19,24,34,30,31,33,43])).
% 58.79/58.80 cnf(12836,plain,
% 58.79/58.80 (P3(x128361,f6(a4,x128362))+P8(f6(a4,x128362),f7(a3,x128363))),
% 58.79/58.80 inference(scs_inference,[],[12772,12778,12798,12806,12602,12735,12659,12568,12754,12559,12665,1539,2286,2371,6699,16,25,19,24,34,30,31,33,43,46])).
% 58.79/58.80 cnf(12845,plain,
% 58.79/58.80 (P4(f7(a4,x128451),f7(a3,x128452))),
% 58.79/58.80 inference(scs_inference,[],[12827,12832,12834,12784,12674,25,19,24,30])).
% 58.79/58.80 cnf(12848,plain,
% 58.79/58.80 (~P3(x128481,x128482)),
% 58.79/58.80 inference(rename_variables,[],[12568])).
% 58.79/58.80 cnf(12851,plain,
% 58.79/58.80 (P3(a1,f7(a4,x128511))+P3(a2,f7(a4,x128511))+P3(a1,f6(a4,x128512))),
% 58.79/58.80 inference(scs_inference,[],[1,12827,12832,12834,12784,12674,12568,12848,25,19,24,30,12836,51])).
% 58.79/58.80 cnf(12857,plain,
% 58.79/58.80 (~P2(x128571,f6(x128571,x128572))),
% 58.79/58.80 inference(rename_variables,[],[6433])).
% 58.79/58.80 cnf(12864,plain,
% 58.79/58.80 (P3(a2,f7(a4,x128641))+P3(a1,f7(a4,x128641))),
% 58.79/58.80 inference(scs_inference,[],[12845,12787,12816,12615,12568,6433,12857,19,24,33,41,25,12851])).
% 58.79/58.80 cnf(12866,plain,
% 58.79/58.80 (P3(a1,f7(a4,x128661))),
% 58.79/58.80 inference(scs_inference,[],[12568,12864])).
% 58.79/58.80 cnf(12872,plain,
% 58.79/58.80 ($false),
% 58.79/58.80 inference(scs_inference,[],[12866,12568]),
% 58.79/58.80 ['proof']).
% 58.79/58.80 % SZS output end Proof
% 58.79/58.80 % Total time :58.130000s
%------------------------------------------------------------------------------