%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO255+1 : TPTP v8.2.0. Bugfixed v6.4.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:58 EDT 2024
% Result : Theorem 58.59s 58.74s
% Output : CNFRefutation 58.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO255+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/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 10:15:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 58.59/58.72 %-------------------------------------------
% 58.59/58.72 % File :CSE---1.7
% 58.59/58.72 % Problem :theBenchmark
% 58.59/58.72 % Transform :cnf
% 58.59/58.72 % Format :tptp:raw
% 58.59/58.72 % Command :java -jar mcs_scs.jar %d %s
% 58.59/58.72
% 58.59/58.72 % Result :Theorem 58.030000s
% 58.59/58.72 % Output :CNFRefutation 58.030000s
% 58.59/58.72 %-------------------------------------------
% 58.59/58.74 %------------------------------------------------------------------------------
% 58.59/58.74 % File : GEO255+1 : TPTP v8.2.0. Bugfixed v6.4.0.
% 58.59/58.74 % Domain : Geometry (Constructive)
% 58.59/58.74 % Problem : Property of order and betweeness
% 58.59/58.74 % Version : [vPl98] axioms : Especial.
% 58.59/58.74 % English :
% 58.59/58.74
% 58.59/58.74 % Refs : [vPl98] von Plato (1998), A Constructive Theory of Ordered Aff
% 58.59/58.74 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.59/58.74 % Source : [ILTP]
% 58.59/58.74 % Names : Theorem 6.2.i [vPl98]
% 58.59/58.74
% 58.59/58.74 % Status : Theorem
% 58.59/58.74 % Rating : 0.06 v8.2.0, 0.07 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.00 v6.4.0
% 58.59/58.74 % Syntax : Number of formulae : 32 ( 7 unt; 0 def)
% 58.59/58.74 % Number of atoms : 106 ( 0 equ)
% 58.59/58.74 % Maximal formula atoms : 10 ( 3 avg)
% 58.59/58.74 % Number of connectives : 91 ( 17 ~; 24 |; 27 &)
% 58.59/58.74 % ( 5 <=>; 18 =>; 0 <=; 0 <~>)
% 58.59/58.74 % Maximal formula depth : 13 ( 6 avg)
% 58.59/58.74 % Maximal term depth : 3 ( 1 avg)
% 58.59/58.74 % Number of predicates : 12 ( 12 usr; 0 prp; 1-4 aty)
% 58.59/58.74 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% 58.59/58.74 % Number of variables : 74 ( 74 !; 0 ?)
% 58.59/58.74 % SPC : FOF_THM_RFO_NEQ
% 58.59/58.74
% 58.59/58.74 % Comments : Definitions unfolded, hence Especial.
% 58.59/58.74 % Bugfixes : v6.4.0 - Bugfix in GEO007+1.ax, fixed conjecture.
% 58.59/58.74 %------------------------------------------------------------------------------
% 58.59/58.74 include('Axioms/GEO007+0.ax').
% 58.59/58.74 %------------------------------------------------------------------------------
% 58.59/58.74 fof(con,conjecture,
% 58.59/58.74 ! [L,A,B] :
% 58.59/58.74 ( ( line(L)
% 58.59/58.74 & distinct_points(A,B) )
% 58.59/58.74 => ~ ( before_on_line(L,A,B)
% 58.59/58.74 & before_on_line(L,B,A) ) ) ).
% 58.59/58.74
% 58.59/58.74 %------------------------------------------------------------------------------
% 58.59/58.74 %-------------------------------------------
% 58.59/58.74 % Proof found
% 58.59/58.74 % SZS status Theorem for theBenchmark
% 58.59/58.74 % SZS output start Proof
% 58.59/58.75 %ClaNum:62(EqnAxiom:0)
% 58.59/58.75 %VarNum:269(SingletonVarNum:105)
% 58.59/58.75 %MaxLitNum:10
% 58.59/58.75 %MaxfuncDepth:2
% 58.59/58.75 %SharedTerms:7
% 58.59/58.75 %goalClause: 1 2 3 4
% 58.59/58.75 %singleGoalClaCount:4
% 58.59/58.75 [1]P1(a1)
% 58.59/58.75 [2]P2(a2,a3)
% 58.59/58.75 [3]P3(a1,a2,a3)
% 58.59/58.75 [4]P3(a1,a3,a2)
% 58.59/58.75 [6]~P11(x61,x61)
% 58.59/58.75 [7]~P2(x71,x71)
% 58.59/58.75 [8]~P5(x81,x81)
% 58.59/58.75 [11]~P5(x111,f4(x111))
% 58.59/58.75 [5]~P8(x51,x52)
% 58.59/58.75 [9]~P10(x91,x92)
% 58.59/58.75 [13]~P4(x131,f5(x132,x131))
% 58.59/58.75 [14]~P11(f5(x141,x142),x141)
% 58.59/58.75 [15]~P11(f6(x151,x152),f4(f6(x152,x151)))
% 58.59/58.75 [16]~P1(x161)+P1(f4(x161))
% 58.59/58.75 [18]~P6(x181,x182)+P11(x181,x182)
% 58.59/58.75 [19]~P6(x191,x192)+P11(x191,f4(x192))
% 58.59/58.75 [33]~P2(x331,x332)+~P4(x332,f6(x331,x332))
% 58.59/58.75 [34]~P2(x341,x342)+~P4(x341,f6(x341,x342))
% 58.59/58.75 [41]P2(x411,x412)+~P3(x413,x411,x412)
% 58.59/58.75 [54]~P3(x541,x542,x543)+~P11(x541,f6(x542,x543))
% 58.59/58.75 [20]~P1(x201)+~P12(x202)+P1(f5(x201,x202))
% 58.59/58.75 [28]~P4(x281,x282)+P8(x281,x282)+P8(x281,f4(x282))
% 58.59/58.75 [30]~P11(x301,x302)+P6(x301,x302)+~P11(x301,f4(x302))
% 58.59/58.75 [49]~P11(x491,x492)+~P11(x491,f4(x492))+~P4(f7(x491,x492),x492)
% 58.59/58.75 [50]~P11(x501,x502)+~P11(x501,f4(x502))+~P4(f7(x501,x502),x501)
% 58.59/58.75 [24]~P11(x243,x241)+P11(x241,x242)+P11(x243,x242)
% 58.59/58.75 [26]~P2(x263,x261)+P2(x261,x262)+P2(x263,x262)
% 58.59/58.75 [27]~P5(x273,x271)+P5(x271,x272)+P5(x273,x272)
% 58.59/58.75 [46]~P9(x462,x461,x463)+P8(x461,x462)+P8(x463,x462)
% 58.59/58.75 [51]P8(x511,x512)+~P9(x512,x513,x511)+P8(x511,f4(x512))
% 58.59/58.75 [52]P8(x521,x522)+~P9(x522,x521,x523)+P8(x521,f4(x522))
% 58.59/58.75 [53]~P9(x532,x533,x531)+P8(x531,f4(x532))+P8(x533,f4(x532))
% 58.59/58.75 [57]~P3(x571,x573,x572)+~P3(x571,x574,x573)+P7(x571,x572,x573,x574)
% 58.59/58.75 [58]~P3(x581,x583,x584)+~P3(x581,x582,x583)+P7(x581,x582,x583,x584)
% 58.59/58.75 [59]~P7(x591,x592,x593,x594)+P3(x591,x592,x593)+P3(x591,x594,x593)
% 58.59/58.75 [60]P3(x601,x603,x602)+P3(x601,x602,x603)+~P7(x601,x604,x602,x603)
% 58.59/58.75 [61]P3(x611,x613,x612)+P3(x611,x612,x613)+~P7(x611,x612,x613,x614)
% 58.59/58.75 [62]~P7(x621,x624,x622,x623)+P3(x621,x622,x623)+P3(x621,x622,x624)
% 58.59/58.75 [22]~P1(x222)+~P1(x221)+P11(x221,x222)+P11(x221,f4(x222))
% 58.59/58.75 [29]~P12(x292)+~P12(x291)+~P2(x291,x292)+P1(f6(x291,x292))
% 58.59/58.75 [37]~P11(x371,x372)+P10(x371,x372)+P10(x371,f4(x372))+~P11(x371,f4(x372))
% 58.59/58.75 [35]~P11(x351,x353)+P11(x351,x352)+~P11(x351,f4(x353))+P11(x353,f4(x352))
% 58.59/58.75 [36]~P11(x363,x361)+P11(x361,x362)+~P11(x363,f4(x361))+P11(x363,f4(x362))
% 58.59/58.75 [39]~P1(x392)+~P1(x391)+~P11(x391,x392)+~P11(x391,f4(x392))+P12(f7(x391,x392))
% 58.59/58.75 [56]P3(x562,x563,x561)+~P2(x563,x561)+P8(x561,x562)+P8(x563,x562)+P8(x561,f4(x562))+P8(x563,f4(x562))+P11(x562,f6(x563,x561))
% 58.59/58.75 [55]P8(x554,x553)+~P2(x554,x551)+~P5(x553,x552)+P8(x551,x552)+P8(x551,x553)+P8(x554,x552)+P8(x551,f4(x552))+P8(x551,f4(x553))+P8(x554,f4(x552))+P8(x554,f4(x553))
% 58.59/58.75 %EqnAxiom
% 58.59/58.75
% 58.59/58.75 %-------------------------------------------
% 58.76/58.84 cnf(63,plain,
% 58.76/58.84 (~P3(x631,x632,x632)),
% 58.76/58.84 inference(scs_inference,[],[7,41])).
% 58.76/58.84 cnf(99,plain,
% 58.76/58.84 (P11(f4(a1),a1)+~P1(f4(a1))),
% 58.76/58.84 inference(scs_inference,[],[1,63,6,14,18,19,62,60,61,22])).
% 58.76/58.84 cnf(413,plain,
% 58.76/58.84 (P11(f4(a1),a1)),
% 58.76/58.84 inference(scs_inference,[],[1,99,16])).
% 58.76/58.84 cnf(414,plain,
% 58.76/58.84 (P11(a1,f4(a1))),
% 58.76/58.84 inference(scs_inference,[],[6,413,24])).
% 58.76/58.84 cnf(13847,plain,
% 58.76/58.84 (P11(a1,a1)+~P11(a1,f4(f4(a1)))),
% 58.76/58.84 inference(scs_inference,[],[6,414,35])).
% 58.76/58.84 cnf(13863,plain,
% 58.76/58.84 (~P11(a1,f4(f4(a1)))),
% 58.76/58.84 inference(scs_inference,[],[6,13847])).
% 58.76/58.84 cnf(26736,plain,
% 58.76/58.84 (P11(f4(a1),f4(f4(a1)))),
% 58.76/58.84 inference(scs_inference,[],[13863,414,24])).
% 58.76/58.84 cnf(26742,plain,
% 58.76/58.84 (P11(f4(f4(a1)),f4(a1))),
% 58.76/58.84 inference(scs_inference,[],[6,26736,24])).
% 58.76/58.84 cnf(26755,plain,
% 58.76/58.84 (P10(f4(f4(a1)),a1)+~P11(f4(f4(a1)),a1)),
% 58.76/58.84 inference(scs_inference,[],[26742,9,37])).
% 58.76/58.84 cnf(26762,plain,
% 58.76/58.84 (~P11(f4(f4(a1)),a1)),
% 58.76/58.84 inference(scs_inference,[],[9,26755])).
% 58.76/58.84 cnf(29034,plain,
% 58.76/58.84 (~P11(f4(a1),f5(a1,x290341))+~P11(f4(a1),f4(f5(a1,x290341)))),
% 58.76/58.84 inference(scs_inference,[],[26762,6,14,24,19,18,35])).
% 58.76/58.84 cnf(29073,plain,
% 58.76/58.84 (P11(a1,f4(f5(a1,x290731)))+~P11(f4(a1),f5(a1,x290731))),
% 58.76/58.84 inference(scs_inference,[],[413,29034,24])).
% 58.76/58.84 cnf(29134,plain,
% 58.76/58.84 (P11(a1,f5(a1,x291341))+P11(a1,f4(f5(a1,x291341)))),
% 58.76/58.84 inference(scs_inference,[],[413,29073,24])).
% 58.76/58.84 cnf(29195,plain,
% 58.76/58.84 (P11(f4(f5(a1,x291951)),a1)+P11(a1,f5(a1,x291951))),
% 58.76/58.84 inference(scs_inference,[],[6,29134,24])).
% 58.76/58.84 cnf(88999,plain,
% 58.76/58.84 (P1(f4(a1))),
% 58.76/58.84 inference(scs_inference,[],[1,16])).
% 58.76/58.84 cnf(89001,plain,
% 58.76/58.84 (~P11(a1,f6(a3,a2))),
% 58.76/58.84 inference(scs_inference,[],[1,4,16,54])).
% 58.76/58.84 cnf(89009,plain,
% 58.76/58.84 (~P11(f4(f4(a1)),f5(a1,x890091))),
% 58.76/58.84 inference(scs_inference,[],[1,4,3,26762,14,16,54,57,58,20,24])).
% 58.76/58.84 cnf(89014,plain,
% 58.76/58.84 (~P11(a1,f6(a2,a3))),
% 58.76/58.84 inference(scs_inference,[],[3,54])).
% 58.76/58.84 cnf(89024,plain,
% 58.76/58.84 (P11(a1,f4(f5(a1,x890241)))),
% 58.76/58.84 inference(scs_inference,[],[88999,89009,26736,3,14,6,54,16,24,36,29073])).
% 58.76/58.84 cnf(89028,plain,
% 58.76/58.84 (P11(f4(a1),f6(a2,a3))),
% 58.76/58.84 inference(scs_inference,[],[89014,413,24])).
% 58.76/58.84 cnf(89036,plain,
% 58.76/58.84 (P11(f4(a1),f4(f6(a3,a2)))),
% 58.76/58.84 inference(scs_inference,[],[89028,15,24])).
% 58.76/58.84 cnf(89042,plain,
% 58.76/58.84 (P10(a1,f4(f5(a1,x890421)))+P11(f4(f5(a1,x890421)),a1)),
% 58.76/58.84 inference(scs_inference,[],[89028,89024,15,9,24,37,29195])).
% 58.76/58.84 cnf(89047,plain,
% 58.76/58.84 (~P10(x890471,x890472)),
% 58.76/58.84 inference(rename_variables,[],[9])).
% 58.76/58.84 cnf(89050,plain,
% 58.76/58.84 (P10(f4(a1),f4(f6(a3,a2)))),
% 58.76/58.84 inference(scs_inference,[],[89001,89036,413,9,89047,89042,24,37])).
% 58.76/58.84 cnf(89062,plain,
% 58.76/58.84 ($false),
% 58.76/58.84 inference(scs_inference,[],[89050,9]),
% 58.76/58.84 ['proof']).
% 58.84/58.93 % SZS output end Proof
% 58.84/58.93 % Total time :58.030000s
%------------------------------------------------------------------------------