%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO058-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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:34 EDT 2024
% Result : Unsatisfiable 0.58s 0.70s
% Output : CNFRefutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO058-3 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n020.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 21 07:36:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 0.58/0.69 %-------------------------------------------
% 0.58/0.69 % File :CSE---1.7
% 0.58/0.69 % Problem :theBenchmark
% 0.58/0.69 % Transform :cnf
% 0.58/0.69 % Format :tptp:raw
% 0.58/0.69 % Command :java -jar mcs_scs.jar %d %s
% 0.58/0.69
% 0.58/0.69 % Result :Theorem 0.040000s
% 0.58/0.69 % Output :CNFRefutation 0.040000s
% 0.58/0.69 %-------------------------------------------
% 0.58/0.70 %--------------------------------------------------------------------------
% 0.58/0.70 % File : GEO058-3 : TPTP v8.2.0. Released v1.0.0.
% 0.58/0.70 % Domain : Geometry
% 0.58/0.70 % Problem : U is the only fixed point of reflection(U,V)
% 0.58/0.70 % Version : [Qua89] axioms : Augmented.
% 0.58/0.70 % English :
% 0.58/0.70
% 0.58/0.70 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 0.58/0.70 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 0.58/0.70 % Source : [Qua89]
% 0.58/0.70 % Names : R4 [Qua89]
% 0.58/0.70
% 0.58/0.70 % Status : Unsatisfiable
% 0.58/0.70 % Rating : 0.05 v8.1.0, 0.00 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.10 v5.5.0, 0.20 v5.4.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.00 v4.0.1, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.22 v2.2.1, 0.00 v2.1.0, 0.00 v2.0.0
% 0.58/0.70 % Syntax : Number of clauses : 36 ( 14 unt; 5 nHn; 27 RR)
% 0.58/0.70 % Number of literals : 85 ( 15 equ; 46 neg)
% 0.58/0.70 % Maximal clause size : 8 ( 2 avg)
% 0.58/0.70 % Maximal term depth : 2 ( 1 avg)
% 0.58/0.70 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 0.58/0.70 % Number of functors : 11 ( 11 usr; 5 con; 0-6 aty)
% 0.58/0.70 % Number of variables : 124 ( 6 sgn)
% 0.58/0.70 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.58/0.70
% 0.58/0.70 % Comments :
% 0.58/0.70 %--------------------------------------------------------------------------
% 0.58/0.70 %----Include Tarski geometry axioms
% 0.58/0.70 include('Axioms/GEO002-0.ax').
% 0.58/0.70 %----Include definition of reflection
% 0.58/0.70 include('Axioms/GEO002-2.ax').
% 0.58/0.70 %--------------------------------------------------------------------------
% 0.58/0.70 cnf(d1,axiom,
% 0.58/0.70 equidistant(U,V,U,V) ).
% 0.58/0.70
% 0.58/0.70 cnf(d2,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(W,X,U,V) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d3,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(V,U,W,X) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d4_1,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(U,V,X,W) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d4_2,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(V,U,X,W) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d4_3,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(W,X,V,U) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d4_4,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(X,W,U,V) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d4_5,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | equidistant(X,W,V,U) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(d5,axiom,
% 0.58/0.70 ( ~ equidistant(U,V,W,X)
% 0.58/0.70 | ~ equidistant(W,X,Y,Z)
% 0.58/0.70 | equidistant(U,V,Y,Z) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(e1,axiom,
% 0.58/0.70 V = extension(U,V,W,W) ).
% 0.58/0.70
% 0.58/0.70 cnf(b0,axiom,
% 0.58/0.70 ( Y != extension(U,V,W,X)
% 0.58/0.70 | between(U,V,Y) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(r2_1,axiom,
% 0.58/0.70 between(U,V,reflection(U,V)) ).
% 0.58/0.70
% 0.58/0.70 cnf(r2_2,axiom,
% 0.58/0.70 equidistant(V,reflection(U,V),U,V) ).
% 0.58/0.70
% 0.58/0.70 cnf(r3_1,axiom,
% 0.58/0.70 ( U != V
% 0.58/0.70 | V = reflection(U,V) ) ).
% 0.58/0.70
% 0.58/0.70 cnf(r3_2,axiom,
% 0.58/0.70 U = reflection(U,U) ).
% 0.58/0.70
% 0.58/0.70 cnf(v_equals_reflection,hypothesis,
% 0.58/0.70 v = reflection(u,v) ).
% 0.58/0.70
% 0.58/0.70 cnf(prove_u_equals_v,negated_conjecture,
% 0.58/0.70 u != v ).
% 0.58/0.70
% 0.58/0.70 %--------------------------------------------------------------------------
% 0.58/0.70 %-------------------------------------------
% 0.58/0.70 % Proof found
% 0.58/0.70 % SZS status Theorem for theBenchmark
% 0.58/0.70 % SZS output start Proof
% 0.58/0.70 %ClaNum:70(EqnAxiom:35)
% 0.58/0.70 %VarNum:303(SingletonVarNum:117)
% 0.58/0.70 %MaxLitNum:8
% 0.58/0.70 %MaxfuncDepth:1
% 0.58/0.70 %SharedTerms:11
% 0.58/0.70 %goalClause: 45
% 0.58/0.70 %singleGoalClaCount:1
% 0.58/0.70 [45]~E(a1,a10)
% 0.58/0.70 [46]~P2(a6,a8,a9)
% 0.58/0.70 [47]~P2(a8,a9,a6)
% 0.58/0.70 [48]~P2(a9,a6,a8)
% 0.58/0.70 [36]E(f2(a1,a10,a1,a10),a10)
% 0.58/0.70 [37]P1(x371,x372,x372,x371)
% 0.58/0.70 [38]P1(x381,x382,x381,x382)
% 0.58/0.70 [39]E(f2(x391,x392,x393,x393),x392)
% 0.58/0.70 [41]P2(x411,x412,f2(x411,x412,x413,x414))
% 0.58/0.70 [43]P1(x431,f2(x432,x431,x433,x434),x433,x434)
% 0.58/0.70 [49]~P2(x491,x492,x491)+E(x491,x492)
% 0.58/0.70 [50]~E(x501,x502)+E(f2(x501,x502,x501,x502),x502)
% 0.58/0.70 [51]~P1(x511,x512,x513,x513)+E(x511,x512)
% 0.58/0.70 [53]~P1(x534,x533,x532,x531)+P1(x531,x532,x533,x534)
% 0.58/0.70 [54]~P1(x543,x544,x542,x541)+P1(x541,x542,x543,x544)
% 0.58/0.70 [55]~P1(x554,x553,x551,x552)+P1(x551,x552,x553,x554)
% 0.58/0.70 [56]~P1(x563,x564,x561,x562)+P1(x561,x562,x563,x564)
% 0.58/0.70 [57]~P1(x572,x571,x574,x573)+P1(x571,x572,x573,x574)
% 0.58/0.70 [58]~P1(x582,x581,x583,x584)+P1(x581,x582,x583,x584)
% 0.58/0.70 [59]~P1(x591,x592,x594,x593)+P1(x591,x592,x593,x594)
% 0.58/0.70 [52]P2(x521,x522,x523)+~E(x523,f2(x521,x522,x524,x525))
% 0.58/0.70 [64]~P2(x645,x641,x644)+~P2(x642,x643,x644)+P2(x641,f7(x642,x643,x644,x641,x645),x642)
% 0.58/0.70 [65]~P2(x655,x654,x653)+~P2(x652,x651,x653)+P2(x651,f7(x652,x651,x653,x654,x655),x655)
% 0.58/0.70 [60]~P1(x605,x606,x601,x602)+P1(x601,x602,x603,x604)+~P1(x605,x606,x603,x604)
% 0.58/0.70 [61]~P1(x611,x612,x615,x616)+P1(x611,x612,x613,x614)+~P1(x615,x616,x613,x614)
% 0.58/0.70 [66]~P2(x664,x662,x663)+~P2(x661,x662,x665)+E(x661,x662)+P2(x661,x663,f3(x661,x664,x662,x663,x665))
% 0.58/0.70 [67]~P2(x673,x672,x674)+~P2(x671,x672,x675)+E(x671,x672)+P2(x671,x673,f4(x671,x673,x672,x674,x675))
% 0.58/0.70 [68]~P2(x683,x682,x684)+~P2(x681,x682,x685)+E(x681,x682)+P2(f4(x681,x683,x682,x684,x685),x685,f3(x681,x683,x682,x684,x685))
% 0.58/0.70 [69]~P2(x693,x694,x695)+~P2(x692,x693,x695)+~P1(x692,x695,x692,x696)+~P1(x692,x693,x692,x691)+P2(x691,f5(x692,x693,x691,x694,x695,x696),x696)
% 0.58/0.70 [70]~P2(x703,x702,x705)+~P2(x701,x703,x705)+~P1(x701,x705,x701,x706)+~P1(x701,x703,x701,x704)+P1(x701,x702,x701,f5(x701,x703,x704,x702,x705,x706))
% 0.58/0.70 [62]P2(x625,x623,x624)+P2(x624,x625,x623)+~P1(x623,x621,x623,x622)+~P1(x625,x621,x625,x622)+~P1(x624,x621,x624,x622)+E(x621,x622)+P2(x623,x624,x625)
% 0.58/0.70 [63]~P2(x631,x632,x633)+~P1(x632,x634,x638,x636)+~P1(x632,x633,x638,x635)+~P1(x631,x634,x637,x636)+~P1(x631,x632,x637,x638)+E(x631,x632)+P1(x633,x634,x635,x636)+~P2(x637,x638,x635)
% 0.58/0.70 %EqnAxiom
% 0.58/0.70 [1]E(x11,x11)
% 0.58/0.70 [2]E(x22,x21)+~E(x21,x22)
% 0.58/0.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.58/0.70 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45))
% 0.58/0.70 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55))
% 0.58/0.70 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65))
% 0.58/0.70 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72))
% 0.58/0.70 [8]~E(x81,x82)+E(f5(x81,x83,x84,x85,x86,x87),f5(x82,x83,x84,x85,x86,x87))
% 0.58/0.70 [9]~E(x91,x92)+E(f5(x93,x91,x94,x95,x96,x97),f5(x93,x92,x94,x95,x96,x97))
% 0.58/0.70 [10]~E(x101,x102)+E(f5(x103,x104,x101,x105,x106,x107),f5(x103,x104,x102,x105,x106,x107))
% 0.58/0.70 [11]~E(x111,x112)+E(f5(x113,x114,x115,x111,x116,x117),f5(x113,x114,x115,x112,x116,x117))
% 0.58/0.70 [12]~E(x121,x122)+E(f5(x123,x124,x125,x126,x121,x127),f5(x123,x124,x125,x126,x122,x127))
% 0.58/0.70 [13]~E(x131,x132)+E(f5(x133,x134,x135,x136,x137,x131),f5(x133,x134,x135,x136,x137,x132))
% 0.58/0.70 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145,x146),f7(x142,x143,x144,x145,x146))
% 0.58/0.70 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155,x156),f7(x153,x152,x154,x155,x156))
% 0.58/0.70 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165,x166),f7(x163,x164,x162,x165,x166))
% 0.58/0.70 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171,x176),f7(x173,x174,x175,x172,x176))
% 0.58/0.70 [18]~E(x181,x182)+E(f7(x183,x184,x185,x186,x181),f7(x183,x184,x185,x186,x182))
% 0.58/0.70 [19]~E(x191,x192)+E(f3(x191,x193,x194,x195,x196),f3(x192,x193,x194,x195,x196))
% 0.58/0.70 [20]~E(x201,x202)+E(f3(x203,x201,x204,x205,x206),f3(x203,x202,x204,x205,x206))
% 0.58/0.70 [21]~E(x211,x212)+E(f3(x213,x214,x211,x215,x216),f3(x213,x214,x212,x215,x216))
% 0.58/0.70 [22]~E(x221,x222)+E(f3(x223,x224,x225,x221,x226),f3(x223,x224,x225,x222,x226))
% 0.58/0.70 [23]~E(x231,x232)+E(f3(x233,x234,x235,x236,x231),f3(x233,x234,x235,x236,x232))
% 0.58/0.70 [24]~E(x241,x242)+E(f4(x241,x243,x244,x245,x246),f4(x242,x243,x244,x245,x246))
% 0.58/0.70 [25]~E(x251,x252)+E(f4(x253,x251,x254,x255,x256),f4(x253,x252,x254,x255,x256))
% 0.58/0.70 [26]~E(x261,x262)+E(f4(x263,x264,x261,x265,x266),f4(x263,x264,x262,x265,x266))
% 0.58/0.70 [27]~E(x271,x272)+E(f4(x273,x274,x275,x271,x276),f4(x273,x274,x275,x272,x276))
% 0.58/0.70 [28]~E(x281,x282)+E(f4(x283,x284,x285,x286,x281),f4(x283,x284,x285,x286,x282))
% 0.58/0.70 [29]P1(x292,x293,x294,x295)+~E(x291,x292)+~P1(x291,x293,x294,x295)
% 0.58/0.70 [30]P1(x303,x302,x304,x305)+~E(x301,x302)+~P1(x303,x301,x304,x305)
% 0.58/0.70 [31]P1(x313,x314,x312,x315)+~E(x311,x312)+~P1(x313,x314,x311,x315)
% 0.58/0.70 [32]P1(x323,x324,x325,x322)+~E(x321,x322)+~P1(x323,x324,x325,x321)
% 0.58/0.70 [33]P2(x332,x333,x334)+~E(x331,x332)+~P2(x331,x333,x334)
% 0.58/0.70 [34]P2(x343,x342,x344)+~E(x341,x342)+~P2(x343,x341,x344)
% 0.58/0.70 [35]P2(x353,x354,x352)+~E(x351,x352)+~P2(x353,x354,x351)
% 0.58/0.70
% 0.58/0.70 %-------------------------------------------
% 0.58/0.71 cnf(73,plain,
% 0.58/0.71 (~P2(a1,a10,a1)),
% 0.58/0.71 inference(scs_inference,[],[45,49])).
% 0.58/0.71 cnf(75,plain,
% 0.58/0.71 (~P1(a1,a10,x751,x751)),
% 0.58/0.71 inference(scs_inference,[],[45,49,51])).
% 0.58/0.71 cnf(77,plain,
% 0.58/0.71 (E(x771,f2(x772,x771,x773,x773))),
% 0.58/0.71 inference(scs_inference,[],[45,39,49,51,2])).
% 0.58/0.71 cnf(78,plain,
% 0.58/0.71 (P2(x781,x782,f2(x783,f2(x781,x782,x784,x785),x786,x786))),
% 0.58/0.71 inference(scs_inference,[],[45,39,49,51,2,52])).
% 0.58/0.71 cnf(79,plain,
% 0.58/0.71 (E(f2(x791,x792,x793,x793),x792)),
% 0.58/0.71 inference(rename_variables,[],[39])).
% 0.58/0.71 cnf(81,plain,
% 0.58/0.71 (~P1(x811,x811,a10,a1)),
% 0.58/0.71 inference(scs_inference,[],[45,39,49,51,2,52,53])).
% 0.58/0.71 cnf(87,plain,
% 0.58/0.71 (~E(a1,f2(x871,a10,x872,x872))),
% 0.58/0.71 inference(scs_inference,[],[45,39,79,49,51,2,52,53,54,55,3])).
% 0.58/0.71 cnf(89,plain,
% 0.58/0.71 (P1(f2(x891,x892,x893,x894),x892,x893,x894)),
% 0.58/0.71 inference(scs_inference,[],[45,37,43,39,79,49,51,2,52,53,54,55,3,60])).
% 0.58/0.71 cnf(91,plain,
% 0.58/0.71 (P1(x911,x912,x912,x911)),
% 0.58/0.71 inference(rename_variables,[],[37])).
% 0.58/0.71 cnf(93,plain,
% 0.58/0.71 (~E(a10,a1)),
% 0.58/0.71 inference(scs_inference,[],[45,37,91,43,39,79,49,51,2,52,53,54,55,3,60,29])).
% 0.58/0.71 cnf(115,plain,
% 0.58/0.71 (E(a10,f2(a1,a10,a1,a10))),
% 0.58/0.71 inference(scs_inference,[],[77,36,52,2])).
% 0.58/0.71 cnf(122,plain,
% 0.58/0.71 (P1(f2(x1221,x1222,x1223,x1224),x1222,f2(x1225,x1223,x1226,x1226),x1224)),
% 0.58/0.71 inference(scs_inference,[],[77,89,93,87,36,52,2,51,54,49,31])).
% 0.58/0.71 cnf(123,plain,
% 0.58/0.71 (P1(f2(x1231,x1232,x1233,x1234),x1232,x1233,x1234)),
% 0.58/0.71 inference(rename_variables,[],[89])).
% 0.58/0.71 cnf(124,plain,
% 0.58/0.71 (~E(x1241,f2(x1242,x1241,a10,a1))),
% 0.58/0.71 inference(scs_inference,[],[77,89,123,93,81,87,36,52,2,51,54,49,31,30])).
% 0.58/0.71 cnf(125,plain,
% 0.58/0.71 (P1(f2(x1251,x1252,x1253,x1254),x1252,x1253,x1254)),
% 0.58/0.71 inference(rename_variables,[],[89])).
% 0.58/0.71 cnf(128,plain,
% 0.58/0.71 (P2(x1281,x1282,f2(x1283,f2(x1281,x1282,x1284,x1285),x1286,x1286))),
% 0.58/0.71 inference(rename_variables,[],[78])).
% 0.58/0.71 cnf(130,plain,
% 0.58/0.71 (P2(x1301,x1302,f2(x1303,f2(x1301,x1302,x1304,x1305),x1306,x1306))),
% 0.58/0.71 inference(rename_variables,[],[78])).
% 0.58/0.71 cnf(131,plain,
% 0.58/0.71 (P1(f2(x1311,x1312,x1313,x1314),x1312,x1313,f2(x1315,x1314,x1316,x1316))),
% 0.58/0.71 inference(scs_inference,[],[73,77,89,123,125,78,128,93,81,87,36,52,2,51,54,49,31,30,35,34,32])).
% 0.58/0.71 cnf(132,plain,
% 0.58/0.71 (P1(f2(x1321,x1322,x1323,x1324),x1322,x1323,x1324)),
% 0.58/0.71 inference(rename_variables,[],[89])).
% 0.58/0.71 cnf(140,plain,
% 0.58/0.71 (~P1(x1401,x1401,a1,f2(x1402,a10,x1403,x1403))),
% 0.58/0.71 inference(scs_inference,[],[45,73,77,75,89,123,125,132,78,128,130,93,81,87,36,52,2,51,54,49,31,30,35,34,32,33,29,3,58,59])).
% 0.58/0.71 cnf(153,plain,
% 0.58/0.71 (P1(f2(x1531,x1532,x1533,x1534),x1532,x1533,f2(x1535,x1534,x1536,x1536))),
% 0.58/0.71 inference(rename_variables,[],[131])).
% 0.58/0.71 cnf(156,plain,
% 0.58/0.71 (P1(f2(x1561,x1562,x1563,x1564),x1562,x1563,f2(x1565,x1564,x1566,x1566))),
% 0.58/0.71 inference(rename_variables,[],[131])).
% 0.58/0.71 cnf(159,plain,
% 0.58/0.71 ($false),
% 0.58/0.71 inference(scs_inference,[],[115,122,131,153,156,124,140,51,54,49,60,61,30]),
% 0.58/0.71 ['proof']).
% 0.58/0.71 % SZS output end Proof
% 0.58/0.71 % Total time :0.040000s
%------------------------------------------------------------------------------