%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO085+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n026.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:03:43 EDT 2024
% Result : Theorem 17.56s 17.65s
% Output : CNFRefutation 17.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO085+1 : TPTP v8.2.0. Released v2.4.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.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:13:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 17.56/17.64 %-------------------------------------------
% 17.56/17.64 % File :CSE---1.7
% 17.56/17.64 % Problem :theBenchmark
% 17.56/17.64 % Transform :cnf
% 17.56/17.64 % Format :tptp:raw
% 17.56/17.64 % Command :java -jar mcs_scs.jar %d %s
% 17.56/17.64
% 17.56/17.64 % Result :Theorem 17.010000s
% 17.56/17.64 % Output :CNFRefutation 17.010000s
% 17.56/17.64 %-------------------------------------------
% 17.56/17.65 %--------------------------------------------------------------------------
% 17.56/17.65 % File : GEO085+1 : TPTP v8.2.0. Released v2.4.0.
% 17.56/17.65 % Domain : Geometry (Oriented curves)
% 17.56/17.65 % Problem : Every open curve has at least two endpoints
% 17.56/17.65 % Version : [EHK99] axioms.
% 17.56/17.65 % English :
% 17.56/17.65
% 17.56/17.65 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 17.56/17.65 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 17.56/17.65 % Source : [KE99]
% 17.56/17.65 % Names : Theorem 2.7 (1) [KE99]
% 17.56/17.65
% 17.56/17.65 % Status : Theorem
% 17.56/17.65 % Rating : 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.3.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.16 v3.3.0, 0.21 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.5.0, 0.00 v2.4.0
% 17.56/17.65 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 17.56/17.65 % Number of atoms : 71 ( 11 equ)
% 17.56/17.65 % Maximal formula atoms : 12 ( 4 avg)
% 17.56/17.65 % Number of connectives : 59 ( 5 ~; 9 |; 23 &)
% 17.56/17.65 % ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% 17.56/17.65 % Maximal formula depth : 12 ( 7 avg)
% 17.56/17.65 % Maximal term depth : 2 ( 1 avg)
% 17.56/17.65 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 17.56/17.65 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 17.56/17.65 % Number of variables : 56 ( 45 !; 11 ?)
% 17.56/17.65 % SPC : FOF_THM_RFO_SEQ
% 17.56/17.65
% 17.56/17.65 % Comments :
% 17.56/17.65 %--------------------------------------------------------------------------
% 17.56/17.65 %----Include simple curve axioms
% 17.56/17.65 include('Axioms/GEO004+0.ax').
% 17.56/17.65 %--------------------------------------------------------------------------
% 17.56/17.65 fof(theorem_2_7_1,conjecture,
% 17.56/17.65 ! [C] :
% 17.56/17.65 ( open(C)
% 17.56/17.65 => ? [P,Q] :
% 17.56/17.65 ( P != Q
% 17.56/17.65 & end_point(P,C)
% 17.56/17.65 & end_point(Q,C) ) ) ).
% 17.56/17.65
% 17.56/17.65 %--------------------------------------------------------------------------
% 17.56/17.65 %-------------------------------------------
% 17.56/17.65 % Proof found
% 17.56/17.65 % SZS status Theorem for theBenchmark
% 17.56/17.65 % SZS output start Proof
% 17.56/17.65 %ClaNum:88(EqnAxiom:43)
% 17.56/17.65 %VarNum:335(SingletonVarNum:115)
% 17.56/17.65 %MaxLitNum:12
% 17.56/17.65 %MaxfuncDepth:2
% 17.56/17.65 %SharedTerms:2
% 17.56/17.65 %goalClause: 44 53
% 17.56/17.65 %singleGoalClaCount:1
% 17.56/17.65 [44]P1(a1)
% 17.56/17.65 [45]P2(f6(x451),x451)
% 17.56/17.65 [46]P3(x461)+P4(f7(x461),x461)
% 17.56/17.65 [48]~P1(x481)+P4(f13(x481),x481)
% 17.56/17.65 [47]P1(x471)+~P4(x472,x471)
% 17.56/17.65 [50]~P3(x501)+~P4(x502,x501)
% 17.56/17.65 [51]~P4(x511,x512)+P5(x511,x512)
% 17.56/17.65 [52]~P2(x521,x522)+P5(x521,x522)
% 17.56/17.65 [54]~P2(x541,x542)+~P4(x541,x542)
% 17.56/17.65 [55]~P4(x552,x551)+~E(f2(x551,x552),x552)
% 17.56/17.65 [57]P7(x571,x572)+P5(f8(x572,x571),x571)
% 17.56/17.65 [61]~P4(x612,x611)+P4(f2(x611,x612),x611)
% 17.56/17.65 [68]P7(x681,x682)+~P5(f8(x682,x681),x682)
% 17.56/17.65 [75]~P2(x751,x752)+P6(x751,f15(x752,x751),f3(x752,x751))
% 17.56/17.65 [70]~P2(x702,x701)+E(f14(f15(x701,x702),f3(x701,x702)),x701)
% 17.56/17.65 [71]P5(x711,x712)+~P6(x711,x713,x712)
% 17.56/17.65 [72]P5(x721,x722)+~P6(x721,x722,x723)
% 17.56/17.65 [73]~P6(x733,x731,x732)+E(f5(x731,x732),f14(x731,x732))
% 17.56/17.65 [49]P1(x491)+~P7(x491,x492)+E(x491,x492)
% 17.56/17.65 [53]E(x531,x532)+~P4(x532,a1)+~P4(x531,a1)
% 17.56/17.65 [56]P2(x561,x562)+~P5(x561,x562)+P4(x561,x562)
% 17.56/17.65 [64]~P5(x641,x642)+P4(x641,x642)+P5(x641,f9(x641,x642))
% 17.56/17.65 [65]~P5(x651,x652)+P4(x651,x652)+P5(x651,f11(x651,x652))
% 17.56/17.65 [66]~P5(x661,x662)+P4(x661,x662)+P7(f9(x661,x662),x662)
% 17.56/17.65 [67]~P5(x671,x672)+P4(x671,x672)+P7(f11(x671,x672),x672)
% 17.56/17.65 [69]E(x691,x692)+P5(f4(x691,x692),x692)+P5(f4(x691,x692),x691)
% 17.56/17.65 [74]E(x741,x742)+~P5(f4(x741,x742),x742)+~P5(f4(x741,x742),x741)
% 17.56/17.65 [76]~P5(x761,x762)+P4(x761,x762)+~P7(f9(x761,x762),f11(x761,x762))
% 17.56/17.65 [77]~P5(x771,x772)+P4(x771,x772)+~P7(f11(x771,x772),f9(x771,x772))
% 17.56/17.65 [58]~P5(x581,x583)+P5(x581,x582)+~P7(x583,x582)
% 17.56/17.65 [86]~P5(f10(x861,x862,x863),x863)+~P5(f10(x861,x862,x863),x861)+E(x861,f14(x862,x863))
% 17.56/17.65 [87]~P5(f10(x871,x872,x873),x872)+~P5(f10(x871,x872,x873),x871)+E(x871,f14(x872,x873))
% 17.56/17.65 [59]~P5(x591,x594)+P5(x591,x592)+~E(x592,f14(x593,x594))
% 17.56/17.65 [60]~P5(x601,x603)+P5(x601,x602)+~E(x602,f14(x603,x604))
% 17.56/17.65 [82]~P5(x821,x823)+~P5(x821,x822)+P6(x821,x822,x823)+P5(f12(x821,x822,x823),x823)
% 17.56/17.65 [83]~P5(x831,x833)+~P5(x831,x832)+P6(x831,x832,x833)+P5(f12(x831,x832,x833),x832)
% 17.56/17.65 [85]P5(f10(x851,x852,x853),x853)+P5(f10(x851,x852,x853),x852)+P5(f10(x851,x852,x853),x851)+E(x851,f14(x852,x853))
% 17.56/17.65 [79]~P5(x791,x792)+P4(x791,x792)+~P6(x794,x793,x792)+~P5(x791,x793)
% 17.56/17.65 [80]~P5(x801,x802)+P4(x801,x802)+~P6(x804,x802,x803)+~P5(x801,x803)
% 17.56/17.65 [63]~P5(x631,x634)+P5(x631,x632)+P5(x631,x633)+~E(x634,f14(x633,x632))
% 17.56/17.65 [88]~P5(x881,x883)+~P5(x881,x882)+P6(x881,x882,x883)+~P4(f12(x881,x882,x883),x883)+~P4(f12(x881,x882,x883),x882)
% 17.56/17.65 [81]~P3(x814)+~P4(x811,x812)+P6(x811,x812,x813)+~P6(x815,x812,x813)+~E(x814,f14(x812,x813))
% 17.56/17.65 [62]E(x623,x621)+~P4(x621,x624)+~P4(x623,x624)+E(x621,x622)+E(x623,x622)+~P4(x622,x624)
% 17.56/17.65 [78]P7(x782,x781)+~P7(x782,x783)+~P5(x784,x782)+~P4(x784,x783)+P7(x781,x782)+~P7(x781,x783)+~P5(x784,x781)
% 17.56/17.65 [84]P7(x842,x841)+P7(x842,x843)+P7(x843,x841)+P7(x843,x842)+~P7(x842,x844)+~P7(x843,x844)+~P4(x845,x842)+~P4(x845,x843)+P7(x841,x842)+P7(x841,x843)+~P7(x841,x844)+~P4(x845,x841)
% 17.56/17.65 %EqnAxiom
% 17.56/17.65 [1]E(x11,x11)
% 17.56/17.65 [2]E(x22,x21)+~E(x21,x22)
% 17.56/17.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 17.56/17.65 [4]~E(x41,x42)+E(f6(x41),f6(x42))
% 17.56/17.65 [5]~E(x51,x52)+E(f7(x51),f7(x52))
% 17.56/17.65 [6]~E(x61,x62)+E(f13(x61),f13(x62))
% 17.56/17.65 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73))
% 17.56/17.65 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82))
% 17.56/17.65 [9]~E(x91,x92)+E(f8(x91,x93),f8(x92,x93))
% 17.56/17.65 [10]~E(x101,x102)+E(f8(x103,x101),f8(x103,x102))
% 17.56/17.65 [11]~E(x111,x112)+E(f14(x111,x113),f14(x112,x113))
% 17.56/17.65 [12]~E(x121,x122)+E(f14(x123,x121),f14(x123,x122))
% 17.56/17.65 [13]~E(x131,x132)+E(f10(x131,x133,x134),f10(x132,x133,x134))
% 17.56/17.65 [14]~E(x141,x142)+E(f10(x143,x141,x144),f10(x143,x142,x144))
% 17.56/17.65 [15]~E(x151,x152)+E(f10(x153,x154,x151),f10(x153,x154,x152))
% 17.56/17.65 [16]~E(x161,x162)+E(f12(x161,x163,x164),f12(x162,x163,x164))
% 17.56/17.65 [17]~E(x171,x172)+E(f12(x173,x171,x174),f12(x173,x172,x174))
% 17.56/17.65 [18]~E(x181,x182)+E(f12(x183,x184,x181),f12(x183,x184,x182))
% 17.56/17.65 [19]~E(x191,x192)+E(f11(x191,x193),f11(x192,x193))
% 17.56/17.65 [20]~E(x201,x202)+E(f11(x203,x201),f11(x203,x202))
% 17.56/17.65 [21]~E(x211,x212)+E(f9(x211,x213),f9(x212,x213))
% 17.56/17.65 [22]~E(x221,x222)+E(f9(x223,x221),f9(x223,x222))
% 17.56/17.66 [23]~E(x231,x232)+E(f3(x231,x233),f3(x232,x233))
% 17.56/17.66 [24]~E(x241,x242)+E(f3(x243,x241),f3(x243,x242))
% 17.56/17.66 [25]~E(x251,x252)+E(f4(x251,x253),f4(x252,x253))
% 17.56/17.66 [26]~E(x261,x262)+E(f4(x263,x261),f4(x263,x262))
% 17.56/17.66 [27]~E(x271,x272)+E(f15(x271,x273),f15(x272,x273))
% 17.56/17.66 [28]~E(x281,x282)+E(f15(x283,x281),f15(x283,x282))
% 17.56/17.66 [29]~E(x291,x292)+E(f5(x291,x293),f5(x292,x293))
% 17.56/17.66 [30]~E(x301,x302)+E(f5(x303,x301),f5(x303,x302))
% 17.56/17.66 [31]~P1(x311)+P1(x312)+~E(x311,x312)
% 17.56/17.66 [32]P2(x322,x323)+~E(x321,x322)+~P2(x321,x323)
% 17.56/17.66 [33]P2(x333,x332)+~E(x331,x332)+~P2(x333,x331)
% 17.56/17.66 [34]~P3(x341)+P3(x342)+~E(x341,x342)
% 17.56/17.66 [35]P4(x352,x353)+~E(x351,x352)+~P4(x351,x353)
% 17.56/17.66 [36]P4(x363,x362)+~E(x361,x362)+~P4(x363,x361)
% 17.56/17.66 [37]P5(x372,x373)+~E(x371,x372)+~P5(x371,x373)
% 17.56/17.66 [38]P5(x383,x382)+~E(x381,x382)+~P5(x383,x381)
% 17.56/17.66 [39]P6(x392,x393,x394)+~E(x391,x392)+~P6(x391,x393,x394)
% 17.56/17.66 [40]P6(x403,x402,x404)+~E(x401,x402)+~P6(x403,x401,x404)
% 17.56/17.66 [41]P6(x413,x414,x412)+~E(x411,x412)+~P6(x413,x414,x411)
% 17.56/17.66 [42]P7(x422,x423)+~E(x421,x422)+~P7(x421,x423)
% 17.56/17.66 [43]P7(x433,x432)+~E(x431,x432)+~P7(x433,x431)
% 17.56/17.66
% 17.56/17.66 %-------------------------------------------
% 17.56/17.66 cnf(89,plain,
% 17.56/17.66 (~P5(x891,x892)+P5(x891,f14(x893,x892))),
% 17.56/17.66 inference(equality_inference,[],[59])).
% 17.56/17.66 cnf(90,plain,
% 17.56/17.66 (~P5(x901,x902)+P5(x901,f14(x902,x903))),
% 17.56/17.66 inference(equality_inference,[],[60])).
% 17.56/17.66 cnf(98,plain,
% 17.56/17.66 (~P4(x981,x982)+P4(f7(x982),x982)),
% 17.56/17.66 inference(scs_inference,[],[50,46])).
% 17.56/17.66 cnf(163,plain,
% 17.56/17.66 (~P4(x1631,x1632)+~E(f2(x1632,f7(x1632)),f7(x1632))),
% 17.56/17.66 inference(scs_inference,[],[98,55])).
% 17.56/17.66 cnf(169,plain,
% 17.56/17.66 (P4(f2(a1,f13(a1)),a1)),
% 17.56/17.66 inference(scs_inference,[],[44,61,48])).
% 17.56/17.66 cnf(528,plain,
% 17.56/17.66 (~E(f7(a1),f2(a1,f7(a1)))),
% 17.56/17.66 inference(scs_inference,[],[169,163,2])).
% 17.56/17.66 cnf(2095,plain,
% 17.56/17.66 (P4(f13(a1),a1)),
% 17.56/17.66 inference(scs_inference,[],[169,47,48])).
% 17.56/17.66 cnf(2867,plain,
% 17.56/17.66 (P4(f7(a1),a1)),
% 17.56/17.66 inference(scs_inference,[],[169,50,46])).
% 17.56/17.66 cnf(3735,plain,
% 17.56/17.66 (~E(f2(a1,f7(a1)),f7(a1))),
% 17.56/17.66 inference(scs_inference,[],[528,2])).
% 17.56/17.66 cnf(3736,plain,
% 17.56/17.66 (P5(f13(a1),a1)),
% 17.56/17.66 inference(scs_inference,[],[528,2095,2,51])).
% 17.56/17.66 cnf(3775,plain,
% 17.56/17.66 (P5(f13(a1),f14(x37751,a1))),
% 17.56/17.66 inference(scs_inference,[],[3736,89])).
% 17.56/17.66 cnf(3793,plain,
% 17.56/17.66 (~E(x37931,a1)+~E(f2(a1,f7(a1)),f7(x37931))),
% 17.56/17.66 inference(scs_inference,[],[3735,3775,89,90,3,5])).
% 17.56/17.66 cnf(5715,plain,
% 17.56/17.66 (~E(f7(x57151),f2(a1,f7(a1)))+~E(x57151,a1)),
% 17.56/17.66 inference(scs_inference,[],[3793,2])).
% 17.56/17.66 cnf(6711,plain,
% 17.56/17.66 (~P4(f2(a1,f7(a1)),a1)),
% 17.56/17.66 inference(scs_inference,[],[2867,5715,53])).
% 17.56/17.66 cnf(6712,plain,
% 17.56/17.66 ($false),
% 17.56/17.66 inference(scs_inference,[],[6711,2867,61]),
% 17.56/17.66 ['proof']).
% 17.56/17.66 % SZS output end Proof
% 17.56/17.66 % Total time :17.010000s
%------------------------------------------------------------------------------