%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO217+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 : n024.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:39 EDT 2024
% Result : Theorem 58.87s 58.99s
% Output : CNFRefutation 58.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : GEO217+3 : TPTP v8.2.0. Released v4.0.0.
% 0.13/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n024.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 08:59:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.52/0.61 start to proof:theBenchmark
% 58.87/58.97 %-------------------------------------------
% 58.87/58.97 % File :CSE---1.7
% 58.87/58.97 % Problem :theBenchmark
% 58.87/58.97 % Transform :cnf
% 58.87/58.97 % Format :tptp:raw
% 58.87/58.97 % Command :java -jar mcs_scs.jar %d %s
% 58.87/58.97
% 58.87/58.97 % Result :Theorem 58.230000s
% 58.87/58.97 % Output :CNFRefutation 58.230000s
% 58.87/58.97 %-------------------------------------------
% 58.87/58.99 %------------------------------------------------------------------------------
% 58.87/58.99 % File : GEO217+3 : TPTP v8.2.0. Released v4.0.0.
% 58.87/58.99 % Domain : Geometry (Constructive)
% 58.87/58.99 % Problem : Transitivity of parallel
% 58.87/58.99 % Version : [vPl95] axioms.
% 58.87/58.99 % English : If a line L is parallel to the lines M and N, then M and N
% 58.87/58.99 % are parallel.
% 58.87/58.99
% 58.87/58.99 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 58.87/58.99 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.87/58.99 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.87/58.99 % Source : [Rat07]
% 58.87/58.99 % Names : Theorem 8.7.i [vPl95]
% 58.87/58.99
% 58.87/58.99 % Status : Theorem
% 58.87/58.99 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.14 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v4.0.0
% 58.87/58.99 % Syntax : Number of formulae : 36 ( 7 unt; 0 def)
% 58.87/58.99 % Number of atoms : 96 ( 0 equ)
% 58.87/58.99 % Maximal formula atoms : 6 ( 2 avg)
% 58.87/58.99 % Number of connectives : 88 ( 28 ~; 19 |; 14 &)
% 58.87/58.99 % ( 5 <=>; 22 =>; 0 <=; 0 <~>)
% 58.87/58.99 % Maximal formula depth : 9 ( 5 avg)
% 58.87/58.99 % Maximal term depth : 2 ( 1 avg)
% 58.87/58.99 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 58.87/58.99 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 58.87/58.99 % Number of variables : 84 ( 84 !; 0 ?)
% 58.87/58.99 % SPC : FOF_THM_RFO_NEQ
% 58.87/58.99
% 58.87/58.99 % Comments :
% 58.87/58.99 %------------------------------------------------------------------------------
% 58.87/58.99 include('Axioms/GEO006+0.ax').
% 58.87/58.99 include('Axioms/GEO006+1.ax').
% 58.87/58.99 include('Axioms/GEO006+2.ax').
% 58.87/58.99 include('Axioms/GEO006+3.ax').
% 58.87/58.99 include('Axioms/GEO006+4.ax').
% 58.87/58.99 include('Axioms/GEO006+5.ax').
% 58.87/58.99 include('Axioms/GEO006+6.ax').
% 58.87/58.99 %------------------------------------------------------------------------------
% 58.87/58.99 fof(con,conjecture,
% 58.87/58.99 ! [L,M,N] :
% 58.87/58.99 ( ( parallel_lines(L,M)
% 58.87/58.99 & parallel_lines(L,N) )
% 58.87/58.99 => parallel_lines(M,N) ) ).
% 58.87/58.99
% 58.87/58.99 %------------------------------------------------------------------------------
% 58.87/58.99 %-------------------------------------------
% 58.87/58.99 % Proof found
% 58.87/58.99 % SZS status Theorem for theBenchmark
% 58.87/58.99 % SZS output start Proof
% 58.87/59.01 %ClaNum:49(EqnAxiom:0)
% 58.87/59.01 %VarNum:218(SingletonVarNum:98)
% 58.87/59.01 %MaxLitNum:6
% 58.87/59.01 %MaxfuncDepth:1
% 58.87/59.01 %SharedTerms:6
% 58.87/59.01 %goalClause: 1 2 3
% 58.87/59.01 %singleGoalClaCount:3
% 58.87/59.01 [1]P1(a1,a2)
% 58.87/59.01 [2]P1(a1,a3)
% 58.87/59.01 [3]~P1(a2,a3)
% 58.87/59.01 [4]~P2(x41,x41)
% 58.87/59.01 [5]~P3(x51,x51)
% 58.87/59.01 [6]~P4(x61,x61)
% 58.87/59.01 [7]~P5(x71,f4(x72,x71))
% 58.87/59.01 [8]~P5(x81,f5(x82,x81))
% 58.87/59.01 [9]~P4(f4(x91,x92),x91)
% 58.87/59.01 [10]~P11(f5(x101,x102),x101)
% 58.87/59.01 [11]P6(x111,x112)+P2(x111,x112)
% 58.87/59.01 [12]P7(x121,x122)+P3(x121,x122)
% 58.87/59.01 [14]P11(x141,x142)+P4(x141,x142)
% 58.87/59.01 [15]P1(x151,x152)+P4(x151,x152)
% 58.87/59.01 [16]P8(x161,x162)+P5(x161,x162)
% 58.87/59.01 [17]P9(x171,x172)+P11(x171,x172)
% 58.87/59.01 [18]~P3(x181,x182)+P4(x181,x182)
% 58.87/59.01 [21]~P6(x211,x212)+~P2(x211,x212)
% 58.87/59.01 [22]~P7(x221,x222)+~P3(x221,x222)
% 58.87/59.01 [23]~P1(x231,x232)+~P4(x231,x232)
% 58.87/59.01 [24]~P8(x241,x242)+~P5(x241,x242)
% 58.92/59.01 [25]~P9(x251,x252)+~P11(x251,x252)
% 58.92/59.01 [45]~P2(x451,x452)+~P5(x452,f7(x451,x452))
% 58.92/59.01 [46]~P2(x461,x462)+~P5(x461,f7(x461,x462))
% 58.92/59.01 [47]~P4(x471,x472)+~P5(f6(x471,x472),x472)
% 58.92/59.01 [48]~P4(x481,x482)+~P5(f6(x481,x482),x481)
% 58.92/59.01 [19]~P12(x192)+~P10(x191)+P10(f4(x191,x192))
% 58.92/59.01 [20]~P12(x202)+~P10(x201)+P10(f5(x201,x202))
% 58.92/59.01 [26]~P2(x263,x261)+P2(x261,x262)+P2(x263,x262)
% 58.92/59.01 [27]~P5(x271,x273)+P2(x271,x272)+P5(x272,x273)
% 58.92/59.01 [28]~P3(x283,x281)+P3(x281,x282)+P3(x283,x282)
% 58.92/59.01 [29]~P4(x293,x291)+P3(x291,x292)+P4(x293,x292)
% 58.92/59.01 [30]~P5(x303,x301)+P3(x301,x302)+P5(x303,x302)
% 58.92/59.01 [31]~P4(x313,x311)+P4(x311,x312)+P4(x313,x312)
% 58.92/59.01 [32]~P4(x323,x322)+P11(x321,x322)+P11(x321,x323)
% 58.92/59.01 [34]~P10(x342)+~P10(x341)+~P4(x341,x342)+P12(f6(x341,x342))
% 58.92/59.01 [35]~P12(x352)+~P12(x351)+~P2(x351,x352)+P10(f7(x351,x352))
% 58.92/59.01 [37]~P4(x371,x373)+~P11(x371,x373)+P4(x371,x372)+P11(x373,x372)
% 58.92/59.01 [38]~P4(x382,x383)+~P11(x382,x383)+P4(x381,x382)+P4(x381,x383)
% 58.92/59.01 [39]~P4(x392,x393)+~P11(x392,x393)+P4(x391,x392)+P11(x391,x393)
% 58.92/59.01 [40]~P4(x403,x401)+~P11(x403,x401)+P4(x401,x402)+P11(x403,x402)
% 58.92/59.01 [41]~P4(x413,x412)+~P11(x413,x412)+P4(x411,x412)+P11(x411,x413)
% 58.92/59.01 [42]~P4(x421,x423)+~P11(x421,x423)+P11(x421,x422)+P11(x423,x422)
% 58.92/59.01 [44]P11(x443,x444)+~P3(x443,x442)+P5(x441,x442)+P5(x441,x443)+P11(x442,x444)
% 58.92/59.01 [49]P5(x494,x493)+~P2(x494,x491)+~P3(x493,x492)+P5(x491,x492)+P5(x491,x493)+P5(x494,x492)
% 58.92/59.01 %EqnAxiom
% 58.92/59.01
% 58.92/59.01 %-------------------------------------------
% 58.92/59.03 cnf(54,plain,
% 58.92/59.03 (~P3(f4(x541,x542),x541)),
% 58.92/59.03 inference(scs_inference,[],[6,9,14,15,18])).
% 58.92/59.03 cnf(82,plain,
% 58.92/59.03 (~P4(f4(x821,x822),f4(x821,x823))),
% 58.92/59.03 inference(scs_inference,[],[9,54,8,16,14,25,15,12,29])).
% 58.92/59.03 cnf(83,plain,
% 58.92/59.03 (~P4(f4(x831,x832),x831)),
% 58.92/59.03 inference(rename_variables,[],[9])).
% 58.92/59.03 cnf(85,plain,
% 58.92/59.03 (~P4(x851,f4(x851,x852))),
% 58.92/59.03 inference(scs_inference,[],[9,83,6,54,8,16,14,25,15,12,29,31])).
% 58.92/59.03 cnf(88,plain,
% 58.92/59.03 (~P3(x881,f4(x881,x882))),
% 58.92/59.03 inference(scs_inference,[],[9,83,6,54,5,8,16,14,25,15,12,29,31,28])).
% 58.92/59.03 cnf(91,plain,
% 58.92/59.03 (~P5(x911,f4(f5(x912,x911),x913))),
% 58.92/59.03 inference(scs_inference,[],[9,83,6,54,5,8,16,14,25,15,12,29,31,28,30])).
% 58.92/59.03 cnf(96,plain,
% 58.92/59.03 (~P3(f4(x961,x962),f4(x961,x963))),
% 58.92/59.03 inference(scs_inference,[],[82,91,16,18])).
% 58.92/59.03 cnf(107,plain,
% 58.92/59.03 (~P3(f4(x1071,x1072),x1071)),
% 58.92/59.03 inference(rename_variables,[],[54])).
% 58.92/59.03 cnf(109,plain,
% 58.92/59.03 (~P4(x1091,f4(f4(x1091,x1092),x1093))),
% 58.92/59.03 inference(scs_inference,[],[85,82,54,107,88,91,16,18,14,12,25,15,28,29])).
% 58.92/59.03 cnf(110,plain,
% 58.92/59.03 (~P3(f4(x1101,x1102),x1101)),
% 58.92/59.03 inference(rename_variables,[],[54])).
% 58.92/59.03 cnf(112,plain,
% 58.92/59.03 (~P5(x1121,f4(f4(x1122,x1121),x1123))),
% 58.92/59.03 inference(scs_inference,[],[85,82,54,107,110,88,91,7,16,18,14,12,25,15,28,29,30])).
% 58.92/59.03 cnf(132,plain,
% 58.92/59.03 (~P3(f4(f4(x1321,x1322),x1323),f4(x1321,x1324))),
% 58.92/59.03 inference(scs_inference,[],[9,82,96,54,112,16,14,12,15,29,28])).
% 58.92/59.03 cnf(135,plain,
% 58.92/59.03 (~P5(x1351,f4(x1352,x1353))),
% 58.92/59.03 inference(scs_inference,[],[9,82,96,54,112,7,16,14,12,15,29,28,30])).
% 58.92/59.03 cnf(155,plain,
% 58.92/59.03 (P11(f4(x1551,x1552),x1553)+~P3(f4(x1551,x1552),f5(x1553,x1554))),
% 58.92/59.03 inference(scs_inference,[],[109,10,132,135,8,16,14,12,15,25,44])).
% 58.92/59.03 cnf(296,plain,
% 58.92/59.03 (P11(a1,a2)),
% 58.92/59.03 inference(scs_inference,[],[1,23,14])).
% 58.92/59.03 cnf(612,plain,
% 58.92/59.03 (~P5(f6(a2,a3),a2)),
% 58.92/59.03 inference(scs_inference,[],[3,48,15])).
% 58.92/59.03 cnf(615,plain,
% 58.92/59.03 (P11(a2,x6151)+~P3(a2,f5(x6151,f6(a2,a3)))),
% 58.92/59.03 inference(scs_inference,[],[10,612,8,16,44])).
% 58.92/59.03 cnf(619,plain,
% 58.92/59.03 (~P9(a2,x6191)+~P3(a2,f5(x6191,f6(a2,a3)))),
% 58.92/59.03 inference(scs_inference,[],[10,612,8,16,44,25])).
% 58.92/59.03 cnf(719,plain,
% 58.92/59.03 (P11(a2,x7191)+~P4(a1,a2)+P11(a1,x7191)),
% 58.92/59.03 inference(scs_inference,[],[296,42])).
% 58.92/59.03 cnf(1639,plain,
% 58.92/59.03 (~P4(a2,f5(a2,x16391))+~P3(a2,f5(f5(a2,x16391),f6(a2,a3)))),
% 58.92/59.03 inference(scs_inference,[],[10,6,615,37])).
% 58.92/59.03 cnf(1667,plain,
% 58.92/59.03 (~P4(f5(x16671,f6(a2,a3)),a2)+~P9(a2,x16671)),
% 58.92/59.03 inference(scs_inference,[],[6,619,29])).
% 58.92/59.03 cnf(1749,plain,
% 58.92/59.03 (P11(a2,x17491)+~P4(f5(x17491,f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[1667,17])).
% 58.92/59.03 cnf(1781,plain,
% 58.92/59.03 (~P4(a2,f5(a2,x17811))+~P4(f5(f5(a2,x17811),f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[10,6,1749,41])).
% 58.92/59.03 cnf(1797,plain,
% 58.92/59.03 (~P3(f4(x17971,x17972),f5(x17973,x17974))+~P9(f4(x17971,x17972),x17973)),
% 58.92/59.03 inference(scs_inference,[],[155,25])).
% 58.92/59.03 cnf(2665,plain,
% 58.92/59.03 (P11(a2,x26651)+~P3(f5(x26651,f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[612,10,8,44])).
% 58.92/59.03 cnf(2669,plain,
% 58.92/59.03 (~P9(a2,x26691)+~P3(f5(x26691,f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[612,10,8,44,25])).
% 58.92/59.03 cnf(2695,plain,
% 58.92/59.03 (~P4(a2,f5(a2,x26951))+~P3(f5(f5(a2,x26951),f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[10,6,2665,37])).
% 58.92/59.03 cnf(2726,plain,
% 58.92/59.03 (P7(f5(x27261,f6(a2,a3)),a2)+~P9(a2,x27261)),
% 58.92/59.03 inference(scs_inference,[],[2669,12])).
% 58.92/59.03 cnf(2757,plain,
% 58.92/59.03 (P11(a2,x27571)+P7(f5(x27571,f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[2726,17])).
% 58.92/59.03 cnf(2788,plain,
% 58.92/59.03 (~P4(a2,f5(a2,x27881))+P7(f5(f5(a2,x27881),f6(a2,a3)),a2)),
% 58.92/59.03 inference(scs_inference,[],[10,6,2757,41])).
% 58.92/59.04 cnf(3662,plain,
% 58.92/59.04 (P3(x36621,f5(x36621,x36622))),
% 58.92/59.04 inference(scs_inference,[],[10,6,14,29])).
% 58.92/59.04 cnf(3770,plain,
% 58.92/59.04 (P4(x37701,f5(x37701,x37702))),
% 58.92/59.04 inference(scs_inference,[],[10,6,14,31])).
% 58.92/59.04 cnf(3774,plain,
% 58.92/59.04 (P4(x37741,f5(x37741,x37742))),
% 58.92/59.04 inference(rename_variables,[],[3770])).
% 58.92/59.04 cnf(3777,plain,
% 58.92/59.04 (P4(x37771,f5(x37771,x37772))),
% 58.92/59.04 inference(rename_variables,[],[3770])).
% 58.92/59.04 cnf(3780,plain,
% 58.92/59.04 (P4(x37801,f5(x37801,x37802))),
% 58.92/59.04 inference(rename_variables,[],[3770])).
% 58.92/59.04 cnf(3783,plain,
% 58.92/59.04 (P4(x37831,f5(x37831,x37832))),
% 58.92/59.04 inference(rename_variables,[],[3770])).
% 58.92/59.04 cnf(3791,plain,
% 58.92/59.04 (P11(f5(x37911,x37912),f5(x37911,x37913))),
% 58.92/59.04 inference(scs_inference,[],[10,3770,3774,3777,3780,3783,23,1639,1781,2695,2788,12,14,15,32])).
% 58.92/59.04 cnf(3794,plain,
% 58.92/59.04 (P4(f5(f4(x37941,x37942),x37943),f4(x37941,x37944))),
% 58.92/59.04 inference(scs_inference,[],[82,10,3770,3774,3777,3780,3783,23,1639,1781,2695,2788,12,14,15,32,31])).
% 58.92/59.04 cnf(3797,plain,
% 58.92/59.04 (~P4(f5(f5(a2,x37971),f6(a2,a3)),f4(a2,x37972))),
% 58.92/59.04 inference(scs_inference,[],[82,54,10,3770,3774,3777,3780,3783,23,1639,1781,2695,2788,12,14,15,32,31,29])).
% 58.92/59.04 cnf(3802,plain,
% 58.92/59.04 (~P3(f5(f5(a2,x38021),f6(a2,a3)),f4(a2,x38022))),
% 58.92/59.04 inference(scs_inference,[],[82,54,10,3770,3774,3777,3780,3783,23,1639,1781,2695,2788,12,14,15,32,31,29,25,18])).
% 58.92/59.04 cnf(3818,plain,
% 58.92/59.04 (P11(f5(f5(a2,x38181),f6(a2,a3)),f4(a2,x38182))),
% 58.92/59.04 inference(scs_inference,[],[3791,3794,3797,3802,23,12,25,14])).
% 58.92/59.04 cnf(3822,plain,
% 58.92/59.04 (P4(f4(x38221,x38222),f5(f4(x38221,x38223),x38224))),
% 58.92/59.04 inference(scs_inference,[],[6,3791,3794,3797,3802,23,12,25,14,15,31])).
% 58.92/59.04 cnf(3841,plain,
% 58.92/59.04 (P4(f5(f4(x38411,x38412),x38413),x38411)),
% 58.92/59.04 inference(scs_inference,[],[3818,9,3822,23,25,31])).
% 58.92/59.04 cnf(3857,plain,
% 58.92/59.04 (P4(x38571,f5(f4(x38571,x38572),x38573))),
% 58.92/59.04 inference(scs_inference,[],[6,3841,23,31])).
% 58.92/59.04 cnf(7002,plain,
% 58.92/59.04 (~P11(f4(x70021,x70022),f5(f4(x70021,x70023),x70024))),
% 58.92/59.04 inference(scs_inference,[],[82,10,3822,37])).
% 58.92/59.04 cnf(7019,plain,
% 58.92/59.04 (~P11(f5(f4(x70191,x70192),x70193),f4(x70191,x70194))),
% 58.92/59.04 inference(scs_inference,[],[6,3794,7002,37])).
% 58.92/59.04 cnf(7027,plain,
% 58.92/59.04 (~P11(x70271,f5(f4(x70271,x70272),x70273))),
% 58.92/59.04 inference(scs_inference,[],[85,10,3857,7019,17,37])).
% 58.92/59.04 cnf(7082,plain,
% 58.92/59.04 (~P11(f5(f4(x70821,x70822),x70823),x70821)),
% 58.92/59.04 inference(scs_inference,[],[6,3841,7027,37])).
% 58.92/59.04 cnf(7144,plain,
% 58.92/59.04 (P4(f5(x71441,x71442),x71441)),
% 58.92/59.04 inference(scs_inference,[],[3770,6,7082,32,31])).
% 58.92/59.04 cnf(7156,plain,
% 58.92/59.04 (P4(f5(x71561,x71562),f4(x71561,x71563))),
% 58.92/59.04 inference(scs_inference,[],[3770,85,31])).
% 58.92/59.04 cnf(7237,plain,
% 58.92/59.04 (P11(f5(x72371,x72372),f5(f4(x72371,x72373),x72374))),
% 58.92/59.04 inference(scs_inference,[],[3857,10,32])).
% 58.92/59.04 cnf(7296,plain,
% 58.92/59.04 (~P4(f5(x72961,x72962),f5(f4(x72961,x72963),x72964))),
% 58.92/59.04 inference(scs_inference,[],[7082,7237,10,42])).
% 58.92/59.04 cnf(7302,plain,
% 58.92/59.04 (~P3(f5(x73021,x73022),f5(f4(x73021,x73023),x73024))),
% 58.92/59.04 inference(scs_inference,[],[7082,7237,10,42,15,18])).
% 58.92/59.04 cnf(7378,plain,
% 58.92/59.04 (P4(f4(x73781,x73782),f5(x73781,x73783))),
% 58.92/59.04 inference(scs_inference,[],[7156,6,10,32,31])).
% 58.92/59.04 cnf(7430,plain,
% 58.92/59.04 (~P3(f5(f4(x74301,x74302),x74303),f5(x74301,x74304))),
% 58.92/59.04 inference(scs_inference,[],[7302,5,28])).
% 58.92/59.04 cnf(7433,plain,
% 58.92/59.04 (~P4(f5(f4(x74331,x74332),x74333),f5(x74331,x74334))),
% 58.92/59.04 inference(scs_inference,[],[7302,6,5,28,29])).
% 58.92/59.04 cnf(7441,plain,
% 58.92/59.04 (~P4(f5(x74411,x74412),f5(x74411,x74413))),
% 58.92/59.04 inference(scs_inference,[],[7302,7296,7433,7430,12,15,29])).
% 58.92/59.04 cnf(7444,plain,
% 58.92/59.04 (~P3(f5(x74441,x74442),f5(x74441,x74443))),
% 58.92/59.04 inference(scs_inference,[],[7302,7296,7433,7430,12,15,29,18])).
% 58.92/59.04 cnf(7607,plain,
% 58.92/59.04 (P3(x76071,f5(f4(x76071,x76072),x76073))),
% 58.92/59.04 inference(scs_inference,[],[7144,7296,29])).
% 58.92/59.04 cnf(7630,plain,
% 58.92/59.04 (~P11(f4(x76301,x76302),f5(x76301,x76303))),
% 58.92/59.04 inference(scs_inference,[],[10,9,7378,37])).
% 58.92/59.04 cnf(7747,plain,
% 58.92/59.04 (~P11(f5(x77471,x77472),f4(x77471,x77473))),
% 58.92/59.04 inference(scs_inference,[],[7002,7156,7296,37])).
% 58.92/59.04 cnf(7810,plain,
% 58.92/59.04 (~P11(x78101,f5(x78101,x78102))),
% 58.92/59.04 inference(scs_inference,[],[3662,7027,7296,18,40])).
% 58.92/59.04 cnf(7832,plain,
% 58.92/59.04 (P11(a1,a3)),
% 58.92/59.04 inference(scs_inference,[],[2,23,14])).
% 58.92/59.04 cnf(8151,plain,
% 58.92/59.04 (P3(f5(f4(a1,x81511),x81512),a3)+P4(a3,a1)),
% 58.92/59.04 inference(scs_inference,[],[6,7832,7027,7607,38,18,719,28])).
% 58.92/59.04 cnf(8170,plain,
% 58.92/59.04 (P4(a1,a3)+P3(f5(f4(a1,x81701),x81702),a3)),
% 58.92/59.04 inference(scs_inference,[],[6,8151,31])).
% 58.92/59.04 cnf(8173,plain,
% 58.92/59.04 (P3(f5(f4(a1,x81731),x81732),a3)),
% 58.92/59.04 inference(scs_inference,[],[2,8170,23])).
% 58.92/59.04 cnf(8562,plain,
% 58.92/59.04 (P3(a3,f5(f4(a1,x85621),x85622))),
% 58.92/59.04 inference(scs_inference,[],[8173,7444,28])).
% 58.92/59.04 cnf(8568,plain,
% 58.92/59.04 (P3(a3,f5(a1,x85681))),
% 58.92/59.04 inference(scs_inference,[],[8173,7430,28])).
% 58.92/59.04 cnf(8614,plain,
% 58.92/59.04 (P3(f5(f4(a1,x86141),x86142),f4(a3,x86143))),
% 58.92/59.04 inference(scs_inference,[],[8562,88,28])).
% 58.92/59.04 cnf(8632,plain,
% 58.92/59.04 (P3(f5(a1,x86321),f4(a3,x86322))),
% 58.92/59.04 inference(scs_inference,[],[8568,88,28])).
% 58.92/59.04 cnf(8652,plain,
% 58.92/59.04 (P3(f4(a3,x86521),f5(a1,x86522))),
% 58.92/59.04 inference(scs_inference,[],[8614,7430,28])).
% 58.92/59.04 cnf(8857,plain,
% 58.92/59.04 (~P4(a1,a3)),
% 58.92/59.04 inference(scs_inference,[],[2,8652,1797,155,23])).
% 58.92/59.04 cnf(8859,plain,
% 58.92/59.04 (P4(a2,a3)),
% 58.92/59.04 inference(scs_inference,[],[2,8652,3,1797,155,23,15])).
% 58.92/59.04 cnf(8863,plain,
% 58.92/59.04 (P4(f5(a1,x88631),a3)),
% 58.92/59.04 inference(scs_inference,[],[2,8652,3,7144,1797,155,23,15,18,31])).
% 58.92/59.04 cnf(8887,plain,
% 58.92/59.04 (~P4(a1,a2)),
% 58.92/59.04 inference(scs_inference,[],[1,23])).
% 58.92/59.04 cnf(8889,plain,
% 58.92/59.04 (P4(f5(a1,x88891),f4(a3,x88892))),
% 58.92/59.04 inference(scs_inference,[],[1,8632,23,18])).
% 58.92/59.04 cnf(8907,plain,
% 58.92/59.04 (P4(a3,f5(a1,x89071))),
% 58.92/59.04 inference(scs_inference,[],[8568,18])).
% 58.92/59.04 cnf(8912,plain,
% 58.92/59.04 (P4(f5(a1,x89121),a2)),
% 58.92/59.04 inference(scs_inference,[],[8887,8889,7747,8568,7144,18,32,31])).
% 58.92/59.04 cnf(8946,plain,
% 58.92/59.04 (~P11(f5(a1,x89461),a2)),
% 58.92/59.04 inference(scs_inference,[],[8912,8887,7810,10,32,41])).
% 58.92/59.04 cnf(8957,plain,
% 58.92/59.04 (~P11(a2,a3)),
% 58.92/59.04 inference(scs_inference,[],[8907,8859,8887,8857,7630,32,38])).
% 58.92/59.04 cnf(8972,plain,
% 58.92/59.04 (~P4(f5(x89721,x89722),f5(x89721,x89723))),
% 58.92/59.04 inference(rename_variables,[],[7441])).
% 58.92/59.04 cnf(8974,plain,
% 58.92/59.04 ($false),
% 58.92/59.04 inference(scs_inference,[],[8957,8946,8863,8912,7441,8972,32,41,31]),
% 58.92/59.04 ['proof']).
% 58.92/59.04 % SZS output end Proof
% 58.92/59.04 % Total time :58.230000s
%------------------------------------------------------------------------------