%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO268+3 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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:05:02 EDT 2024
% Result : Theorem 61.56s 61.83s
% Output : CNFRefutation 61.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO268+3 : TPTP v8.2.0. Released v4.0.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n024.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 09:36:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.56/0.58 start to proof:theBenchmark
% 61.56/61.81 %-------------------------------------------
% 61.56/61.81 % File :CSE---1.7
% 61.56/61.81 % Problem :theBenchmark
% 61.56/61.81 % Transform :cnf
% 61.56/61.81 % Format :tptp:raw
% 61.56/61.81 % Command :java -jar mcs_scs.jar %d %s
% 61.56/61.81
% 61.56/61.81 % Result :Theorem 60.960000s
% 61.56/61.81 % Output :CNFRefutation 60.960000s
% 61.56/61.81 %-------------------------------------------
% 61.56/61.83 %------------------------------------------------------------------------------
% 61.56/61.83 % File : GEO268+3 : TPTP v8.2.0. Released v4.0.0.
% 61.56/61.83 % Domain : Geometry (Constructive)
% 61.56/61.83 % Problem : Equivalence of unequally directed opposite and reversed lines
% 61.56/61.83 % Version : [vPl98] axioms.
% 61.56/61.83 % English :
% 61.56/61.83
% 61.56/61.83 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 61.56/61.83 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 61.56/61.83 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 61.56/61.83 % Source : [Rat07]
% 61.56/61.83 % Names : Theorem 3.12 [vPl98]
% 61.56/61.83
% 61.56/61.83 % Status : Theorem
% 61.56/61.83 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.09 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.07 v5.0.0, 0.00 v4.0.1, 0.05 v4.0.0
% 61.56/61.83 % Syntax : Number of formulae : 37 ( 6 unt; 0 def)
% 61.56/61.83 % Number of atoms : 111 ( 0 equ)
% 61.56/61.83 % Maximal formula atoms : 10 ( 3 avg)
% 61.56/61.83 % Number of connectives : 86 ( 12 ~; 22 |; 24 &)
% 61.56/61.83 % ( 11 <=>; 17 =>; 0 <=; 0 <~>)
% 61.56/61.83 % Maximal formula depth : 13 ( 5 avg)
% 61.56/61.83 % Maximal term depth : 3 ( 1 avg)
% 61.56/61.83 % Number of predicates : 18 ( 18 usr; 0 prp; 1-4 aty)
% 61.56/61.83 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 61.56/61.83 % Number of variables : 83 ( 83 !; 0 ?)
% 61.56/61.83 % SPC : FOF_THM_RFO_NEQ
% 61.56/61.83
% 61.56/61.83 % Comments :
% 61.56/61.83 %------------------------------------------------------------------------------
% 61.56/61.83 include('Axioms/GEO009+0.ax').
% 61.56/61.83 %------------------------------------------------------------------------------
% 61.56/61.83 fof(con,conjecture,
% 61.56/61.83 ! [L,M] :
% 61.56/61.83 ( unequally_directed_lines(L,M)
% 61.56/61.83 <=> unequally_directed_opposite_lines(L,reverse_line(M)) ) ).
% 61.56/61.83
% 61.56/61.83 %------------------------------------------------------------------------------
% 61.56/61.83 %-------------------------------------------
% 61.56/61.83 % Proof found
% 61.56/61.83 % SZS status Theorem for theBenchmark
% 61.56/61.83 % SZS output start Proof
% 61.56/61.85 %ClaNum:68(EqnAxiom:0)
% 61.56/61.85 %VarNum:311(SingletonVarNum:129)
% 61.56/61.85 %MaxLitNum:10
% 61.56/61.85 %MaxfuncDepth:2
% 61.56/61.85 %SharedTerms:7
% 61.56/61.85 %goalClause: 12 20
% 61.56/61.85 [1]P1(x11,x11)
% 61.56/61.85 [5]~P2(x51,x51)
% 61.56/61.85 [6]~P3(x61,x61)
% 61.56/61.85 [9]~P3(x91,f6(x91))
% 61.56/61.85 [3]~P9(x31,x32)
% 61.56/61.85 [4]~P12(x41,x42)
% 61.56/61.85 [2]P1(f1(x21,x22),x21)
% 61.56/61.85 [10]~P4(x101,f1(x102,x101))
% 61.56/61.85 [12]P14(a2,a3)+P18(a2,f6(a3))
% 61.56/61.85 [20]~P14(a2,a3)+~P18(a2,f6(a3))
% 61.56/61.85 [11]~P13(x111)+P13(f6(x111))
% 61.56/61.85 [13]P10(x131,x132)+P18(x131,x132)
% 61.56/61.85 [14]P1(x141,x142)+P14(x141,x142)
% 61.56/61.85 [16]~P5(x161,x162)+P18(x161,x162)
% 61.56/61.85 [17]~P5(x171,x172)+P14(x171,x172)
% 61.56/61.85 [18]~P15(x181,x182)+P4(x181,x182)
% 61.56/61.85 [25]~P10(x251,x252)+~P18(x251,x252)
% 61.56/61.85 [26]~P1(x261,x262)+~P14(x261,x262)
% 61.56/61.85 [15]P14(x151,x152)+P14(x151,f6(x152))
% 61.56/61.85 [21]~P18(x211,x212)+P14(x211,f6(x212))
% 61.56/61.85 [22]~P15(x221,x222)+P9(x221,f6(x222))
% 61.56/61.85 [23]~P17(x231,x232)+P12(x231,f6(x232))
% 61.56/61.85 [27]P18(x271,x272)+~P14(x271,f6(x272))
% 61.56/61.85 [40]~P2(x401,x402)+~P4(x402,f4(x401,x402))
% 61.56/61.85 [41]~P2(x411,x412)+~P4(x411,f4(x411,x412))
% 61.56/61.85 [59]~P2(x591,x592)+P1(f4(x591,x592),f6(f4(x592,x591)))
% 61.56/61.85 [50]P2(x501,x502)+~P6(x503,x501,x502)
% 61.56/61.85 [51]P11(x511,x512)+~P6(x512,x513,x511)
% 61.56/61.85 [52]P11(x521,x522)+~P6(x522,x521,x523)
% 61.56/61.85 [60]~P6(x601,x602,x603)+P1(x601,f4(x602,x603))
% 61.56/61.85 [32]P9(x321,x322)+~P4(x321,x322)+P15(x321,x322)
% 61.56/61.85 [36]~P18(x361,x362)+~P14(x361,x362)+P5(x361,x362)
% 61.56/61.85 [24]~P16(x242)+~P13(x241)+P13(f1(x241,x242))
% 61.56/61.85 [57]~P14(x571,x572)+~P14(x571,f6(x572))+~P4(f5(x571,x572),x572)
% 61.56/61.85 [58]~P14(x581,x582)+~P14(x581,f6(x582))+~P4(f5(x581,x582),x581)
% 61.56/61.85 [30]~P14(x303,x301)+P14(x301,x302)+P14(x303,x302)
% 61.56/61.85 [34]~P2(x343,x341)+P2(x341,x342)+P2(x343,x342)
% 61.56/61.85 [35]~P3(x353,x351)+P3(x351,x352)+P3(x353,x352)
% 61.56/61.85 [53]~P8(x532,x533,x531)+P15(x531,x532)+P15(x533,x532)
% 61.56/61.85 [54]P9(x541,x542)+P15(x541,x542)+~P8(x542,x543,x541)
% 61.56/61.85 [55]P9(x551,x552)+P15(x551,x552)+~P8(x552,x551,x553)
% 61.56/61.85 [56]~P8(x562,x561,x563)+P9(x561,x562)+P9(x563,x562)
% 61.56/61.85 [63]~P6(x631,x633,x632)+~P6(x631,x634,x633)+P7(x631,x632,x633,x634)
% 61.56/61.85 [64]~P6(x641,x643,x644)+~P6(x641,x642,x643)+P7(x641,x642,x643,x644)
% 61.56/61.85 [65]~P7(x651,x652,x653,x654)+P6(x651,x652,x653)+P6(x651,x654,x653)
% 61.56/61.85 [66]P6(x661,x663,x662)+P6(x661,x662,x663)+~P7(x661,x664,x662,x663)
% 61.56/61.85 [67]P6(x671,x673,x672)+P6(x671,x672,x673)+~P7(x671,x672,x673,x674)
% 61.56/61.85 [68]~P7(x681,x684,x682,x683)+P6(x681,x682,x683)+P6(x681,x682,x684)
% 61.56/61.85 [37]~P16(x372)+~P16(x371)+~P2(x371,x372)+P13(f4(x371,x372))
% 61.56/61.85 [44]~P14(x441,x442)+P12(x441,x442)+P12(x441,f6(x442))+~P14(x441,f6(x442))
% 61.56/61.85 [42]~P14(x421,x423)+P14(x421,x422)+~P14(x421,f6(x423))+P14(x423,f6(x422))
% 61.56/61.85 [43]~P14(x433,x431)+P14(x431,x432)+~P14(x433,f6(x431))+P14(x433,f6(x432))
% 61.56/61.85 [46]~P13(x462)+~P13(x461)+~P14(x461,x462)+~P14(x461,f6(x462))+P16(f5(x461,x462))
% 61.56/61.85 [62]~P2(x622,x623)+~P11(x623,x621)+~P11(x622,x621)+P6(x621,x622,x623)+~P1(x621,f4(x622,x623))
% 61.56/61.85 [61]P9(x614,x613)+~P2(x614,x611)+~P3(x613,x612)+P9(x611,x612)+P9(x611,x613)+P9(x614,x612)+P9(x611,f6(x612))+P9(x611,f6(x613))+P9(x614,f6(x612))+P9(x614,f6(x613))
% 61.56/61.85 %EqnAxiom
% 61.56/61.85
% 61.56/61.86 %-------------------------------------------
% 61.70/61.92 cnf(73,plain,
% 61.70/61.92 (~P15(x731,x732)),
% 61.70/61.92 inference(scs_inference,[],[5,10,3,18,50,22])).
% 61.70/61.92 cnf(238,plain,
% 61.70/61.92 (P10(a2,f6(a3))+~P14(a2,a3)),
% 61.70/61.92 inference(scs_inference,[],[13,20])).
% 61.70/61.92 cnf(314,plain,
% 61.70/61.92 (P1(x3141,f6(x3142))+P18(x3141,x3142)),
% 61.70/61.92 inference(scs_inference,[],[14,27])).
% 61.70/61.92 cnf(466,plain,
% 61.70/61.92 (~P5(x4661,x4661)),
% 61.70/61.92 inference(scs_inference,[],[1,17,26])).
% 61.70/61.93 cnf(618,plain,
% 61.70/61.93 (P14(x6181,f6(x6181))),
% 61.70/61.93 inference(scs_inference,[],[1,15,26])).
% 61.70/61.93 cnf(619,plain,
% 61.70/61.93 (~P1(x6191,f6(x6191))),
% 61.70/61.93 inference(scs_inference,[],[618,26])).
% 61.70/61.93 cnf(1226,plain,
% 61.70/61.93 (~P14(x12261,x12261)),
% 61.70/61.93 inference(scs_inference,[],[619,466,314,36])).
% 61.70/61.93 cnf(1227,plain,
% 61.70/61.93 (P14(f6(x12271),x12271)),
% 61.70/61.93 inference(scs_inference,[],[1226,15])).
% 61.70/61.93 cnf(1859,plain,
% 61.70/61.93 (P14(f6(a2),a3)+P10(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[618,30,238])).
% 61.70/61.93 cnf(1920,plain,
% 61.70/61.93 (~P1(f6(a2),a3)+P10(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[1859,26])).
% 61.70/61.93 cnf(1981,plain,
% 61.70/61.93 (~P18(a2,f6(a3))+~P1(f6(a2),a3)),
% 61.70/61.93 inference(scs_inference,[],[1920,25])).
% 61.70/61.93 cnf(2042,plain,
% 61.70/61.93 (~P1(f6(a2),a3)+P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[1981,12])).
% 61.70/61.93 cnf(2103,plain,
% 61.70/61.93 (P14(f6(a2),a3)+P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[2042,14])).
% 61.70/61.93 cnf(2164,plain,
% 61.70/61.93 (P14(a3,f6(a2))+P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[1226,2103,30])).
% 61.70/61.93 cnf(2225,plain,
% 61.70/61.93 (P18(a3,a2)+P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[2164,27])).
% 61.70/61.93 cnf(6315,plain,
% 61.70/61.93 (P12(x63151,f6(x63151))+~P14(x63151,f6(f6(x63151)))),
% 61.70/61.93 inference(scs_inference,[],[619,4,14,44])).
% 61.70/61.93 cnf(9536,plain,
% 61.70/61.93 (~P14(a3,a2)+P5(a3,a2)+P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[2225,36])).
% 61.70/61.93 cnf(9597,plain,
% 61.70/61.93 (~P18(a2,f6(a3))+~P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[9536,20])).
% 61.70/61.93 cnf(9658,plain,
% 61.70/61.93 (P10(a2,f6(a3))+~P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[9597,13])).
% 61.70/61.93 cnf(9719,plain,
% 61.70/61.93 (P14(f6(a3),a2)+P10(a2,f6(a3))+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[618,9658,30])).
% 61.70/61.93 cnf(9780,plain,
% 61.70/61.93 (~P18(a2,f6(a3))+P14(f6(a3),a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[9719,25])).
% 61.70/61.93 cnf(9841,plain,
% 61.70/61.93 (P14(a2,a3)+P14(f6(a3),a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[9780,12])).
% 61.70/61.93 cnf(9902,plain,
% 61.70/61.93 (P14(a3,a2)+P14(f6(a3),a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[1226,9841,30])).
% 61.70/61.93 cnf(9963,plain,
% 61.70/61.93 (P14(a2,f6(a3))+P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[1226,9902,30])).
% 61.70/61.93 cnf(10024,plain,
% 61.70/61.93 (~P1(a2,f6(a3))+P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[9963,26])).
% 61.70/61.93 cnf(10085,plain,
% 61.70/61.93 (P18(a2,a3)+P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[10024,314])).
% 61.70/61.93 cnf(10146,plain,
% 61.70/61.93 (~P10(a2,a3)+P14(a3,a2)+P5(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[10085,25])).
% 61.70/61.93 cnf(10207,plain,
% 61.70/61.93 (P5(a3,a2)+~P18(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[10146,36])).
% 61.70/61.93 cnf(10876,plain,
% 61.70/61.93 (P14(a2,a3)+P5(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[2225,10207])).
% 61.70/61.93 cnf(10937,plain,
% 61.70/61.93 (~P18(a2,f6(a3))+P5(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[10876,20])).
% 61.70/61.93 cnf(10998,plain,
% 61.70/61.93 (P10(a2,f6(a3))+P5(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[10937,13])).
% 61.70/61.93 cnf(11059,plain,
% 61.70/61.93 (P14(a3,a2)+P10(a2,f6(a3))+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[10998,17])).
% 61.70/61.93 cnf(11120,plain,
% 61.70/61.93 (~P18(a2,f6(a3))+P14(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[11059,25])).
% 61.70/61.93 cnf(11181,plain,
% 61.70/61.93 (P14(a3,a2)+P14(a2,a3)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[11120,12])).
% 61.70/61.93 cnf(11242,plain,
% 61.70/61.93 (P14(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[1226,11181,30])).
% 61.70/61.93 cnf(11303,plain,
% 61.70/61.93 (~P1(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[11242,26])).
% 61.70/61.93 cnf(11364,plain,
% 61.70/61.93 (P18(a2,a3)+~P1(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[11303,13])).
% 61.70/61.93 cnf(11425,plain,
% 61.70/61.93 (~P1(a3,a2)+P14(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[11364,21])).
% 61.70/61.93 cnf(11486,plain,
% 61.70/61.93 (~P1(a2,f6(a3))+~P1(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[11425,26])).
% 61.70/61.93 cnf(11547,plain,
% 61.70/61.93 (P14(a3,a2)+~P1(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[11486,14])).
% 61.70/61.93 cnf(54852,plain,
% 61.70/61.93 (~P14(x548521,f6(f6(x548521)))),
% 61.70/61.93 inference(scs_inference,[],[4,6315])).
% 61.70/61.93 cnf(54855,plain,
% 61.70/61.93 (~P14(f1(x548551,x548552),x548551)),
% 61.70/61.93 inference(scs_inference,[],[2,4,6315,26])).
% 61.70/61.93 cnf(54857,plain,
% 61.70/61.93 (P14(f1(x548571,x548572),f6(x548571))),
% 61.70/61.93 inference(scs_inference,[],[73,2,4,6315,26,15])).
% 61.70/61.93 cnf(54859,plain,
% 61.70/61.93 (P14(f6(f1(x548591,x548592)),x548591)),
% 61.70/61.93 inference(scs_inference,[],[73,1227,2,4,6315,26,15,30])).
% 61.70/61.93 cnf(54868,plain,
% 61.70/61.93 (~P14(f1(x548681,x548682),f6(f6(x548681)))),
% 61.70/61.93 inference(scs_inference,[],[54855,54857,1226,3,42])).
% 61.70/61.93 cnf(54872,plain,
% 61.70/61.93 (~P14(f6(f1(x548721,x548722)),f6(x548721))+P12(f6(f1(x548721,x548722)),f6(x548721))),
% 61.70/61.93 inference(scs_inference,[],[54855,54857,54859,1226,4,3,42,44])).
% 61.70/61.93 cnf(54877,plain,
% 61.70/61.93 (~P14(f6(f1(x548771,x548772)),f6(x548771))),
% 61.70/61.93 inference(scs_inference,[],[73,4,54872])).
% 61.70/61.93 cnf(54879,plain,
% 61.70/61.93 (~P14(f6(x548791),f1(x548791,x548792))+~P14(f6(x548791),f6(f1(x548791,x548792)))),
% 61.70/61.93 inference(scs_inference,[],[54868,54852,73,4,54872,43])).
% 61.70/61.93 cnf(54886,plain,
% 61.70/61.93 (~P14(f1(f1(x548861,x548862),x548863),x548861)+P12(f1(f1(x548861,x548862),x548863),f6(x548861))),
% 61.70/61.93 inference(scs_inference,[],[54877,54857,4,3,30,44])).
% 61.70/61.93 cnf(54889,plain,
% 61.70/61.93 (~P14(f1(f1(x548891,x548892),x548893),x548891)),
% 61.70/61.93 inference(scs_inference,[],[73,4,54886])).
% 61.70/61.93 cnf(54930,plain,
% 61.70/61.93 (~P14(f6(x549301),f1(x549301,x549302))+P1(f6(x549301),f6(f1(x549301,x549302)))),
% 61.70/61.93 inference(scs_inference,[],[54879,14])).
% 61.70/61.93 cnf(54979,plain,
% 61.70/61.93 (P14(a2,f6(f6(a3)))+P18(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[54852,2225,30])).
% 61.70/61.93 cnf(55007,plain,
% 61.70/61.93 (P14(a3,f6(a2))+P14(a2,f6(f6(a3)))),
% 61.70/61.93 inference(scs_inference,[],[54979,21])).
% 61.70/61.93 cnf(55021,plain,
% 61.70/61.93 (~P1(a3,f6(a2))+P14(a2,f6(f6(a3)))),
% 61.70/61.93 inference(scs_inference,[],[55007,26])).
% 61.70/61.93 cnf(55028,plain,
% 61.70/61.93 (P18(a2,f6(a3))+~P1(a3,f6(a2))),
% 61.70/61.93 inference(scs_inference,[],[55021,27])).
% 61.70/61.93 cnf(55029,plain,
% 61.70/61.93 (P14(a3,f6(a2))+P18(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[55028,14])).
% 61.70/61.93 cnf(55030,plain,
% 61.70/61.93 (P18(a3,a2)+P18(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[55029,27])).
% 61.70/61.93 cnf(55032,plain,
% 61.70/61.93 (~P10(a3,a2)+P18(a2,f6(a3))),
% 61.70/61.93 inference(scs_inference,[],[55030,25])).
% 61.70/61.93 cnf(55038,plain,
% 61.70/61.93 (~P10(a3,a2)+~P14(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[55032,20])).
% 61.70/61.93 cnf(55055,plain,
% 61.70/61.93 (P14(x550551,f6(f1(x550551,x550552)))),
% 61.70/61.93 inference(scs_inference,[],[54859,1226,30])).
% 61.70/61.93 cnf(55081,plain,
% 61.70/61.93 (~P14(x550811,f1(x550811,x550812))+P12(x550811,f6(f1(x550811,x550812)))),
% 61.70/61.93 inference(scs_inference,[],[55055,4,44])).
% 61.70/61.93 cnf(55089,plain,
% 61.70/61.93 (~P14(x550891,f1(x550891,x550892))),
% 61.70/61.93 inference(scs_inference,[],[4,55081])).
% 61.70/61.93 cnf(55134,plain,
% 61.70/61.93 (P14(f6(x551341),f1(x551341,x551342))),
% 61.70/61.93 inference(scs_inference,[],[55089,1227,30])).
% 61.70/61.93 cnf(55141,plain,
% 61.70/61.93 (~P14(f6(x551411),f6(f1(x551411,x551412)))),
% 61.70/61.93 inference(scs_inference,[],[55134,54930,26])).
% 61.70/61.93 cnf(55285,plain,
% 61.70/61.93 (~P10(a3,a2)+P18(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[2225,55038])).
% 61.70/61.93 cnf(55286,plain,
% 61.70/61.93 (P18(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[55285,13])).
% 61.70/61.93 cnf(55287,plain,
% 61.70/61.93 (P5(a3,a2)+~P10(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[55286,10207])).
% 61.70/61.93 cnf(55290,plain,
% 61.70/61.93 (P14(a3,f6(a2))),
% 61.70/61.93 inference(scs_inference,[],[55286,25,21])).
% 61.70/61.93 cnf(55300,plain,
% 61.70/61.93 (~P14(a3,a2)+P12(a3,f6(a2))),
% 61.70/61.93 inference(scs_inference,[],[55286,4,25,21,26,58,57,36,44])).
% 61.70/61.93 cnf(55303,plain,
% 61.70/61.93 (P5(a3,a2)+P18(a2,a3)),
% 61.70/61.93 inference(scs_inference,[],[55287,13])).
% 61.70/61.93 cnf(55304,plain,
% 61.70/61.93 (~P14(a3,a2)),
% 61.70/61.93 inference(scs_inference,[],[4,55300])).
% 61.70/61.93 cnf(55317,plain,
% 61.70/61.93 (~P14(a3,f6(f6(a2)))+P12(a3,f6(f6(a2)))),
% 61.70/61.93 inference(scs_inference,[],[55290,55141,73,3,4,30,58,32,27,36,44])).
% 61.70/61.93 cnf(55320,plain,
% 61.70/61.93 (P5(a3,a2)+P14(f6(a3),a2)),
% 61.70/61.93 inference(scs_inference,[],[55304,9902])).
% 61.73/61.93 cnf(55323,plain,
% 61.73/61.93 (~P1(a2,f6(a3))),
% 61.73/61.93 inference(scs_inference,[],[55304,11547])).
% 61.73/61.93 cnf(55324,plain,
% 61.73/61.93 (P18(a2,a3)),
% 61.73/61.93 inference(scs_inference,[],[55304,55303,17])).
% 61.73/61.93 cnf(55325,plain,
% 61.73/61.93 (~P14(a3,f6(f6(a2)))),
% 61.73/61.93 inference(scs_inference,[],[4,55317])).
% 61.73/61.93 cnf(55326,plain,
% 61.73/61.93 (P14(a2,f6(a3))),
% 61.73/61.93 inference(scs_inference,[],[55323,14])).
% 61.73/61.93 cnf(55330,plain,
% 61.73/61.93 (~P14(a3,f1(f1(a2,x553301),x553302))),
% 61.73/61.93 inference(scs_inference,[],[55323,55304,54889,14,17,30])).
% 61.73/61.93 cnf(55333,plain,
% 61.73/61.93 (P14(f6(a3),a2)),
% 61.73/61.93 inference(scs_inference,[],[55323,55304,54889,14,17,30,55320])).
% 61.73/61.93 cnf(55337,plain,
% 61.73/61.93 (~P18(a2,f6(a3))+P12(a2,f6(f6(a3)))),
% 61.73/61.93 inference(scs_inference,[],[55323,55304,54889,4,14,17,30,55320,44,21])).
% 61.73/61.93 cnf(55351,plain,
% 61.73/61.93 (~P18(a2,f6(a3))),
% 61.73/61.93 inference(scs_inference,[],[4,55337])).
% 61.73/61.93 cnf(55355,plain,
% 61.73/61.93 (~P14(f6(x553551),f6(f1(x553551,x553552)))),
% 61.73/61.93 inference(rename_variables,[],[55141])).
% 61.73/61.93 cnf(55360,plain,
% 61.73/61.93 (P12(a2,f6(f1(a3,x553601)))+~P14(f6(a3),f6(a2))),
% 61.73/61.93 inference(scs_inference,[],[55333,55325,55141,55355,4,14,30,43,44])).
% 61.73/61.93 cnf(55367,plain,
% 61.73/61.93 (P14(a2,a3)),
% 61.73/61.93 inference(scs_inference,[],[55351,12])).
% 61.73/61.93 cnf(55368,plain,
% 61.73/61.93 (~P14(f6(a3),f6(a2))),
% 61.73/61.93 inference(scs_inference,[],[4,55360])).
% 61.73/61.93 cnf(55411,plain,
% 61.73/61.93 (P12(a2,f6(a3))),
% 61.73/61.93 inference(scs_inference,[],[55367,55368,55330,55324,55326,55089,4,21,30,36,44])).
% 61.73/61.93 cnf(55417,plain,
% 61.73/61.93 ($false),
% 61.73/61.93 inference(scs_inference,[],[55411,4]),
% 61.73/61.93 ['proof']).
% 61.73/61.99 % SZS output end Proof
% 61.73/61.99 % Total time :60.960000s
%------------------------------------------------------------------------------