%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO077-4 : 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 : n029.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:40 EDT 2024
% Result : Unsatisfiable 58.65s 58.67s
% Output : CNFRefutation 58.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO077-4 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n029.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:40:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 58.62/58.66 %-------------------------------------------
% 58.62/58.66 % File :CSE---1.7
% 58.62/58.66 % Problem :theBenchmark
% 58.62/58.66 % Transform :cnf
% 58.62/58.66 % Format :tptp:raw
% 58.62/58.66 % Command :java -jar mcs_scs.jar %d %s
% 58.62/58.66
% 58.62/58.66 % Result :Theorem 58.040000s
% 58.62/58.66 % Output :CNFRefutation 58.040000s
% 58.62/58.66 %-------------------------------------------
% 58.65/58.67 %--------------------------------------------------------------------------
% 58.65/58.67 % File : GEO077-4 : TPTP v8.2.0. Released v1.0.0.
% 58.65/58.67 % Domain : Geometry (Hilbert)
% 58.65/58.67 % Problem : Three points not collinear if not on line
% 58.65/58.67 % Version : [Ben92] axioms.
% 58.65/58.67 % English :
% 58.65/58.67
% 58.65/58.67 % Refs : [Ben92] Benanav (1992), Recognising Unnecessary Clauses in Res
% 58.65/58.67 % Source : [Ben92]
% 58.65/58.67 % Names : G11A [Ben92]
% 58.65/58.67
% 58.65/58.67 % Status : Unsatisfiable
% 58.65/58.67 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.09 v6.2.0, 0.00 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.30 v5.3.0, 0.22 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.17 v2.4.0, 0.11 v2.3.0, 0.00 v2.2.1, 0.33 v2.2.0, 0.22 v2.1.0, 0.67 v2.0.0
% 58.65/58.67 % Syntax : Number of clauses : 42 ( 12 unt; 18 nHn; 42 RR)
% 58.65/58.67 % Number of literals : 185 ( 46 equ; 107 neg)
% 58.65/58.67 % Maximal clause size : 16 ( 4 avg)
% 58.65/58.67 % Maximal term depth : 2 ( 1 avg)
% 58.65/58.67 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty)
% 58.65/58.67 % Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% 58.65/58.67 % Number of variables : 70 ( 0 sgn)
% 58.65/58.67 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.65/58.67
% 58.65/58.67 % Comments :
% 58.65/58.67 %--------------------------------------------------------------------------
% 58.65/58.67 %----Include axioms for Hilbert geometry
% 58.65/58.67 include('Axioms/GEO003-0.ax').
% 58.65/58.67 %--------------------------------------------------------------------------
% 58.65/58.67 cnf(point1,hypothesis,
% 58.65/58.67 point(point1) ).
% 58.65/58.67
% 58.65/58.67 cnf(point2,hypothesis,
% 58.65/58.67 point(point2) ).
% 58.65/58.67
% 58.65/58.67 cnf(point3,hypothesis,
% 58.65/58.67 point(point3) ).
% 58.65/58.67
% 58.65/58.67 cnf(line,hypothesis,
% 58.65/58.67 line(a_line) ).
% 58.65/58.67
% 58.65/58.67 cnf(point1_on_line,hypothesis,
% 58.65/58.67 on(point1,a_line) ).
% 58.65/58.67
% 58.65/58.67 cnf(point2_on_line,hypothesis,
% 58.65/58.67 on(point2,a_line) ).
% 58.65/58.67
% 58.65/58.67 cnf(point3_not_on_line,hypothesis,
% 58.65/58.67 ~ on(point3,a_line) ).
% 58.65/58.67
% 58.65/58.67 cnf(point1_not_point2,hypothesis,
% 58.65/58.67 point1 != point2 ).
% 58.65/58.67
% 58.65/58.67 cnf(point1_not_point3,hypothesis,
% 58.65/58.67 point1 != point3 ).
% 58.65/58.67
% 58.65/58.67 cnf(point2_not_point3,hypothesis,
% 58.65/58.67 point2 != point3 ).
% 58.65/58.67
% 58.65/58.67 cnf(prove_points_noncollinear,negated_conjecture,
% 58.65/58.67 collinear(point1,point2,point3) ).
% 58.65/58.67
% 58.65/58.67 %--------------------------------------------------------------------------
% 58.65/58.67 %-------------------------------------------
% 58.65/58.67 % Proof found
% 58.65/58.67 % SZS status Theorem for theBenchmark
% 58.65/58.67 % SZS output start Proof
% 58.65/58.67 %ClaNum:69(EqnAxiom:27)
% 58.65/58.67 %VarNum:304(SingletonVarNum:70)
% 58.65/58.67 %MaxLitNum:16
% 58.65/58.67 %MaxfuncDepth:1
% 58.65/58.67 %SharedTerms:17
% 58.65/58.67 %goalClause: 35
% 58.65/58.67 %singleGoalClaCount:1
% 58.65/58.67 [28]P1(a1)
% 58.65/58.67 [29]P1(a8)
% 58.65/58.67 [30]P1(a9)
% 58.65/58.67 [31]P2(a2)
% 58.65/58.67 [32]P2(a3)
% 58.65/58.67 [33]P4(a1,a3)
% 58.65/58.67 [34]P4(a8,a3)
% 58.65/58.67 [35]P3(a1,a8,a9)
% 58.65/58.67 [36]~E(a1,a8)
% 58.65/58.67 [37]~E(a1,a9)
% 58.65/58.67 [38]~E(a9,a8)
% 58.65/58.67 [39]~P4(a9,a3)
% 58.65/58.67 [40]~P2(x401)+P1(f10(x401))
% 58.65/58.67 [41]~P2(x411)+P1(f11(x411))
% 58.65/58.67 [42]~P2(x421)+P1(f12(x421))
% 58.65/58.67 [43]~P5(x431)+P1(f13(x431))
% 58.65/58.67 [44]~P5(x441)+P1(f14(x441))
% 58.65/58.67 [45]~P2(x451)+~E(f11(x451),f10(x451))
% 58.65/58.67 [46]~P2(x461)+P4(f10(x461),x461)
% 58.65/58.67 [47]~P2(x471)+P4(f11(x471),x471)
% 58.65/58.67 [48]~P5(x481)+P4(f13(x481),x481)
% 58.65/58.67 [49]~P2(x491)+~P4(f12(x491),x491)
% 58.65/58.67 [50]~P5(x501)+~P4(f14(x501),x501)
% 58.65/58.67 [51]~P1(x512)+~P1(x511)+E(x511,x512)+P2(f4(x511,x512))
% 58.65/58.67 [52]~P1(x522)+~P1(x521)+E(x521,x522)+P4(x521,f4(x522,x521))
% 58.65/58.67 [53]~P1(x532)+~P1(x531)+E(x531,x532)+P4(x531,f4(x531,x532))
% 58.65/58.67 [56]~P1(x563)+~P5(x562)+~P5(x561)+~P4(x563,x562)+~P4(x563,x561)+E(x561,x562)+~E(f5(x561,x562,x563),x563)
% 58.65/58.67 [58]~P1(x583)+~P5(x582)+~P5(x581)+~P4(x583,x582)+~P4(x583,x581)+E(x581,x582)+P1(f5(x581,x582,x583))
% 58.65/58.67 [59]~P1(x593)+~P5(x592)+~P5(x591)+~P4(x593,x592)+~P4(x593,x591)+E(x591,x592)+P4(f5(x591,x592,x593),x592)
% 58.65/58.67 [60]~P1(x603)+~P5(x602)+~P5(x601)+~P4(x603,x602)+~P4(x603,x601)+E(x601,x602)+P4(f5(x601,x602,x603),x601)
% 58.65/58.67 [61]E(x613,x611)+P3(x613,x611,x612)+~P1(x612)+~P1(x611)+~P1(x613)+E(x611,x612)+E(x613,x612)+P5(f6(x613,x611,x612))
% 58.65/58.67 [62]E(x623,x621)+P3(x621,x622,x623)+~P1(x622)+~P1(x621)+~P1(x623)+E(x621,x622)+E(x623,x622)+P4(x623,f6(x621,x622,x623))
% 58.65/58.67 [63]E(x633,x631)+P3(x631,x633,x632)+~P1(x632)+~P1(x631)+~P1(x633)+E(x631,x632)+E(x633,x632)+P4(x633,f6(x631,x633,x632))
% 58.65/58.67 [64]E(x643,x641)+P3(x643,x641,x642)+~P1(x642)+~P1(x641)+~P1(x643)+E(x641,x642)+E(x643,x642)+P4(x643,f6(x643,x641,x642))
% 58.65/58.67 [65]E(x653,x651)+~P1(x652)+~P1(x651)+~P1(x653)+~P3(x653,x651,x652)+E(x651,x652)+E(x653,x652)+P2(f7(x653,x651,x652))
% 58.65/58.67 [66]E(x663,x661)+~P1(x662)+~P1(x661)+~P1(x663)+~P3(x663,x661,x662)+E(x661,x662)+E(x663,x662)+P4(x662,f7(x663,x661,x662))
% 58.65/58.67 [67]E(x673,x671)+~P1(x672)+~P1(x671)+~P1(x673)+~P3(x673,x671,x672)+E(x671,x672)+E(x673,x672)+P4(x671,f7(x673,x671,x672))
% 58.65/58.67 [68]E(x683,x681)+~P1(x682)+~P1(x681)+~P1(x683)+~P3(x683,x681,x682)+E(x681,x682)+E(x683,x682)+P4(x683,f7(x683,x681,x682))
% 58.65/58.67 [54]~P1(x544)+~P1(x543)+~P2(x542)+~P2(x541)+~P4(x544,x542)+~P4(x544,x541)+~P4(x543,x542)+~P4(x543,x541)+E(x541,x542)+E(x543,x544)
% 58.65/58.68 [55]~P1(x552)+~P1(x551)+~P2(x553)+~P5(x554)+~P4(x552,x554)+~P4(x552,x553)+~P4(x551,x554)+~P4(x551,x553)+E(x551,x552)+P4(x553,x554)
% 58.65/58.68 [57]E(x573,x571)+P3(x573,x571,x572)+~P1(x572)+~P1(x571)+~P1(x573)+~P4(x572,x574)+~P4(x571,x574)+~P4(x573,x574)+E(x571,x572)+E(x573,x572)+~P2(x574)
% 58.65/58.68 [69]E(x695,x693)+P3(x695,x693,x694)+~P1(x694)+~P1(x693)+~P1(x695)+~P5(x692)+~P5(x691)+~P4(x694,x692)+~P4(x694,x691)+~P4(x693,x692)+~P4(x693,x691)+~P4(x695,x692)+~P4(x695,x691)+E(x691,x692)+E(x693,x694)+E(x695,x694)
% 58.65/58.68 %EqnAxiom
% 58.65/58.68 [1]E(x11,x11)
% 58.65/58.68 [2]E(x22,x21)+~E(x21,x22)
% 58.65/58.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.65/58.68 [4]~E(x41,x42)+E(f10(x41),f10(x42))
% 58.65/58.68 [5]~E(x51,x52)+E(f11(x51),f11(x52))
% 58.65/58.68 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 58.65/58.68 [7]~E(x71,x72)+E(f13(x71),f13(x72))
% 58.65/58.68 [8]~E(x81,x82)+E(f14(x81),f14(x82))
% 58.65/58.68 [9]~E(x91,x92)+E(f7(x91,x93,x94),f7(x92,x93,x94))
% 58.65/58.68 [10]~E(x101,x102)+E(f7(x103,x101,x104),f7(x103,x102,x104))
% 58.65/58.68 [11]~E(x111,x112)+E(f7(x113,x114,x111),f7(x113,x114,x112))
% 58.65/58.68 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 58.65/58.68 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 58.65/58.68 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 58.65/58.68 [15]~E(x151,x152)+E(f5(x151,x153,x154),f5(x152,x153,x154))
% 58.65/58.68 [16]~E(x161,x162)+E(f5(x163,x161,x164),f5(x163,x162,x164))
% 58.65/58.68 [17]~E(x171,x172)+E(f5(x173,x174,x171),f5(x173,x174,x172))
% 58.65/58.68 [18]~E(x181,x182)+E(f4(x181,x183),f4(x182,x183))
% 58.65/58.68 [19]~E(x191,x192)+E(f4(x193,x191),f4(x193,x192))
% 58.65/58.68 [20]~P1(x201)+P1(x202)+~E(x201,x202)
% 58.65/58.68 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213)
% 58.65/58.68 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221)
% 58.65/58.68 [23]~P5(x231)+P5(x232)+~E(x231,x232)
% 58.65/58.68 [24]~P2(x241)+P2(x242)+~E(x241,x242)
% 58.65/58.68 [25]P3(x252,x253,x254)+~E(x251,x252)+~P3(x251,x253,x254)
% 58.65/58.68 [26]P3(x263,x262,x264)+~E(x261,x262)+~P3(x263,x261,x264)
% 58.65/58.68 [27]P3(x273,x274,x272)+~E(x271,x272)+~P3(x273,x274,x271)
% 58.65/58.68
% 58.65/58.68 %-------------------------------------------
% 58.65/58.68 cnf(70,plain,
% 58.65/58.68 (~E(a8,a9)),
% 58.65/58.68 inference(scs_inference,[],[34,39,21])).
% 58.65/58.68 cnf(1400,plain,
% 58.65/58.68 (~E(f11(a3),a9)),
% 58.65/58.68 inference(scs_inference,[],[32,39,47,21])).
% 58.65/58.68 cnf(3714,plain,
% 58.65/58.68 (~E(a8,a1)),
% 58.65/58.68 inference(scs_inference,[],[36,2])).
% 58.65/58.68 cnf(3715,plain,
% 58.65/58.68 (~E(x37151,a8)+~E(a1,x37151)),
% 58.65/58.68 inference(scs_inference,[],[36,2,3])).
% 58.65/58.68 cnf(3719,plain,
% 58.65/58.68 (~E(a9,a1)),
% 58.65/58.68 inference(scs_inference,[],[37,2])).
% 58.65/58.68 cnf(3724,plain,
% 58.65/58.68 (~E(x37241,a9)+~E(a8,x37241)),
% 58.65/58.68 inference(scs_inference,[],[70,1400,2,3])).
% 58.65/58.68 cnf(3762,plain,
% 58.65/58.68 (~E(x37621,a1)+~E(a9,x37621)),
% 58.65/58.68 inference(scs_inference,[],[3719,3])).
% 58.65/58.68 cnf(3763,plain,
% 58.65/58.68 (~E(x37631,a9)+~E(x37631,a1)),
% 58.65/58.68 inference(scs_inference,[],[3719,3,2])).
% 58.65/58.68 cnf(3782,plain,
% 58.65/58.68 (~E(x37821,a1)+~E(x37821,a8)),
% 58.65/58.68 inference(scs_inference,[],[3715,2])).
% 58.65/58.68 cnf(3840,plain,
% 58.65/58.68 (P2(f7(a1,a8,a9))),
% 58.65/58.68 inference(scs_inference,[],[29,28,35,37,36,30,3724,65])).
% 58.65/58.68 cnf(3888,plain,
% 58.65/58.68 (P4(a9,f4(a1,a9))),
% 58.65/58.68 inference(scs_inference,[],[28,30,3762,52])).
% 58.65/58.68 cnf(3904,plain,
% 58.65/58.68 (P4(a1,f4(a9,a1))),
% 58.65/58.68 inference(scs_inference,[],[30,28,3763,52])).
% 58.65/58.68 cnf(3935,plain,
% 58.65/58.68 (P4(a9,f7(a1,a8,a9))),
% 58.65/58.68 inference(scs_inference,[],[29,28,35,70,37,30,3782,66])).
% 58.65/58.68 cnf(6541,plain,
% 58.65/58.68 (P4(a8,f7(a1,a8,a9))),
% 58.65/58.68 inference(scs_inference,[],[35,3888,39,32,28,37,29,70,36,30,40,42,46,45,49,22,67])).
% 58.65/58.68 cnf(6551,plain,
% 58.65/58.68 (~P4(a1,f7(a1,a8,a9))),
% 58.65/58.68 inference(scs_inference,[],[6541,3714,33,39,34,32,28,29,3935,3840,22,54])).
% 58.65/58.68 cnf(6568,plain,
% 58.65/58.68 ($false),
% 58.65/58.68 inference(scs_inference,[],[35,3904,6551,28,37,29,70,36,30,22,68]),
% 58.65/58.68 ['proof']).
% 58.65/58.68 % SZS output end Proof
% 58.65/58.68 % Total time :58.040000s
%------------------------------------------------------------------------------