%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO204+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 : n019.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:30 EDT 2024
% Result : Theorem 58.69s 58.72s
% Output : CNFRefutation 58.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO204+3 : TPTP v8.2.0. Released v4.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.34 % Computer : n019.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri Jun 21 09:55:39 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.47/0.60 start to proof:theBenchmark
% 58.69/58.70 %-------------------------------------------
% 58.69/58.70 % File :CSE---1.7
% 58.69/58.70 % Problem :theBenchmark
% 58.69/58.70 % Transform :cnf
% 58.69/58.70 % Format :tptp:raw
% 58.69/58.70 % Command :java -jar mcs_scs.jar %d %s
% 58.69/58.70
% 58.69/58.70 % Result :Theorem 58.050000s
% 58.69/58.70 % Output :CNFRefutation 58.050000s
% 58.69/58.70 %-------------------------------------------
% 58.69/58.71 %------------------------------------------------------------------------------
% 58.69/58.71 % File : GEO204+3 : TPTP v8.2.0. Released v4.0.0.
% 58.69/58.71 % Domain : Geometry (Constructive)
% 58.69/58.71 % Problem : Distinct points and equal lines
% 58.69/58.71 % Version : [vPl95] axioms.
% 58.69/58.71 % English : If the points X and Y are distinct, and the points Y and Z are
% 58.69/58.71 % equal, then X and Z are distinct, and the line connecting X
% 58.69/58.71 % and Y is equivalent to the line connecting X and Z.
% 58.69/58.71
% 58.69/58.71 % Refs : [vPl95] von Plato (1995), The Axioms of Constructive Geometry
% 58.69/58.71 % : [ROK06] Raths et al. (2006), The ILTP Problem Library for Intu
% 58.69/58.71 % : [Rat07] Raths (2007), Email to Geoff Sutcliffe
% 58.69/58.71 % Source : [Rat07]
% 58.69/58.71 % Names : Theorem 5.5 [vPl95]
% 58.69/58.71
% 58.69/58.71 % Status : Theorem
% 58.69/58.71 % Rating : 0.00 v6.1.0, 0.08 v6.0.0, 0.25 v5.5.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.29 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.16 v4.0.0
% 58.69/58.71 % Syntax : Number of formulae : 36 ( 7 unt; 0 def)
% 58.69/58.71 % Number of atoms : 97 ( 0 equ)
% 58.69/58.71 % Maximal formula atoms : 6 ( 2 avg)
% 58.69/58.71 % Number of connectives : 89 ( 28 ~; 19 |; 15 &)
% 58.69/58.71 % ( 5 <=>; 22 =>; 0 <=; 0 <~>)
% 58.69/58.71 % Maximal formula depth : 9 ( 5 avg)
% 58.69/58.71 % Maximal term depth : 2 ( 1 avg)
% 58.69/58.71 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 58.69/58.71 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty)
% 58.69/58.71 % Number of variables : 84 ( 84 !; 0 ?)
% 58.69/58.71 % SPC : FOF_THM_RFO_NEQ
% 58.69/58.71
% 58.69/58.71 % Comments :
% 58.69/58.71 %------------------------------------------------------------------------------
% 58.69/58.71 include('Axioms/GEO006+0.ax').
% 58.69/58.71 include('Axioms/GEO006+1.ax').
% 58.69/58.72 include('Axioms/GEO006+2.ax').
% 58.69/58.72 include('Axioms/GEO006+3.ax').
% 58.69/58.72 include('Axioms/GEO006+4.ax').
% 58.69/58.72 include('Axioms/GEO006+5.ax').
% 58.69/58.72 include('Axioms/GEO006+6.ax').
% 58.69/58.72 %------------------------------------------------------------------------------
% 58.69/58.72 fof(con,conjecture,
% 58.69/58.72 ! [X,Y,Z] :
% 58.69/58.72 ( ( distinct_points(X,Y)
% 58.69/58.72 & equal_points(Y,Z) )
% 58.69/58.72 => ( distinct_points(X,Z)
% 58.69/58.72 & equal_lines(line_connecting(X,Y),line_connecting(X,Z)) ) ) ).
% 58.69/58.72
% 58.69/58.72 %------------------------------------------------------------------------------
% 58.69/58.72 %-------------------------------------------
% 58.69/58.72 % Proof found
% 58.69/58.72 % SZS status Theorem for theBenchmark
% 58.69/58.72 % SZS output start Proof
% 58.69/58.73 %ClaNum:49(EqnAxiom:0)
% 58.69/58.73 %VarNum:218(SingletonVarNum:98)
% 58.69/58.73 %MaxLitNum:6
% 58.69/58.73 %MaxfuncDepth:1
% 58.69/58.73 %SharedTerms:9
% 58.69/58.73 %goalClause: 1 2 48
% 58.69/58.73 %singleGoalClaCount:2
% 58.69/58.73 [1]P1(a1,a2)
% 58.69/58.73 [2]P5(a2,a3)
% 58.69/58.73 [3]~P1(x31,x31)
% 58.69/58.73 [4]~P2(x41,x41)
% 58.69/58.73 [5]~P3(x51,x51)
% 58.69/58.73 [6]~P4(x61,f4(x62,x61))
% 58.69/58.73 [7]~P4(x71,f5(x72,x71))
% 58.69/58.73 [8]~P3(f4(x81,x82),x81)
% 58.69/58.73 [9]~P7(f5(x91,x92),x91)
% 58.69/58.73 [48]~P1(a1,a3)+~P6(f7(a1,a2),f7(a1,a3))
% 58.69/58.73 [10]P5(x101,x102)+P1(x101,x102)
% 58.69/58.73 [11]P6(x111,x112)+P2(x111,x112)
% 58.69/58.73 [13]P7(x131,x132)+P3(x131,x132)
% 58.69/58.73 [14]P8(x141,x142)+P3(x141,x142)
% 58.69/58.73 [15]P9(x151,x152)+P4(x151,x152)
% 58.69/58.73 [16]P10(x161,x162)+P7(x161,x162)
% 58.69/58.73 [17]~P2(x171,x172)+P3(x171,x172)
% 58.69/58.73 [20]~P5(x201,x202)+~P1(x201,x202)
% 58.69/58.73 [21]~P6(x211,x212)+~P2(x211,x212)
% 58.69/58.73 [22]~P8(x221,x222)+~P3(x221,x222)
% 58.69/58.73 [23]~P9(x231,x232)+~P4(x231,x232)
% 58.69/58.73 [24]~P10(x241,x242)+~P7(x241,x242)
% 58.69/58.73 [44]~P1(x441,x442)+~P4(x442,f7(x441,x442))
% 58.69/58.73 [45]~P1(x451,x452)+~P4(x451,f7(x451,x452))
% 58.69/58.73 [46]~P3(x461,x462)+~P4(f6(x461,x462),x462)
% 58.69/58.73 [47]~P3(x471,x472)+~P4(f6(x471,x472),x471)
% 58.69/58.73 [18]~P12(x182)+~P11(x181)+P11(f4(x181,x182))
% 58.69/58.73 [19]~P12(x192)+~P11(x191)+P11(f5(x191,x192))
% 58.69/58.73 [25]~P1(x253,x251)+P1(x251,x252)+P1(x253,x252)
% 58.69/58.73 [26]~P4(x261,x263)+P1(x261,x262)+P4(x262,x263)
% 58.69/58.73 [27]~P2(x273,x271)+P2(x271,x272)+P2(x273,x272)
% 58.69/58.73 [28]~P3(x283,x281)+P2(x281,x282)+P3(x283,x282)
% 58.69/58.73 [29]~P4(x293,x291)+P2(x291,x292)+P4(x293,x292)
% 58.69/58.73 [30]~P3(x303,x301)+P3(x301,x302)+P3(x303,x302)
% 58.69/58.73 [31]~P3(x313,x312)+P7(x311,x312)+P7(x311,x313)
% 58.69/58.73 [33]~P11(x332)+~P11(x331)+~P3(x331,x332)+P12(f6(x331,x332))
% 58.69/58.73 [34]~P12(x342)+~P12(x341)+~P1(x341,x342)+P11(f7(x341,x342))
% 58.69/58.73 [36]~P3(x361,x363)+~P7(x361,x363)+P3(x361,x362)+P7(x363,x362)
% 58.69/58.73 [37]~P3(x372,x373)+~P7(x372,x373)+P3(x371,x372)+P3(x371,x373)
% 58.69/58.73 [38]~P3(x382,x383)+~P7(x382,x383)+P3(x381,x382)+P7(x381,x383)
% 58.69/58.73 [39]~P3(x393,x391)+~P7(x393,x391)+P3(x391,x392)+P7(x393,x392)
% 58.69/58.73 [40]~P3(x403,x402)+~P7(x403,x402)+P3(x401,x402)+P7(x401,x403)
% 58.69/58.73 [41]~P3(x411,x413)+~P7(x411,x413)+P7(x411,x412)+P7(x413,x412)
% 58.69/58.73 [43]P7(x433,x434)+~P2(x433,x432)+P4(x431,x432)+P4(x431,x433)+P7(x432,x434)
% 58.69/58.73 [49]P4(x494,x493)+~P1(x494,x491)+~P2(x493,x492)+P4(x491,x492)+P4(x491,x493)+P4(x494,x492)
% 58.69/58.73 %EqnAxiom
% 58.69/58.73
% 58.69/58.73 %-------------------------------------------
% 58.69/58.75 cnf(58,plain,
% 58.69/58.75 (~P2(f4(x581,x582),x581)),
% 58.69/58.75 inference(scs_inference,[],[1,3,4,6,8,20,10,11,15,17])).
% 58.69/58.75 cnf(66,plain,
% 58.69/58.75 (P1(a2,a1)),
% 58.69/58.75 inference(scs_inference,[],[1,3,4,6,9,5,8,20,10,11,15,17,13,14,16,25])).
% 58.69/58.75 cnf(87,plain,
% 58.69/58.75 (~P3(x871,f4(x871,x872))),
% 58.69/58.75 inference(scs_inference,[],[66,7,58,8,5,14,13,15,11,20,30])).
% 58.69/58.75 cnf(92,plain,
% 58.69/58.75 (~P2(x921,f4(x921,x922))),
% 58.69/58.75 inference(scs_inference,[],[66,7,58,8,5,14,13,15,11,20,30,24,17])).
% 58.69/58.75 cnf(7589,plain,
% 58.69/58.75 (~P4(x75891,x75892)),
% 58.69/58.75 inference(scs_inference,[],[92,6,29])).
% 58.69/58.75 cnf(10157,plain,
% 58.69/58.75 (~P8(f5(x101571,x101572),x101571)),
% 58.69/58.75 inference(scs_inference,[],[9,13,22])).
% 58.69/58.75 cnf(10203,plain,
% 58.69/58.75 (P2(x102031,f4(f5(x102031,x102032),x102033))),
% 58.69/58.75 inference(scs_inference,[],[9,87,13,28])).
% 58.69/58.75 cnf(10206,plain,
% 58.69/58.75 (P2(f4(f5(x102061,x102062),x102063),x102061)),
% 58.69/58.75 inference(scs_inference,[],[4,10203,21,27])).
% 58.69/58.75 cnf(10215,plain,
% 58.69/58.75 (P2(x102151,f5(x102151,x102152))),
% 58.69/58.75 inference(scs_inference,[],[58,10206,21,27])).
% 58.69/58.75 cnf(10224,plain,
% 58.69/58.75 (P2(f5(x102241,x102242),x102241)),
% 58.69/58.75 inference(scs_inference,[],[4,10215,21,27])).
% 58.69/58.75 cnf(10241,plain,
% 58.69/58.75 (P2(f5(x102411,x102412),f4(x102411,x102413))),
% 58.69/58.75 inference(scs_inference,[],[92,10215,10224,21,27])).
% 58.69/58.75 cnf(10934,plain,
% 58.69/58.75 (P7(f5(f5(x109341,x109342),x109343),x109341)),
% 58.69/58.75 inference(scs_inference,[],[10157,9,14,31])).
% 58.69/58.75 cnf(10974,plain,
% 58.69/58.75 (P2(f4(x109741,x109742),f5(x109741,x109743))),
% 58.69/58.75 inference(scs_inference,[],[10241,4,27])).
% 58.69/58.75 cnf(11640,plain,
% 58.69/58.75 (P3(f4(x116401,x116402),f5(x116401,x116403))),
% 58.69/58.75 inference(scs_inference,[],[10974,17])).
% 58.69/58.75 cnf(11646,plain,
% 58.69/58.75 (P3(f5(x116461,x116462),f4(x116461,x116463))),
% 58.69/58.75 inference(scs_inference,[],[10241,17])).
% 58.69/58.75 cnf(11652,plain,
% 58.69/58.75 (P3(x116521,f5(x116521,x116522))),
% 58.69/58.75 inference(scs_inference,[],[10215,17])).
% 58.69/58.75 cnf(11749,plain,
% 58.69/58.75 (P7(f5(f5(x117491,x117492),x117493),f4(x117491,x117494))),
% 58.69/58.75 inference(scs_inference,[],[9,11646,31])).
% 58.69/58.75 cnf(11759,plain,
% 58.69/58.75 (~P7(f5(x117591,x117592),x117591)),
% 58.69/58.75 inference(rename_variables,[],[9])).
% 58.69/58.75 cnf(11761,plain,
% 58.69/58.75 (P7(f4(x117611,x117612),f5(x117611,x117613))+~P3(f5(f5(x117611,x117613),x117614),f4(x117611,x117612))),
% 58.69/58.75 inference(scs_inference,[],[9,11759,11640,11749,24,31,41])).
% 58.69/58.75 cnf(12546,plain,
% 58.69/58.75 (~P3(f5(f5(x125461,x125462),x125463),f4(x125461,x125464))),
% 58.69/58.75 inference(scs_inference,[],[9,11640,8,11761,36])).
% 58.69/58.75 cnf(14721,plain,
% 58.69/58.75 (~P7(f4(x147211,x147212),f5(x147211,x147213))),
% 58.69/58.75 inference(scs_inference,[],[10974,9,12546,17,38])).
% 58.69/58.75 cnf(15332,plain,
% 58.69/58.75 (P1(a1,a3)),
% 58.69/58.75 inference(scs_inference,[],[2,66,20,25])).
% 58.69/58.75 cnf(15500,plain,
% 58.69/58.75 (P7(x155001,f5(x155001,x155002))+~P3(f5(f5(x155001,x155002),x155003),x155001)),
% 58.69/58.75 inference(scs_inference,[],[9,10934,41])).
% 58.69/58.75 cnf(15543,plain,
% 58.69/58.75 (~P3(f5(f5(x155431,x155432),x155433),x155431)),
% 58.69/58.75 inference(scs_inference,[],[9,11652,5,15500,40])).
% 58.69/58.75 cnf(15663,plain,
% 58.69/58.75 (~P7(x156631,f5(x156631,x156632))),
% 58.69/58.75 inference(scs_inference,[],[11652,9,15543,38])).
% 58.69/58.75 cnf(15868,plain,
% 58.69/58.75 (P4(a3,f5(x158681,x158682))+P4(a3,x158681)+P4(a1,x158681)),
% 58.69/58.75 inference(scs_inference,[],[15332,10215,14721,7589,16,49])).
% 58.69/58.75 cnf(15871,plain,
% 58.69/58.75 (P4(a3,x158711)+P4(a3,f5(x158711,x158712))),
% 58.69/58.75 inference(scs_inference,[],[15663,7589,16,15868])).
% 58.69/58.75 cnf(15874,plain,
% 58.69/58.75 (P4(a3,f5(x158741,x158742))),
% 58.69/58.75 inference(scs_inference,[],[7589,15871])).
% 58.69/58.75 cnf(15877,plain,
% 58.69/58.75 ($false),
% 58.69/58.75 inference(scs_inference,[],[15874,7589]),
% 58.69/58.75 ['proof']).
% 58.69/58.76 % SZS output end Proof
% 58.69/58.76 % Total time :58.050000s
%------------------------------------------------------------------------------