%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO258+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 : n028.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:59 EDT 2024
% Result : Theorem 58.69s 58.70s
% Output : CNFRefutation 58.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO258+3 : TPTP v8.2.0. Released v4.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 09:47:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.41/0.61 start to proof:theBenchmark
% 58.68/58.68 %-------------------------------------------
% 58.68/58.68 % File :CSE---1.7
% 58.68/58.68 % Problem :theBenchmark
% 58.68/58.68 % Transform :cnf
% 58.68/58.68 % Format :tptp:raw
% 58.68/58.68 % Command :java -jar mcs_scs.jar %d %s
% 58.68/58.68
% 58.68/58.68 % Result :Theorem 58.040000s
% 58.68/58.68 % Output :CNFRefutation 58.040000s
% 58.68/58.69 %-------------------------------------------
% 58.69/58.70 %------------------------------------------------------------------------------
% 58.69/58.70 % File : GEO258+3 : TPTP v8.2.0. Released v4.0.0.
% 58.69/58.70 % Domain : Geometry (Constructive)
% 58.69/58.70 % Problem : Betweeness
% 58.69/58.70 % Version : [vPl98] axioms.
% 58.69/58.70 % English :
% 58.69/58.70
% 58.69/58.70 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 58.69/58.70 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.69/58.70 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.69/58.70 % Source : [Rat07]
% 58.69/58.70 % Names : Theorem 6.4.i [vPl98]
% 58.69/58.70
% 58.69/58.70 % Status : Theorem
% 58.69/58.70 % Rating : 0.00 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 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.69/58.70 % Syntax : Number of formulae : 37 ( 6 unt; 0 def)
% 58.69/58.70 % Number of atoms : 111 ( 0 equ)
% 58.69/58.70 % Maximal formula atoms : 10 ( 3 avg)
% 58.69/58.70 % Number of connectives : 86 ( 12 ~; 22 |; 24 &)
% 58.69/58.70 % ( 10 <=>; 18 =>; 0 <=; 0 <~>)
% 58.69/58.70 % Maximal formula depth : 13 ( 5 avg)
% 58.69/58.70 % Maximal term depth : 3 ( 1 avg)
% 58.69/58.70 % Number of predicates : 18 ( 18 usr; 0 prp; 1-4 aty)
% 58.69/58.70 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 58.69/58.70 % Number of variables : 85 ( 85 !; 0 ?)
% 58.69/58.70 % SPC : FOF_THM_RFO_NEQ
% 58.69/58.70
% 58.69/58.70 % Comments :
% 58.69/58.70 %------------------------------------------------------------------------------
% 58.69/58.70 include('Axioms/GEO009+0.ax').
% 58.69/58.70 %------------------------------------------------------------------------------
% 58.69/58.70 fof(con,conjecture,
% 58.69/58.70 ! [L,A,B,C] :
% 58.69/58.70 ( between_on_line(L,A,B,C)
% 58.69/58.70 => between_on_line(L,C,B,A) ) ).
% 58.69/58.70
% 58.69/58.70 %------------------------------------------------------------------------------
% 58.69/58.70 %-------------------------------------------
% 58.69/58.70 % Proof found
% 58.69/58.70 % SZS status Theorem for theBenchmark
% 58.69/58.70 % SZS output start Proof
% 58.72/58.72 %ClaNum:68(EqnAxiom:0)
% 58.72/58.72 %VarNum:311(SingletonVarNum:129)
% 58.72/58.72 %MaxLitNum:10
% 58.72/58.72 %MaxfuncDepth:2
% 58.72/58.72 %SharedTerms:6
% 58.72/58.72 %goalClause: 3 12
% 58.72/58.72 %singleGoalClaCount:2
% 58.72/58.72 [3]P2(a2,a3,a4,a5)
% 58.72/58.72 [12]~P2(a2,a5,a4,a3)
% 58.72/58.72 [1]P1(x11,x11)
% 58.72/58.72 [6]~P5(x61,x61)
% 58.72/58.72 [7]~P6(x71,x71)
% 58.72/58.72 [10]~P6(x101,f8(x101))
% 58.72/58.72 [4]~P9(x41,x42)
% 58.72/58.72 [5]~P12(x51,x52)
% 58.72/58.72 [2]P1(f1(x21,x22),x21)
% 58.72/58.72 [11]~P3(x111,f1(x112,x111))
% 58.72/58.72 [13]~P13(x131)+P13(f8(x131))
% 58.72/58.72 [14]P10(x141,x142)+P14(x141,x142)
% 58.72/58.72 [15]P1(x151,x152)+P15(x151,x152)
% 58.72/58.72 [17]~P7(x171,x172)+P14(x171,x172)
% 58.72/58.72 [18]~P7(x181,x182)+P15(x181,x182)
% 58.72/58.72 [19]~P16(x191,x192)+P3(x191,x192)
% 58.72/58.72 [25]~P10(x251,x252)+~P14(x251,x252)
% 58.72/58.72 [26]~P1(x261,x262)+~P15(x261,x262)
% 58.72/58.72 [16]P15(x161,x162)+P15(x161,f8(x162))
% 58.72/58.72 [21]~P14(x211,x212)+P15(x211,f8(x212))
% 58.72/58.72 [22]~P16(x221,x222)+P9(x221,f8(x222))
% 58.72/58.72 [23]~P18(x231,x232)+P12(x231,f8(x232))
% 58.72/58.72 [27]P14(x271,x272)+~P15(x271,f8(x272))
% 58.72/58.72 [40]~P5(x401,x402)+~P3(x402,f6(x401,x402))
% 58.72/58.72 [41]~P5(x411,x412)+~P3(x411,f6(x411,x412))
% 58.72/58.72 [59]~P5(x591,x592)+P1(f6(x591,x592),f8(f6(x592,x591)))
% 58.72/58.72 [50]P5(x501,x502)+~P4(x503,x501,x502)
% 58.72/58.72 [51]P11(x511,x512)+~P4(x512,x513,x511)
% 58.72/58.72 [52]P11(x521,x522)+~P4(x522,x521,x523)
% 58.72/58.72 [60]~P4(x601,x602,x603)+P1(x601,f6(x602,x603))
% 58.72/58.72 [32]P9(x321,x322)+~P3(x321,x322)+P16(x321,x322)
% 58.72/58.72 [36]~P14(x361,x362)+~P15(x361,x362)+P7(x361,x362)
% 58.72/58.72 [24]~P17(x242)+~P13(x241)+P13(f1(x241,x242))
% 58.72/58.72 [57]~P15(x571,x572)+~P15(x571,f8(x572))+~P3(f7(x571,x572),x572)
% 58.72/58.72 [58]~P15(x581,x582)+~P15(x581,f8(x582))+~P3(f7(x581,x582),x581)
% 58.72/58.72 [30]~P15(x303,x301)+P15(x301,x302)+P15(x303,x302)
% 58.72/58.72 [34]~P5(x343,x341)+P5(x341,x342)+P5(x343,x342)
% 58.72/58.72 [35]~P6(x353,x351)+P6(x351,x352)+P6(x353,x352)
% 58.72/58.72 [53]~P8(x532,x533,x531)+P16(x531,x532)+P16(x533,x532)
% 58.72/58.72 [54]P9(x541,x542)+P16(x541,x542)+~P8(x542,x543,x541)
% 58.72/58.72 [55]P9(x551,x552)+P16(x551,x552)+~P8(x552,x551,x553)
% 58.72/58.72 [56]~P8(x562,x561,x563)+P9(x561,x562)+P9(x563,x562)
% 58.72/58.72 [63]~P4(x631,x633,x632)+~P4(x631,x634,x633)+P2(x631,x632,x633,x634)
% 58.72/58.72 [64]~P4(x641,x643,x644)+~P4(x641,x642,x643)+P2(x641,x642,x643,x644)
% 58.72/58.72 [65]~P2(x651,x652,x653,x654)+P4(x651,x652,x653)+P4(x651,x654,x653)
% 58.72/58.72 [66]P4(x661,x663,x662)+P4(x661,x662,x663)+~P2(x661,x664,x662,x663)
% 58.72/58.72 [67]P4(x671,x673,x672)+P4(x671,x672,x673)+~P2(x671,x672,x673,x674)
% 58.72/58.72 [68]~P2(x681,x684,x682,x683)+P4(x681,x682,x683)+P4(x681,x682,x684)
% 58.72/58.72 [37]~P17(x372)+~P17(x371)+~P5(x371,x372)+P13(f6(x371,x372))
% 58.72/58.72 [44]~P15(x441,x442)+P12(x441,x442)+P12(x441,f8(x442))+~P15(x441,f8(x442))
% 58.72/58.72 [42]~P15(x421,x423)+P15(x421,x422)+~P15(x421,f8(x423))+P15(x423,f8(x422))
% 58.72/58.72 [43]~P15(x433,x431)+P15(x431,x432)+~P15(x433,f8(x431))+P15(x433,f8(x432))
% 58.72/58.72 [46]~P13(x462)+~P13(x461)+~P15(x461,x462)+~P15(x461,f8(x462))+P17(f7(x461,x462))
% 58.72/58.72 [62]~P5(x622,x623)+~P11(x623,x621)+~P11(x622,x621)+P4(x621,x622,x623)+~P1(x621,f6(x622,x623))
% 58.72/58.72 [61]P9(x614,x613)+~P5(x614,x611)+~P6(x613,x612)+P9(x611,x612)+P9(x611,x613)+P9(x614,x612)+P9(x611,f8(x612))+P9(x611,f8(x613))+P9(x614,f8(x612))+P9(x614,f8(x613))
% 58.72/58.72 %EqnAxiom
% 58.72/58.72
% 58.72/58.72 %-------------------------------------------
% 58.72/58.76 cnf(73,plain,
% 58.72/58.76 (~P16(x731,x732)),
% 58.72/58.76 inference(scs_inference,[],[6,4,11,50,19,22])).
% 58.72/58.76 cnf(82,plain,
% 58.72/58.76 (~P4(a2,a4,a5)+~P4(a2,a3,a4)),
% 58.72/58.76 inference(scs_inference,[],[12,6,4,11,50,19,22,65,66,67,63])).
% 58.72/58.76 cnf(89,plain,
% 58.72/58.76 (~P4(a2,a4,a3)+~P4(a2,a5,a4)),
% 58.72/58.76 inference(scs_inference,[],[12,64])).
% 58.72/58.76 cnf(93,plain,
% 58.72/58.76 (~P2(a2,a3,a4,a3)+~P4(a2,a5,a4)),
% 58.72/58.76 inference(scs_inference,[],[12,64,65,67,68])).
% 58.72/58.76 cnf(96,plain,
% 58.72/58.76 (P12(x961,x962)+~P15(x961,x962)+~P4(a2,a5,a4)+~P15(x961,f8(x962))),
% 58.72/58.76 inference(scs_inference,[],[12,5,64,65,68,44])).
% 58.72/58.76 cnf(243,plain,
% 58.72/58.76 (P10(x2431,x2432)+P15(x2431,f8(x2432))),
% 58.72/58.76 inference(scs_inference,[],[14,21])).
% 58.72/58.76 cnf(623,plain,
% 58.72/58.76 (P15(x6231,f8(x6231))),
% 58.72/58.76 inference(scs_inference,[],[1,16,26])).
% 58.72/58.76 cnf(1366,plain,
% 58.72/58.76 (~P4(a2,a5,a4)+P4(a2,a3,a4)),
% 58.72/58.76 inference(scs_inference,[],[3,89,67])).
% 58.72/58.76 cnf(2002,plain,
% 58.72/58.76 (P4(a2,a4,a5)+~P2(a2,a3,a4,a3)),
% 58.72/58.76 inference(scs_inference,[],[3,93,66])).
% 58.72/58.76 cnf(2719,plain,
% 58.72/58.76 (~P4(a2,a3,a4)+~P2(a2,a3,a4,a3)),
% 58.72/58.76 inference(scs_inference,[],[12,2002,63])).
% 58.72/58.76 cnf(3926,plain,
% 58.72/58.76 (P15(f8(x39261),x39261)),
% 58.72/58.76 inference(scs_inference,[],[623,1,30,26])).
% 58.72/58.76 cnf(6335,plain,
% 58.72/58.76 (P12(f8(f8(x63351)),x63351)+~P15(f8(f8(x63351)),x63351)),
% 58.72/58.76 inference(scs_inference,[],[10,3926,623,5,7,35,58,44])).
% 58.72/58.76 cnf(6342,plain,
% 58.72/58.76 (~P15(f8(f8(x63421)),x63421)),
% 58.72/58.76 inference(scs_inference,[],[5,6335])).
% 58.72/58.76 cnf(21097,plain,
% 58.72/58.76 (~P15(x210971,x210971)),
% 58.72/58.76 inference(scs_inference,[],[1,623,57,26])).
% 58.72/58.76 cnf(21105,plain,
% 58.72/58.76 (~P15(f1(x211051,x211052),x211051)),
% 58.72/58.76 inference(scs_inference,[],[2,21097,18,26])).
% 58.72/58.76 cnf(21107,plain,
% 58.72/58.76 (P15(f8(f1(x211071,x211072)),x211071)),
% 58.72/58.76 inference(scs_inference,[],[2,21097,623,18,26,30])).
% 58.72/58.76 cnf(21130,plain,
% 58.72/58.76 (P15(x211301,f8(f1(x211301,x211302)))),
% 58.72/58.76 inference(scs_inference,[],[21097,21107,30])).
% 58.72/58.76 cnf(24884,plain,
% 58.72/58.76 (~P15(f1(x248841,x248842),f8(f8(x248841)))),
% 58.72/58.76 inference(scs_inference,[],[21105,21097,16,42])).
% 58.72/58.76 cnf(33137,plain,
% 58.72/58.76 (P12(x331371,f1(x331371,x331372))+~P15(x331371,f1(x331371,x331372))),
% 58.72/58.76 inference(scs_inference,[],[21130,5,57,58,44])).
% 58.72/58.76 cnf(33144,plain,
% 58.72/58.76 (~P15(x331441,f1(x331441,x331442))),
% 58.72/58.76 inference(scs_inference,[],[5,33137])).
% 58.72/58.76 cnf(40658,plain,
% 58.72/58.76 (~P15(f1(f1(x406581,x406582),x406583),x406581)),
% 58.72/58.76 inference(scs_inference,[],[21105,33144,30])).
% 58.72/58.76 cnf(40667,plain,
% 58.72/58.76 (~P15(f1(x406671,x406672),f1(f1(x406671,x406673),x406674))),
% 58.72/58.76 inference(scs_inference,[],[21105,40658,30])).
% 58.72/58.76 cnf(47292,plain,
% 58.72/58.76 (~P15(f1(f1(x472921,x472922),x472923),f1(x472921,x472924))),
% 58.72/58.76 inference(scs_inference,[],[40658,21105,30])).
% 58.72/58.76 cnf(47306,plain,
% 58.72/58.76 (P15(f1(f1(x473061,x473062),x473063),f8(x473061))),
% 58.72/58.76 inference(scs_inference,[],[40658,6342,30,243,16])).
% 58.72/58.76 cnf(52452,plain,
% 58.72/58.76 (P15(f8(x524521),f1(x524521,x524522))),
% 58.72/58.76 inference(scs_inference,[],[47292,47306,73,15,30])).
% 58.72/58.76 cnf(52458,plain,
% 58.72/58.76 (P4(a2,a3,a4)),
% 58.72/58.76 inference(scs_inference,[],[3,47292,47306,73,15,30,65,89,1366])).
% 58.72/58.76 cnf(52463,plain,
% 58.72/58.76 (~P4(a2,a4,a5)),
% 58.72/58.76 inference(scs_inference,[],[52458,82])).
% 58.72/58.76 cnf(52466,plain,
% 58.72/58.76 (~P2(a2,a3,a4,a3)),
% 58.72/58.76 inference(scs_inference,[],[52458,2719])).
% 58.72/58.76 cnf(52483,plain,
% 58.72/58.76 (~P15(f8(x524831),f8(f1(x524831,x524832)))),
% 58.72/58.76 inference(scs_inference,[],[52458,52452,40667,33144,24884,21097,5,4,52,60,15,26,30,16,96,42])).
% 58.72/58.76 cnf(52501,plain,
% 58.72/58.76 ($false),
% 58.72/58.76 inference(scs_inference,[],[3,52463,52466,52483,52458,73,15,64,68]),
% 58.72/58.76 ['proof']).
% 58.72/58.79 % SZS output end Proof
% 58.72/58.79 % Total time :58.040000s
%------------------------------------------------------------------------------