%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO218+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 : n021.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:40 EDT 2024
% Result : Theorem 58.72s 58.80s
% Output : CNFRefutation 58.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO218+3 : TPTP v8.2.0. Released v4.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri Jun 21 08:17:24 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.22/0.59 start to proof:theBenchmark
% 58.72/58.78 %-------------------------------------------
% 58.72/58.78 % File :CSE---1.7
% 58.72/58.78 % Problem :theBenchmark
% 58.72/58.78 % Transform :cnf
% 58.72/58.78 % Format :tptp:raw
% 58.72/58.78 % Command :java -jar mcs_scs.jar %d %s
% 58.72/58.78
% 58.72/58.78 % Result :Theorem 58.110000s
% 58.72/58.78 % Output :CNFRefutation 58.110000s
% 58.72/58.78 %-------------------------------------------
% 58.72/58.80 %------------------------------------------------------------------------------
% 58.72/58.80 % File : GEO218+3 : TPTP v8.2.0. Released v4.0.0.
% 58.72/58.80 % Domain : Geometry (Constructive)
% 58.72/58.80 % Problem : Transitivity of parallel and orthogonal
% 58.72/58.80 % Version : [vPl95] axioms.
% 58.72/58.80 % English : If two lines L and M are parallel and a third line N is
% 58.72/58.80 % orthogonal to L, then M is orthogonal to N.
% 58.72/58.80
% 58.72/58.80 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 58.72/58.80 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.72/58.80 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.72/58.80 % Source : [Rat07]
% 58.72/58.80 % Names : Theorem 8.7.ii [vPl95]
% 58.72/58.80
% 58.72/58.80 % Status : Theorem
% 58.72/58.80 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0, 0.21 v5.0.0, 0.10 v4.1.0, 0.06 v4.0.1, 0.05 v4.0.0
% 58.72/58.80 % Syntax : Number of formulae : 36 ( 7 unt; 0 def)
% 58.72/58.80 % Number of atoms : 96 ( 0 equ)
% 58.72/58.80 % Maximal formula atoms : 6 ( 2 avg)
% 58.72/58.80 % Number of connectives : 88 ( 28 ~; 19 |; 14 &)
% 58.72/58.80 % ( 5 <=>; 22 =>; 0 <=; 0 <~>)
% 58.72/58.80 % Maximal formula depth : 9 ( 5 avg)
% 58.72/58.80 % Maximal term depth : 2 ( 1 avg)
% 58.72/58.80 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 58.72/58.80 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 58.72/58.80 % Number of variables : 84 ( 84 !; 0 ?)
% 58.72/58.80 % SPC : FOF_THM_RFO_NEQ
% 58.72/58.80
% 58.72/58.80 % Comments :
% 58.72/58.80 %------------------------------------------------------------------------------
% 58.72/58.80 include('Axioms/GEO006+0.ax').
% 58.72/58.80 include('Axioms/GEO006+1.ax').
% 58.72/58.80 include('Axioms/GEO006+2.ax').
% 58.72/58.80 include('Axioms/GEO006+3.ax').
% 58.72/58.80 include('Axioms/GEO006+4.ax').
% 58.72/58.80 include('Axioms/GEO006+5.ax').
% 58.72/58.80 include('Axioms/GEO006+6.ax').
% 58.72/58.80 %------------------------------------------------------------------------------
% 58.72/58.80 fof(con,conjecture,
% 58.72/58.80 ! [L,M,N] :
% 58.72/58.80 ( ( parallel_lines(L,M)
% 58.72/58.80 & orthogonal_lines(L,N) )
% 58.72/58.80 => orthogonal_lines(M,N) ) ).
% 58.72/58.80
% 58.72/58.80 %------------------------------------------------------------------------------
% 58.72/58.80 %-------------------------------------------
% 58.72/58.80 % Proof found
% 58.72/58.80 % SZS status Theorem for theBenchmark
% 58.72/58.80 % SZS output start Proof
% 58.77/58.82 %ClaNum:49(EqnAxiom:0)
% 58.77/58.82 %VarNum:218(SingletonVarNum:98)
% 58.77/58.82 %MaxLitNum:6
% 58.77/58.82 %MaxfuncDepth:1
% 58.77/58.82 %SharedTerms:6
% 58.77/58.82 %goalClause: 1 2 3
% 58.77/58.82 %singleGoalClaCount:3
% 58.77/58.82 [1]P1(a1,a2)
% 58.77/58.82 [2]P2(a1,a3)
% 58.77/58.82 [3]~P2(a2,a3)
% 58.77/58.82 [4]~P3(x41,x41)
% 58.77/58.82 [5]~P4(x51,x51)
% 58.77/58.82 [6]~P5(x61,x61)
% 58.77/58.82 [7]~P6(x71,f4(x72,x71))
% 58.77/58.82 [8]~P6(x81,f5(x82,x81))
% 58.77/58.82 [9]~P5(f4(x91,x92),x91)
% 58.77/58.82 [10]~P11(f5(x101,x102),x101)
% 58.77/58.82 [11]P7(x111,x112)+P3(x111,x112)
% 58.77/58.82 [12]P8(x121,x122)+P4(x121,x122)
% 58.77/58.82 [14]P11(x141,x142)+P5(x141,x142)
% 58.77/58.82 [15]P1(x151,x152)+P5(x151,x152)
% 58.77/58.82 [16]P9(x161,x162)+P6(x161,x162)
% 58.77/58.82 [17]P2(x171,x172)+P11(x171,x172)
% 58.77/58.82 [18]~P4(x181,x182)+P5(x181,x182)
% 58.77/58.82 [21]~P7(x211,x212)+~P3(x211,x212)
% 58.77/58.82 [22]~P8(x221,x222)+~P4(x221,x222)
% 58.77/58.82 [23]~P1(x231,x232)+~P5(x231,x232)
% 58.77/58.82 [24]~P9(x241,x242)+~P6(x241,x242)
% 58.77/58.82 [25]~P2(x251,x252)+~P11(x251,x252)
% 58.77/58.82 [45]~P3(x451,x452)+~P6(x452,f7(x451,x452))
% 58.77/58.82 [46]~P3(x461,x462)+~P6(x461,f7(x461,x462))
% 58.77/58.82 [47]~P5(x471,x472)+~P6(f6(x471,x472),x472)
% 58.77/58.82 [48]~P5(x481,x482)+~P6(f6(x481,x482),x481)
% 58.77/58.82 [19]~P12(x192)+~P10(x191)+P10(f4(x191,x192))
% 58.77/58.82 [20]~P12(x202)+~P10(x201)+P10(f5(x201,x202))
% 58.77/58.82 [26]~P3(x263,x261)+P3(x261,x262)+P3(x263,x262)
% 58.77/58.82 [27]~P6(x271,x273)+P3(x271,x272)+P6(x272,x273)
% 58.77/58.82 [28]~P4(x283,x281)+P4(x281,x282)+P4(x283,x282)
% 58.77/58.82 [29]~P5(x293,x291)+P4(x291,x292)+P5(x293,x292)
% 58.77/58.82 [30]~P6(x303,x301)+P4(x301,x302)+P6(x303,x302)
% 58.77/58.82 [31]~P5(x313,x311)+P5(x311,x312)+P5(x313,x312)
% 58.77/58.82 [32]~P5(x323,x322)+P11(x321,x322)+P11(x321,x323)
% 58.77/58.82 [34]~P10(x342)+~P10(x341)+~P5(x341,x342)+P12(f6(x341,x342))
% 58.77/58.82 [35]~P12(x352)+~P12(x351)+~P3(x351,x352)+P10(f7(x351,x352))
% 58.77/58.82 [37]~P5(x371,x373)+~P11(x371,x373)+P5(x371,x372)+P11(x373,x372)
% 58.77/58.82 [38]~P5(x382,x383)+~P11(x382,x383)+P5(x381,x382)+P5(x381,x383)
% 58.77/58.82 [39]~P5(x392,x393)+~P11(x392,x393)+P5(x391,x392)+P11(x391,x393)
% 58.77/58.82 [40]~P5(x403,x401)+~P11(x403,x401)+P5(x401,x402)+P11(x403,x402)
% 58.77/58.82 [41]~P5(x413,x412)+~P11(x413,x412)+P5(x411,x412)+P11(x411,x413)
% 58.77/58.82 [42]~P5(x421,x423)+~P11(x421,x423)+P11(x421,x422)+P11(x423,x422)
% 58.77/58.82 [44]P11(x443,x444)+~P4(x443,x442)+P6(x441,x442)+P6(x441,x443)+P11(x442,x444)
% 58.77/58.82 [49]P6(x494,x493)+~P3(x494,x491)+~P4(x493,x492)+P6(x491,x492)+P6(x491,x493)+P6(x494,x492)
% 58.77/58.82 %EqnAxiom
% 58.77/58.82
% 58.77/58.82 %-------------------------------------------
% 58.80/58.85 cnf(56,plain,
% 58.80/58.85 (~P4(f4(x561,x562),x561)),
% 58.80/58.85 inference(scs_inference,[],[6,10,9,15,17,14,18])).
% 58.80/58.85 cnf(80,plain,
% 58.80/58.85 (~P5(x801,f4(x801,x802))),
% 58.80/58.85 inference(scs_inference,[],[6,56,8,9,15,12,16,14,29])).
% 58.80/58.85 cnf(83,plain,
% 58.80/58.85 (~P4(x831,f4(x831,x832))),
% 58.80/58.85 inference(scs_inference,[],[6,56,8,9,5,15,12,16,14,29,28])).
% 58.80/58.85 cnf(86,plain,
% 58.80/58.85 (~P6(x861,f4(f5(x862,x861),x863))),
% 58.80/58.85 inference(scs_inference,[],[6,56,8,9,5,15,12,16,14,29,28,30])).
% 58.80/58.85 cnf(99,plain,
% 58.80/58.85 (~P4(x991,f4(f4(x991,x992),x993))),
% 58.80/58.85 inference(scs_inference,[],[80,56,83,86,15,12,14,16,28])).
% 58.80/58.85 cnf(100,plain,
% 58.80/58.85 (~P4(f4(x1001,x1002),x1001)),
% 58.80/58.85 inference(rename_variables,[],[56])).
% 58.80/58.85 cnf(102,plain,
% 58.80/58.85 (~P5(x1021,f4(f4(x1021,x1022),x1023))),
% 58.80/58.85 inference(scs_inference,[],[80,56,100,83,86,15,12,14,16,28,29])).
% 58.80/58.85 cnf(103,plain,
% 58.80/58.85 (~P4(f4(x1031,x1032),x1031)),
% 58.80/58.85 inference(rename_variables,[],[56])).
% 58.80/58.85 cnf(105,plain,
% 58.80/58.85 (~P6(x1051,f4(f4(x1052,x1051),x1053))),
% 58.80/58.85 inference(scs_inference,[],[80,56,100,103,7,83,86,15,12,14,16,28,29,30])).
% 58.80/58.85 cnf(125,plain,
% 58.80/58.85 (~P5(f4(x1251,x1252),f4(x1251,x1253))),
% 58.80/58.85 inference(scs_inference,[],[102,56,9,99,105,15,12,16,14,29])).
% 58.80/58.85 cnf(205,plain,
% 58.80/58.85 (P11(a1,a2)),
% 58.80/58.85 inference(scs_inference,[],[1,23,14])).
% 58.80/58.85 cnf(2906,plain,
% 58.80/58.85 (~P4(a1,a2)+P5(f4(a2,x29061),a1)),
% 58.80/58.85 inference(scs_inference,[],[9,205,38,18])).
% 58.80/58.85 cnf(2908,plain,
% 58.80/58.85 (~P5(a1,f4(a2,x29081))+P5(f4(a2,x29082),a1)),
% 58.80/58.85 inference(scs_inference,[],[9,205,56,38,18,29])).
% 58.80/58.85 cnf(2968,plain,
% 58.80/58.85 (~P5(f4(a2,x29681),a1)+P5(f4(a2,x29682),a1)),
% 58.80/58.85 inference(scs_inference,[],[9,2906,29])).
% 58.80/58.85 cnf(3016,plain,
% 58.80/58.85 (P11(f4(a2,x30161),a1)+P5(f4(a2,x30162),a1)),
% 58.80/58.85 inference(scs_inference,[],[2968,14])).
% 58.80/58.85 cnf(3048,plain,
% 58.80/58.85 (~P2(f4(a2,x30481),a1)+P5(f4(a2,x30482),a1)),
% 58.80/58.85 inference(scs_inference,[],[3016,25])).
% 58.80/58.85 cnf(4286,plain,
% 58.80/58.85 (P4(x42861,f5(x42861,x42862))),
% 58.80/58.85 inference(scs_inference,[],[10,6,14,29])).
% 58.80/58.85 cnf(4304,plain,
% 58.80/58.85 (P5(x43041,f5(x43041,x43042))),
% 58.80/58.85 inference(scs_inference,[],[10,6,14,31])).
% 58.80/58.85 cnf(5264,plain,
% 58.80/58.85 (P4(f5(x52641,x52642),x52641)),
% 58.80/58.85 inference(scs_inference,[],[4286,5,28])).
% 58.80/58.85 cnf(5270,plain,
% 58.80/58.85 (P4(f5(x52701,x52702),f4(x52701,x52703))),
% 58.80/58.85 inference(scs_inference,[],[4286,83,28])).
% 58.80/58.85 cnf(8829,plain,
% 58.80/58.85 (P5(f5(x88291,x88292),x88291)),
% 58.80/58.85 inference(scs_inference,[],[5264,18])).
% 58.80/58.85 cnf(8837,plain,
% 58.80/58.85 (P5(f5(x88371,x88372),f4(x88371,x88373))),
% 58.80/58.85 inference(scs_inference,[],[5270,18])).
% 58.80/58.85 cnf(8936,plain,
% 58.80/58.85 (~P5(a1,a2)),
% 58.80/58.85 inference(scs_inference,[],[1,23])).
% 58.80/58.85 cnf(8938,plain,
% 58.80/58.85 (P5(f5(a1,x89381),a2)),
% 58.80/58.85 inference(scs_inference,[],[1,4304,23,31])).
% 58.80/58.85 cnf(8970,plain,
% 58.80/58.85 (P5(x89701,f4(f5(x89701,x89702),x89703))),
% 58.80/58.85 inference(scs_inference,[],[80,8829,31])).
% 58.80/58.85 cnf(8983,plain,
% 58.80/58.85 (P5(f4(x89831,x89832),f5(x89831,x89833))),
% 58.80/58.85 inference(scs_inference,[],[80,56,8837,31,29])).
% 58.80/58.85 cnf(8992,plain,
% 58.80/58.85 (P5(f4(f5(a1,x89921),x89922),a2)),
% 58.80/58.85 inference(scs_inference,[],[8936,8970,31])).
% 58.80/58.85 cnf(9018,plain,
% 58.80/58.85 (P5(a2,f4(f5(a1,x90181),x90182))),
% 58.80/58.85 inference(scs_inference,[],[125,8992,31])).
% 58.80/58.85 cnf(9022,plain,
% 58.80/58.85 (P5(a2,f5(a1,x90221))),
% 58.80/58.85 inference(scs_inference,[],[125,56,8992,31,29])).
% 58.80/58.85 cnf(9032,plain,
% 58.80/58.85 (P5(f4(f5(a1,x90321),x90322),f4(a2,x90323))),
% 58.80/58.85 inference(scs_inference,[],[80,9018,31])).
% 58.80/58.85 cnf(9045,plain,
% 58.80/58.85 (P5(f4(a2,x90451),f5(a1,x90452))),
% 58.80/58.85 inference(scs_inference,[],[125,56,9032,31,29])).
% 58.80/58.85 cnf(9055,plain,
% 58.80/58.85 (P5(f5(a1,x90551),f4(a2,x90552))),
% 58.80/58.85 inference(scs_inference,[],[125,9045,31])).
% 58.80/58.85 cnf(9162,plain,
% 58.80/58.85 (P11(a2,a3)),
% 58.80/58.85 inference(scs_inference,[],[3,17])).
% 58.80/58.85 cnf(11258,plain,
% 58.80/58.85 (~P4(a1,a2)),
% 58.80/58.85 inference(scs_inference,[],[8938,8936,23,18])).
% 58.80/58.85 cnf(11260,plain,
% 58.80/58.85 (~P11(a1,a3)),
% 58.80/58.85 inference(scs_inference,[],[2,8938,8936,23,18,25])).
% 58.80/58.85 cnf(11262,plain,
% 58.80/58.86 (~P5(f4(a2,x112621),a1)),
% 58.80/58.86 inference(scs_inference,[],[2,8938,8936,9,23,18,25,31])).
% 58.80/58.86 cnf(11265,plain,
% 58.80/58.86 (~P11(x112651,f5(x112651,x112652))),
% 58.80/58.86 inference(scs_inference,[],[2,8938,8936,9,4304,10,6,23,18,25,31,41])).
% 58.80/58.86 cnf(11269,plain,
% 58.80/58.86 (~P11(f4(x112691,x112692),f5(x112691,x112693))),
% 58.80/58.86 inference(scs_inference,[],[2,8938,8983,8936,9,4304,10,6,80,23,18,25,31,41,39])).
% 58.80/58.86 cnf(11272,plain,
% 58.80/58.86 (~P5(a1,f4(a2,x112721))),
% 58.80/58.86 inference(scs_inference,[],[2,8938,8983,8936,9,4304,10,6,80,23,18,25,31,41,39,2908])).
% 58.80/58.86 cnf(11280,plain,
% 58.80/58.86 (P5(a1,a3)),
% 58.80/58.86 inference(scs_inference,[],[2,8938,8983,8936,9,4304,10,6,80,23,18,25,31,41,39,2908,3016,3048,17,14])).
% 58.80/58.86 cnf(11308,plain,
% 58.80/58.86 (~P5(a2,a1)),
% 58.80/58.86 inference(scs_inference,[],[11258,11280,11269,11262,11272,6,15,17,23,18,29])).
% 58.80/58.86 cnf(11311,plain,
% 58.80/58.86 (~P5(f5(a1,x113111),a3)),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11269,11262,11272,6,15,17,23,18,29,32])).
% 58.80/58.86 cnf(11312,plain,
% 58.80/58.86 (~P11(x113121,f5(x113121,x113122))),
% 58.80/58.86 inference(rename_variables,[],[11265])).
% 58.80/58.86 cnf(11314,plain,
% 58.80/58.86 (~P5(f4(a2,x113141),f4(a1,x113142))),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11269,11262,11272,9,6,15,17,23,18,29,32,31])).
% 58.80/58.86 cnf(11317,plain,
% 58.80/58.86 (~P4(a2,a1)),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11269,11262,11272,5,9,6,15,17,23,18,29,32,31,28])).
% 58.80/58.86 cnf(11320,plain,
% 58.80/58.86 (~P11(f5(a1,x113201),f4(a2,x113202))),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11312,11269,11262,11272,9055,5,9,6,15,17,23,18,29,32,31,28,41])).
% 58.80/58.86 cnf(11323,plain,
% 58.80/58.86 (~P11(x113231,f5(x113231,x113232))),
% 58.80/58.86 inference(rename_variables,[],[11265])).
% 58.80/58.86 cnf(11325,plain,
% 58.80/58.86 (~P11(f5(a1,x113251),a2)),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11312,11269,11262,11272,9055,5,8938,9,10,6,15,17,23,18,29,32,31,28,41,40])).
% 58.80/58.86 cnf(11326,plain,
% 58.80/58.86 (~P11(f5(x113261,x113262),x113261)),
% 58.80/58.86 inference(rename_variables,[],[10])).
% 58.80/58.86 cnf(11328,plain,
% 58.80/58.86 (~P11(a2,f5(a1,x113281))),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11312,11323,11269,11262,11272,9055,5,9022,8938,8936,9,10,6,15,17,23,18,29,32,31,28,41,40,39])).
% 58.80/58.86 cnf(11332,plain,
% 58.80/58.86 (~P11(f4(a2,x113321),f5(a1,x113322))),
% 58.80/58.86 inference(scs_inference,[],[11258,11260,11280,11265,11312,11323,11269,11262,11272,9055,5,9022,9045,8938,8936,9,10,11326,6,15,17,23,18,29,32,31,28,41,40,39,37])).
% 58.80/58.86 cnf(11353,plain,
% 58.80/58.86 (~P4(f4(a2,x113531),f4(a1,x113532))),
% 58.80/58.86 inference(scs_inference,[],[11308,11317,11314,11320,9055,15,12,17,23,18])).
% 58.80/58.86 cnf(11355,plain,
% 58.80/58.86 (~P5(a2,f4(a1,x113551))),
% 58.80/58.86 inference(scs_inference,[],[11308,11317,11314,11320,9055,56,15,12,17,23,18,29])).
% 58.80/58.86 cnf(11356,plain,
% 58.80/58.86 (~P4(f4(x113561,x113562),x113561)),
% 58.80/58.86 inference(rename_variables,[],[56])).
% 58.80/58.86 cnf(11358,plain,
% 58.80/58.86 (~P5(f4(a1,x113581),a2)),
% 58.80/58.86 inference(scs_inference,[],[11308,11317,11314,11320,9055,9,56,15,12,17,23,18,29,31])).
% 58.80/58.86 cnf(11359,plain,
% 58.80/58.86 (~P5(f4(x113591,x113592),x113591)),
% 58.80/58.86 inference(rename_variables,[],[9])).
% 58.80/58.86 cnf(11361,plain,
% 58.80/58.86 (~P4(a2,f4(a1,x113611))),
% 58.80/58.86 inference(scs_inference,[],[11308,11317,11314,11320,9055,9,56,11356,15,12,17,23,18,29,31,28])).
% 58.80/58.86 cnf(11365,plain,
% 58.80/58.86 (P5(f5(x113651,x113652),f4(x113651,x113653))),
% 58.80/58.86 inference(rename_variables,[],[8837])).
% 58.80/58.86 cnf(11368,plain,
% 58.80/58.86 (~P11(f5(x113681,x113682),f4(x113681,x113683))),
% 58.80/58.86 inference(scs_inference,[],[11308,11317,11314,11320,11332,8837,11365,9055,9,11359,56,11356,10,15,12,17,23,18,29,31,28,41,40])).
% 58.80/58.86 cnf(11399,plain,
% 58.80/58.86 (~P5(a2,a3)),
% 58.80/58.86 inference(scs_inference,[],[11368,11353,11355,11358,11325,11311,8983,83,125,9162,15,12,17,23,18,29,28,41])).
% 58.80/58.86 cnf(11423,plain,
% 58.80/58.86 (~P4(a2,a3)),
% 58.80/58.86 inference(scs_inference,[],[11399,11361,11328,9022,15,17,12,23,18])).
% 58.80/58.86 cnf(11425,plain,
% 58.80/58.86 (~P5(f5(a1,x114251),f5(a2,x114252))),
% 58.80/58.86 inference(scs_inference,[],[11399,11361,11328,11265,9022,15,17,12,23,18,32])).
% 58.80/58.86 cnf(11447,plain,
% 58.80/58.86 ($false),
% 58.80/58.86 inference(scs_inference,[],[11423,11425,11332,11311,8938,9045,15,18,12,17,23,29]),
% 58.80/58.86 ['proof']).
% 58.80/58.86 % SZS output end Proof
% 58.80/58.86 % Total time :58.110000s
%------------------------------------------------------------------------------