%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO231+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 : n025.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:47 EDT 2024
% Result : Theorem 58.53s 58.75s
% Output : CNFRefutation 58.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : GEO231+3 : TPTP v8.2.0. Released v4.0.0.
% 0.05/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n025.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Fri Jun 21 06:37:53 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.53 start to proof:theBenchmark
% 58.53/58.73 %-------------------------------------------
% 58.53/58.73 % File :CSE---1.7
% 58.53/58.73 % Problem :theBenchmark
% 58.53/58.73 % Transform :cnf
% 58.53/58.73 % Format :tptp:raw
% 58.53/58.73 % Command :java -jar mcs_scs.jar %d %s
% 58.53/58.73
% 58.53/58.73 % Result :Theorem 58.030000s
% 58.53/58.73 % Output :CNFRefutation 58.030000s
% 58.53/58.73 %-------------------------------------------
% 58.53/58.75 %------------------------------------------------------------------------------
% 58.53/58.75 % File : GEO231+3 : TPTP v8.2.0. Released v4.0.0.
% 58.53/58.75 % Domain : Geometry (Constructive)
% 58.53/58.75 % Problem : Oppositely and equally directed lines
% 58.53/58.75 % Version : [vPl98] axioms.
% 58.53/58.75 % English :
% 58.53/58.75
% 58.53/58.75 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 58.53/58.75 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.53/58.75 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.53/58.75 % Source : [Rat07]
% 58.53/58.75 % Names : Therorem 3.5 [vPl98]
% 58.53/58.75
% 58.53/58.75 % Status : Theorem
% 58.53/58.75 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v6.1.0, 0.08 v6.0.0, 0.00 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.53/58.75 % Syntax : Number of formulae : 37 ( 6 unt; 0 def)
% 58.53/58.75 % Number of atoms : 112 ( 0 equ)
% 58.53/58.75 % Maximal formula atoms : 10 ( 3 avg)
% 58.53/58.75 % Number of connectives : 87 ( 12 ~; 22 |; 25 &)
% 58.53/58.75 % ( 10 <=>; 18 =>; 0 <=; 0 <~>)
% 58.53/58.75 % Maximal formula depth : 13 ( 5 avg)
% 58.53/58.75 % Maximal term depth : 3 ( 1 avg)
% 58.53/58.75 % Number of predicates : 18 ( 18 usr; 0 prp; 1-4 aty)
% 58.53/58.75 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 58.53/58.75 % Number of variables : 84 ( 84 !; 0 ?)
% 58.53/58.75 % SPC : FOF_THM_RFO_NEQ
% 58.53/58.75
% 58.53/58.75 % Comments :
% 58.53/58.75 %------------------------------------------------------------------------------
% 58.53/58.75 include('Axioms/GEO009+0.ax').
% 58.53/58.75 %------------------------------------------------------------------------------
% 58.53/58.75 fof(con,conjecture,
% 58.53/58.75 ! [L,M,N] :
% 58.53/58.75 ( ( equally_directed_opposite_lines(L,M)
% 58.53/58.75 & equally_directed_lines(L,N) )
% 58.53/58.75 => equally_directed_opposite_lines(M,N) ) ).
% 58.53/58.75
% 58.53/58.75 %------------------------------------------------------------------------------
% 58.53/58.75 %-------------------------------------------
% 58.53/58.75 % Proof found
% 58.53/58.75 % SZS status Theorem for theBenchmark
% 58.53/58.75 % SZS output start Proof
% 58.53/58.76 %ClaNum:69(EqnAxiom:0)
% 58.53/58.76 %VarNum:311(SingletonVarNum:129)
% 58.53/58.76 %MaxLitNum:10
% 58.53/58.76 %MaxfuncDepth:2
% 58.53/58.76 %SharedTerms:6
% 58.53/58.76 %goalClause: 1 2 5
% 58.53/58.76 %singleGoalClaCount:3
% 58.53/58.76 [1]P1(a1,a2)
% 58.53/58.76 [2]P9(a1,a3)
% 58.53/58.76 [5]~P9(a3,a2)
% 58.53/58.76 [3]P1(x31,x31)
% 58.53/58.76 [8]~P2(x81,x81)
% 58.53/58.76 [9]~P3(x91,x91)
% 58.53/58.76 [12]~P3(x121,f7(x121))
% 58.53/58.76 [6]~P10(x61,x62)
% 58.53/58.76 [7]~P12(x71,x72)
% 58.53/58.76 [4]P1(f4(x41,x42),x41)
% 58.53/58.76 [13]~P4(x131,f4(x132,x131))
% 58.53/58.76 [14]~P13(x141)+P13(f7(x141))
% 58.53/58.76 [15]P9(x151,x152)+P14(x151,x152)
% 58.53/58.76 [16]P1(x161,x162)+P15(x161,x162)
% 58.53/58.76 [18]~P5(x181,x182)+P14(x181,x182)
% 58.53/58.76 [19]~P5(x191,x192)+P15(x191,x192)
% 58.53/58.76 [20]~P16(x201,x202)+P4(x201,x202)
% 58.53/58.76 [26]~P9(x261,x262)+~P14(x261,x262)
% 58.53/58.76 [27]~P1(x271,x272)+~P15(x271,x272)
% 58.53/58.76 [17]P15(x171,x172)+P15(x171,f7(x172))
% 58.53/58.76 [22]~P14(x221,x222)+P15(x221,f7(x222))
% 58.53/58.76 [23]~P16(x231,x232)+P10(x231,f7(x232))
% 58.53/58.76 [24]~P18(x241,x242)+P12(x241,f7(x242))
% 58.53/58.76 [28]P14(x281,x282)+~P15(x281,f7(x282))
% 58.53/58.76 [41]~P2(x411,x412)+~P4(x412,f5(x411,x412))
% 58.53/58.76 [42]~P2(x421,x422)+~P4(x421,f5(x421,x422))
% 58.53/58.76 [60]~P2(x601,x602)+P1(f5(x601,x602),f7(f5(x602,x601)))
% 58.53/58.76 [51]P2(x511,x512)+~P6(x513,x511,x512)
% 58.53/58.76 [52]P11(x521,x522)+~P6(x522,x523,x521)
% 58.53/58.76 [53]P11(x531,x532)+~P6(x532,x531,x533)
% 58.53/58.76 [61]~P6(x611,x612,x613)+P1(x611,f5(x612,x613))
% 58.53/58.76 [33]P10(x331,x332)+~P4(x331,x332)+P16(x331,x332)
% 58.53/58.76 [37]~P14(x371,x372)+~P15(x371,x372)+P5(x371,x372)
% 58.53/58.76 [25]~P17(x252)+~P13(x251)+P13(f4(x251,x252))
% 58.53/58.76 [58]~P15(x581,x582)+~P15(x581,f7(x582))+~P4(f6(x581,x582),x582)
% 58.53/58.76 [59]~P15(x591,x592)+~P15(x591,f7(x592))+~P4(f6(x591,x592),x591)
% 58.53/58.76 [31]~P15(x313,x311)+P15(x311,x312)+P15(x313,x312)
% 58.53/58.76 [35]~P2(x353,x351)+P2(x351,x352)+P2(x353,x352)
% 58.53/58.76 [36]~P3(x363,x361)+P3(x361,x362)+P3(x363,x362)
% 58.53/58.76 [54]~P8(x542,x543,x541)+P16(x541,x542)+P16(x543,x542)
% 58.53/58.76 [55]P10(x551,x552)+P16(x551,x552)+~P8(x552,x553,x551)
% 58.53/58.76 [56]P10(x561,x562)+P16(x561,x562)+~P8(x562,x561,x563)
% 58.53/58.76 [57]~P8(x572,x571,x573)+P10(x571,x572)+P10(x573,x572)
% 58.53/58.76 [64]~P6(x641,x643,x642)+~P6(x641,x644,x643)+P7(x641,x642,x643,x644)
% 58.53/58.76 [65]~P6(x651,x653,x654)+~P6(x651,x652,x653)+P7(x651,x652,x653,x654)
% 58.53/58.76 [66]~P7(x661,x662,x663,x664)+P6(x661,x662,x663)+P6(x661,x664,x663)
% 58.53/58.76 [67]P6(x671,x673,x672)+P6(x671,x672,x673)+~P7(x671,x674,x672,x673)
% 58.53/58.76 [68]P6(x681,x683,x682)+P6(x681,x682,x683)+~P7(x681,x682,x683,x684)
% 58.53/58.76 [69]~P7(x691,x694,x692,x693)+P6(x691,x692,x693)+P6(x691,x692,x694)
% 58.53/58.76 [38]~P17(x382)+~P17(x381)+~P2(x381,x382)+P13(f5(x381,x382))
% 58.53/58.76 [45]~P15(x451,x452)+P12(x451,x452)+P12(x451,f7(x452))+~P15(x451,f7(x452))
% 58.53/58.76 [43]~P15(x431,x433)+P15(x431,x432)+~P15(x431,f7(x433))+P15(x433,f7(x432))
% 58.53/58.76 [44]~P15(x443,x441)+P15(x441,x442)+~P15(x443,f7(x441))+P15(x443,f7(x442))
% 58.53/58.76 [47]~P13(x472)+~P13(x471)+~P15(x471,x472)+~P15(x471,f7(x472))+P17(f6(x471,x472))
% 58.53/58.76 [63]~P2(x632,x633)+~P11(x633,x631)+~P11(x632,x631)+P6(x631,x632,x633)+~P1(x631,f5(x632,x633))
% 58.53/58.76 [62]P10(x624,x623)+~P2(x624,x621)+~P3(x623,x622)+P10(x621,x622)+P10(x621,x623)+P10(x624,x622)+P10(x621,f7(x622))+P10(x621,f7(x623))+P10(x624,f7(x622))+P10(x624,f7(x623))
% 58.53/58.76 %EqnAxiom
% 58.53/58.76
% 58.53/58.76 %-------------------------------------------
% 58.53/58.79 cnf(74,plain,
% 58.53/58.79 (~P16(x741,x742)),
% 58.53/58.79 inference(scs_inference,[],[8,6,13,51,20,23])).
% 58.53/58.79 cnf(239,plain,
% 58.53/58.79 (P15(a3,f7(a2))),
% 58.53/58.79 inference(scs_inference,[],[5,15,22])).
% 58.53/58.79 cnf(240,plain,
% 58.53/58.79 (~P1(a3,f7(a2))),
% 58.53/58.79 inference(scs_inference,[],[239,27])).
% 58.53/58.79 cnf(242,plain,
% 58.53/58.79 (P14(a3,a2)),
% 58.53/58.79 inference(scs_inference,[],[239,27,28])).
% 58.53/58.79 cnf(321,plain,
% 58.53/58.79 (P15(a3,x3211)+P1(a3,f7(a2))+P15(f7(a2),x3211)),
% 58.53/58.79 inference(scs_inference,[],[240,16,31])).
% 58.53/58.79 cnf(322,plain,
% 58.53/58.79 (P15(f7(a2),x3221)+P15(a3,x3221)),
% 58.53/58.79 inference(scs_inference,[],[240,321])).
% 58.53/58.79 cnf(329,plain,
% 58.53/58.79 (P12(a3,a2)+P15(f7(a2),a2)),
% 58.53/58.79 inference(scs_inference,[],[240,239,242,7,321,37,58,59,45])).
% 58.53/58.79 cnf(337,plain,
% 58.53/58.79 (~P1(f7(a2),a2)),
% 58.53/58.79 inference(scs_inference,[],[7,329,27])).
% 58.53/58.79 cnf(455,plain,
% 58.53/58.79 (P12(a3,a2)+~P15(a3,a2)),
% 58.53/58.79 inference(scs_inference,[],[239,7,59,58,44,45])).
% 58.53/58.79 cnf(459,plain,
% 58.53/58.79 (~P15(a3,a2)),
% 58.53/58.79 inference(scs_inference,[],[7,455])).
% 58.53/58.79 cnf(513,plain,
% 58.53/58.79 (P15(a1,f7(a2))),
% 58.53/58.79 inference(scs_inference,[],[1,17,27])).
% 58.53/58.79 cnf(747,plain,
% 58.53/58.79 (P14(f7(a2),x7471)+P15(a3,f7(x7471))),
% 58.53/58.79 inference(scs_inference,[],[322,28])).
% 58.53/58.79 cnf(1203,plain,
% 58.53/58.79 (~P9(f7(a2),x12031)+P15(a3,f7(x12031))),
% 58.53/58.79 inference(scs_inference,[],[747,26])).
% 58.53/58.79 cnf(1837,plain,
% 58.53/58.79 (P12(a1,a2)+~P15(a1,a2)),
% 58.53/58.79 inference(scs_inference,[],[513,7,58,59,44,45])).
% 58.53/58.79 cnf(1841,plain,
% 58.53/58.79 (~P15(a1,a2)),
% 58.53/58.79 inference(scs_inference,[],[7,1837])).
% 58.53/58.79 cnf(3459,plain,
% 58.53/58.79 (P15(f7(a2),x34591)+P15(a2,x34591)),
% 58.53/58.79 inference(scs_inference,[],[337,16,31])).
% 58.53/58.79 cnf(13568,plain,
% 58.53/58.79 (~P15(x135681,x135681)),
% 58.53/58.79 inference(scs_inference,[],[3,27])).
% 58.53/58.79 cnf(13578,plain,
% 58.53/58.79 (P15(f7(x135781),x135781)),
% 58.53/58.79 inference(scs_inference,[],[13568,17])).
% 58.53/58.79 cnf(13579,plain,
% 58.63/58.79 (~P15(x135791,x135791)),
% 58.63/58.79 inference(rename_variables,[],[13568])).
% 58.63/58.79 cnf(13582,plain,
% 58.63/58.79 (~P15(x135821,x135821)),
% 58.63/58.79 inference(rename_variables,[],[13568])).
% 58.63/58.79 cnf(13584,plain,
% 58.63/58.79 (P15(f7(a2),a3)),
% 58.63/58.79 inference(scs_inference,[],[13568,13579,13582,17,22,322])).
% 58.63/58.79 cnf(13589,plain,
% 58.63/58.79 (~P15(f4(x135891,x135892),x135891)),
% 58.63/58.79 inference(scs_inference,[],[13568,13579,13582,4,17,22,322,28,27])).
% 58.63/58.79 cnf(13604,plain,
% 58.63/58.79 (~P15(f4(x136041,x136042),x136041)),
% 58.63/58.79 inference(rename_variables,[],[13589])).
% 58.63/58.79 cnf(13608,plain,
% 58.63/58.79 (P15(f4(f7(x136081),x136082),x136081)),
% 58.63/58.79 inference(scs_inference,[],[13589,13604,22,15,17])).
% 58.63/58.79 cnf(13609,plain,
% 58.63/58.79 (~P15(f4(x136091,x136092),x136091)),
% 58.63/58.79 inference(rename_variables,[],[13589])).
% 58.63/58.79 cnf(13611,plain,
% 58.63/58.79 (P15(x136111,f7(x136111))),
% 58.63/58.79 inference(scs_inference,[],[13589,13604,13609,22,15,17,31])).
% 58.63/58.79 cnf(13624,plain,
% 58.63/58.79 (P15(f7(f4(x136241,x136242)),x136241)),
% 58.63/58.79 inference(scs_inference,[],[13589,13611,31])).
% 58.63/58.79 cnf(13658,plain,
% 58.63/58.79 (P15(x136581,f4(f7(x136581),x136582))),
% 58.63/58.79 inference(scs_inference,[],[13568,13608,31])).
% 58.63/58.79 cnf(13665,plain,
% 58.63/58.79 (P15(x136651,f7(f4(x136651,x136652)))),
% 58.63/58.79 inference(scs_inference,[],[13568,13624,31])).
% 58.63/58.79 cnf(13914,plain,
% 58.63/58.79 (P15(f7(a1),a2)),
% 58.63/58.79 inference(scs_inference,[],[1841,13611,31])).
% 58.63/58.79 cnf(13926,plain,
% 58.63/58.79 (P15(f7(f4(a1,x139261)),a2)),
% 58.63/58.79 inference(scs_inference,[],[1841,13665,31])).
% 58.63/58.79 cnf(13937,plain,
% 58.63/58.79 (P15(f4(f7(a1),x139371),a2)),
% 58.63/58.79 inference(scs_inference,[],[1841,13658,31])).
% 58.63/58.79 cnf(13948,plain,
% 58.63/58.79 (P15(a2,f7(a1))),
% 58.63/58.79 inference(scs_inference,[],[13568,13914,31])).
% 58.63/58.79 cnf(13963,plain,
% 58.63/58.79 (P15(a2,f7(f4(a1,x139631)))),
% 58.63/58.79 inference(scs_inference,[],[13568,13926,31])).
% 58.63/58.79 cnf(13964,plain,
% 58.63/58.79 (~P15(x139641,x139641)),
% 58.63/58.79 inference(rename_variables,[],[13568])).
% 58.63/58.79 cnf(13966,plain,
% 58.63/58.79 (P14(a2,f4(a1,x139661))),
% 58.63/58.79 inference(scs_inference,[],[13568,13926,31,28])).
% 58.63/58.79 cnf(13974,plain,
% 58.63/58.79 (~P15(a2,f4(a1,x139741))+P15(f4(a1,x139741),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[13568,13964,13665,13926,31,28,58,26,59,43])).
% 58.63/58.79 cnf(13981,plain,
% 58.63/58.79 (P15(a2,f4(f7(a1),x139811))),
% 58.63/58.79 inference(scs_inference,[],[13568,13937,31])).
% 58.63/58.79 cnf(14851,plain,
% 58.63/58.79 (P12(f7(f7(x148511)),x148511)+~P15(f7(f7(x148511)),x148511)),
% 58.63/58.79 inference(scs_inference,[],[13578,13948,7,59,58,45])).
% 58.63/58.79 cnf(14859,plain,
% 58.63/58.79 (~P15(f7(f7(x148591)),x148591)),
% 58.63/58.79 inference(scs_inference,[],[7,14851])).
% 58.63/58.79 cnf(14953,plain,
% 58.63/58.79 (P12(a2,a1)+~P15(a2,a1)),
% 58.63/58.79 inference(scs_inference,[],[13948,7,59,58,45])).
% 58.63/58.79 cnf(14960,plain,
% 58.63/58.79 (~P15(a2,a1)),
% 58.63/58.79 inference(scs_inference,[],[7,14953])).
% 58.63/58.79 cnf(15062,plain,
% 58.63/58.79 (~P1(f4(a1,x150621),f7(a2))+~P15(a2,f4(a1,x150621))),
% 58.63/58.79 inference(scs_inference,[],[13974,27])).
% 58.63/58.79 cnf(15183,plain,
% 58.63/58.79 (~P5(a2,f4(a1,x151831))+~P1(f4(a1,x151831),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[15062,19])).
% 58.63/58.79 cnf(15304,plain,
% 58.63/58.79 (P15(f4(a1,x153041),f7(a2))+~P5(a2,f4(a1,x153041))),
% 58.63/58.79 inference(scs_inference,[],[15183,16])).
% 58.63/58.79 cnf(15425,plain,
% 58.63/58.79 (P14(f4(a1,x154251),a2)+~P5(a2,f4(a1,x154251))),
% 58.63/58.79 inference(scs_inference,[],[15304,28])).
% 58.63/58.79 cnf(15546,plain,
% 58.63/58.79 (~P15(a2,f4(a1,x155461))+P14(f4(a1,x155461),a2)),
% 58.63/58.79 inference(scs_inference,[],[13966,15425,37])).
% 58.63/58.79 cnf(15667,plain,
% 58.63/58.79 (~P9(f4(a1,x156671),a2)+~P15(a2,f4(a1,x156671))),
% 58.63/58.79 inference(scs_inference,[],[15546,26])).
% 58.63/58.79 cnf(15776,plain,
% 58.63/58.79 (P12(x157761,f4(x157761,x157762))+~P15(x157761,f4(x157761,x157762))),
% 58.63/58.79 inference(scs_inference,[],[13665,7,58,59,45])).
% 58.63/58.79 cnf(15783,plain,
% 58.63/58.79 (~P15(x157831,f4(x157831,x157832))),
% 58.63/58.79 inference(scs_inference,[],[7,15776])).
% 58.63/58.79 cnf(15807,plain,
% 58.63/58.79 (P15(f7(a2),f4(a1,x158071))+~P9(f4(a1,x158071),a2)),
% 58.63/58.79 inference(scs_inference,[],[15667,3459])).
% 58.63/58.79 cnf(15808,plain,
% 58.63/58.79 (P15(f7(a2),f4(a3,x158081))),
% 58.63/58.79 inference(scs_inference,[],[15783,322])).
% 58.63/58.79 cnf(15809,plain,
% 58.63/58.79 (~P15(x158091,f4(x158091,x158092))),
% 58.63/58.79 inference(rename_variables,[],[15783])).
% 58.63/58.79 cnf(15815,plain,
% 58.63/58.79 (P15(f4(a3,x158151),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[13568,15783,15809,322,16,19,31])).
% 58.63/58.79 cnf(15945,plain,
% 58.63/58.79 (~P1(f7(a2),f4(a1,x159451))+~P9(f4(a1,x159451),a2)),
% 58.63/58.79 inference(scs_inference,[],[15807,27])).
% 58.63/58.79 cnf(16187,plain,
% 58.63/58.79 (P14(f4(a1,x161871),a2)+~P1(f7(a2),f4(a1,x161871))),
% 58.63/58.79 inference(scs_inference,[],[15945,15])).
% 58.63/58.79 cnf(16429,plain,
% 58.63/58.79 (P15(f7(a2),f4(a1,x164291))+P14(f4(a1,x164291),a2)),
% 58.63/58.79 inference(scs_inference,[],[16187,16])).
% 58.63/58.79 cnf(16671,plain,
% 58.63/58.79 (P15(f4(a1,x166711),f7(a2))+P14(f4(a1,x166711),a2)),
% 58.63/58.79 inference(scs_inference,[],[13568,16429,31])).
% 58.63/58.79 cnf(18973,plain,
% 58.63/58.79 (~P1(f4(a1,x189731),f7(a2))+P14(f4(a1,x189731),a2)),
% 58.63/58.79 inference(scs_inference,[],[16671,27])).
% 58.63/58.79 cnf(19215,plain,
% 58.63/58.79 (~P1(f4(a1,x192151),f7(a2))+P15(f4(a1,x192151),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[18973,22])).
% 58.63/58.79 cnf(19456,plain,
% 58.63/58.79 (~P1(f4(a1,x194561),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[19215,27])).
% 58.63/58.79 cnf(19577,plain,
% 58.63/58.79 (P14(f4(a1,x195771),a2)),
% 58.63/58.79 inference(scs_inference,[],[19456,16,28])).
% 58.63/58.79 cnf(19700,plain,
% 58.63/58.79 (P15(f7(a2),f4(a1,x197001))),
% 58.63/58.79 inference(scs_inference,[],[19456,13568,16,31])).
% 58.63/58.79 cnf(19701,plain,
% 58.63/58.79 (P15(f4(a1,x197011),f7(a2))),
% 58.63/58.79 inference(scs_inference,[],[13568,19700,31])).
% 58.63/58.79 cnf(19824,plain,
% 58.63/58.79 (P15(f4(a1,x198241),a2)+~P15(f4(a1,x198241),f7(f7(a2)))),
% 58.63/58.79 inference(scs_inference,[],[19456,13568,16,43])).
% 58.63/58.79 cnf(23087,plain,
% 58.63/58.79 (P1(f4(a1,x230871),f7(f7(a2)))+P15(f4(a1,x230871),a2)),
% 58.63/58.79 inference(scs_inference,[],[16,19824])).
% 58.63/58.79 cnf(23208,plain,
% 58.63/58.79 (P5(f4(a1,x232081),a2)+P1(f4(a1,x232081),f7(f7(a2)))),
% 58.63/58.79 inference(scs_inference,[],[19577,23087,37])).
% 58.63/58.79 cnf(23329,plain,
% 58.63/58.79 (~P15(f4(a1,x233291),f7(f7(a2)))+P5(f4(a1,x233291),a2)),
% 58.63/58.79 inference(scs_inference,[],[23208,27])).
% 58.63/58.79 cnf(23945,plain,
% 58.63/58.79 (P12(a2,f4(a1,x239451))+~P15(a2,f4(a1,x239451))),
% 58.63/58.79 inference(scs_inference,[],[13963,7,59,58,45])).
% 58.63/58.79 cnf(23952,plain,
% 58.63/58.79 (~P15(a2,f4(a1,x239521))),
% 58.63/58.79 inference(scs_inference,[],[7,23945])).
% 58.63/58.79 cnf(24857,plain,
% 58.63/58.79 (P12(f4(a1,x248571),a2)+~P15(f4(a1,x248571),a2)),
% 58.63/58.79 inference(scs_inference,[],[19701,7,58,59,45])).
% 58.63/58.79 cnf(24870,plain,
% 58.63/58.79 (~P15(f4(a1,x248701),f7(f7(a2)))),
% 58.63/58.79 inference(scs_inference,[],[7,24857,19,16,23329])).
% 58.63/58.79 cnf(25770,plain,
% 58.63/58.79 (P15(f7(f4(a1,x257701)),f7(f7(a2)))),
% 58.63/58.79 inference(scs_inference,[],[24870,13578,31])).
% 58.63/58.79 cnf(28434,plain,
% 58.63/58.79 (~P15(a1,f7(a3))),
% 58.63/58.79 inference(scs_inference,[],[2,26,28])).
% 58.63/58.80 cnf(28439,plain,
% 58.63/58.80 (~P14(a1,a3)),
% 58.63/58.80 inference(scs_inference,[],[28434,19,22])).
% 58.63/58.80 cnf(30587,plain,
% 58.63/58.80 (P15(f7(a1),f7(a3))),
% 58.63/58.80 inference(scs_inference,[],[28439,13578,28,31])).
% 58.63/58.80 cnf(32884,plain,
% 58.63/58.80 (~P15(a3,f7(f7(a2)))),
% 58.63/58.80 inference(scs_inference,[],[13568,459,322,43])).
% 58.63/58.80 cnf(32895,plain,
% 58.63/58.80 (~P15(f7(a1),a3)+P15(f7(a1),f7(a2))),
% 58.63/58.80 inference(scs_inference,[],[25770,15815,30587,32884,22,19,16,59,58,43])).
% 58.63/58.80 cnf(33013,plain,
% 58.63/58.80 (P1(f7(a1),a3)+P15(f7(a1),f7(a2))),
% 58.63/58.80 inference(scs_inference,[],[32895,16])).
% 58.63/58.80 cnf(33026,plain,
% 58.63/58.80 (P12(f4(a3,x330261),a2)+~P15(f4(a3,x330261),a2)),
% 58.63/58.80 inference(scs_inference,[],[15815,7,59,58,45])).
% 58.63/58.80 cnf(33033,plain,
% 58.63/58.80 (~P15(f4(a3,x330331),a2)),
% 58.63/58.80 inference(scs_inference,[],[7,33026])).
% 58.63/58.80 cnf(33143,plain,
% 58.63/58.80 (P1(f7(a1),a3)),
% 58.63/58.80 inference(scs_inference,[],[13568,13914,14960,33013,44])).
% 58.63/58.80 cnf(33145,plain,
% 58.63/58.80 (~P15(f7(a1),a3)),
% 58.63/58.80 inference(scs_inference,[],[33143,27])).
% 58.63/58.80 cnf(34422,plain,
% 58.63/58.80 (P15(a2,a3)),
% 58.63/58.80 inference(scs_inference,[],[33145,13948,31])).
% 58.63/58.80 cnf(38607,plain,
% 58.63/58.80 (~P15(f7(a1),f4(a3,x386071))),
% 58.63/58.80 inference(scs_inference,[],[33145,13589,31])).
% 58.63/58.80 cnf(38749,plain,
% 58.63/58.80 (P14(f7(a2),f7(a3))),
% 58.63/58.80 inference(scs_inference,[],[13914,13568,14859,27,31,1203,747])).
% 58.63/58.80 cnf(40371,plain,
% 58.63/58.80 (~P15(f4(f4(x403711,x403712),x403713),x403711)),
% 58.63/58.80 inference(scs_inference,[],[13589,15783,31])).
% 58.63/58.80 cnf(43106,plain,
% 58.63/58.80 (~P15(f7(a1),f4(f4(a3,x431061),x431062))),
% 58.63/58.80 inference(scs_inference,[],[33145,40371,31])).
% 58.63/58.80 cnf(43799,plain,
% 58.63/58.80 (~P15(f7(a2),f7(f4(a3,x437991)))),
% 58.63/58.80 inference(scs_inference,[],[74,43106,38749,38607,23952,33033,13981,15808,15783,13568,17,322,16,31,37,44])).
% 58.63/58.80 cnf(43803,plain,
% 58.63/58.80 (P15(a2,f7(f4(a3,x438031)))),
% 58.63/58.80 inference(scs_inference,[],[74,43106,38749,38607,23952,33033,13981,15808,15783,13568,17,322,16,31,37,44,3459])).
% 58.63/58.80 cnf(43823,plain,
% 58.63/58.80 (P12(a2,f7(a3))),
% 58.63/58.80 inference(scs_inference,[],[43799,43803,13584,38607,23952,40371,34422,15783,7,6,17,16,31,44,3459,43,45])).
% 58.63/58.80 cnf(43826,plain,
% 58.63/58.80 ($false),
% 58.63/58.80 inference(scs_inference,[],[43823,7]),
% 58.63/58.80 ['proof']).
% 58.63/58.82 % SZS output end Proof
% 58.63/58.82 % Total time :58.030000s
%------------------------------------------------------------------------------