%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO083-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:42 EDT 2024
% Result : Unsatisfiable 52.07s 52.29s
% Output : CNFRefutation 52.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO083-1 : TPTP v8.2.0. Released v2.4.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n017.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri Jun 21 10:29:24 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.56/0.61 start to proof:theBenchmark
% 52.07/52.28 %-------------------------------------------
% 52.07/52.28 % File :CSE---1.7
% 52.07/52.28 % Problem :theBenchmark
% 52.07/52.28 % Transform :cnf
% 52.07/52.28 % Format :tptp:raw
% 52.07/52.28 % Command :java -jar mcs_scs.jar %d %s
% 52.07/52.28
% 52.07/52.28 % Result :Theorem 51.490000s
% 52.07/52.28 % Output :CNFRefutation 51.490000s
% 52.07/52.28 %-------------------------------------------
% 52.07/52.29 %--------------------------------------------------------------------------
% 52.07/52.29 % File : GEO083-1 : TPTP v8.2.0. Released v2.4.0.
% 52.07/52.29 % Domain : Geometry (Oriented curves)
% 52.07/52.29 % Problem : Sum is monotone, part 1
% 52.07/52.29 % Version : [EHK99] axioms.
% 52.07/52.29 % English :
% 52.07/52.29
% 52.07/52.29 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 52.07/52.29 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 52.07/52.29 % Source : [TPTP]
% 52.07/52.29 % Names :
% 52.07/52.29
% 52.07/52.29 % Status : Unsatisfiable
% 52.07/52.29 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.21 v7.4.0, 0.18 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.27 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.29 v6.0.0, 0.40 v5.5.0, 0.65 v5.4.0, 0.60 v5.3.0, 0.61 v5.2.0, 0.50 v5.1.0, 0.59 v5.0.0, 0.50 v4.1.0, 0.62 v4.0.1, 0.64 v4.0.0, 0.55 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.50 v3.2.0, 0.46 v3.1.0, 0.45 v2.7.0, 0.42 v2.6.0, 0.44 v2.5.0, 0.67 v2.4.0
% 52.07/52.29 % Syntax : Number of clauses : 52 ( 5 unt; 21 nHn; 47 RR)
% 52.07/52.29 % Number of literals : 158 ( 21 equ; 79 neg)
% 52.07/52.29 % Maximal clause size : 12 ( 3 avg)
% 52.07/52.29 % Maximal term depth : 3 ( 1 avg)
% 52.07/52.29 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 52.07/52.29 % Number of functors : 18 ( 18 usr; 4 con; 0-3 aty)
% 52.07/52.29 % Number of variables : 126 ( 10 sgn)
% 52.07/52.29 % SPC : CNF_UNS_RFO_SEQ_NHN
% 52.07/52.29
% 52.07/52.29 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO083+1.p
% 52.07/52.29 %--------------------------------------------------------------------------
% 52.07/52.29 %----Include simple curve axioms
% 52.07/52.29 include('Axioms/GEO004-0.ax').
% 52.07/52.29 %--------------------------------------------------------------------------
% 52.07/52.29 cnf(corollary_2_6_1_67,negated_conjecture,
% 52.07/52.29 part_of(sk15,sk16) ).
% 52.07/52.29
% 52.07/52.29 cnf(corollary_2_6_1_68,negated_conjecture,
% 52.07/52.29 meet(sk17,sk14,sk15) ).
% 52.07/52.29
% 52.07/52.29 cnf(corollary_2_6_1_69,negated_conjecture,
% 52.07/52.29 meet(sk17,sk14,sk16) ).
% 52.07/52.29
% 52.07/52.29 cnf(corollary_2_6_1_70,negated_conjecture,
% 52.07/52.29 ~ part_of(sum(sk14,sk15),sum(sk14,sk16)) ).
% 52.07/52.29
% 52.07/52.29 %--------------------------------------------------------------------------
% 52.07/52.29 %-------------------------------------------
% 52.07/52.29 % Proof found
% 52.07/52.29 % SZS status Theorem for theBenchmark
% 52.07/52.29 % SZS output start Proof
% 52.15/52.30 %ClaNum:90(EqnAxiom:43)
% 52.15/52.30 %VarNum:331(SingletonVarNum:113)
% 52.15/52.31 %MaxLitNum:12
% 52.15/52.31 %MaxfuncDepth:2
% 52.15/52.31 %SharedTerms:10
% 52.15/52.31 %goalClause: 44 46 47 48
% 52.15/52.31 %singleGoalClaCount:4
% 52.15/52.31 [44]P1(a1,a16)
% 52.15/52.31 [46]P6(a17,a14,a1)
% 52.15/52.31 [47]P6(a17,a14,a16)
% 52.15/52.31 [48]~P1(f18(a14,a1),f18(a14,a16))
% 52.15/52.31 [45]P2(f2(x451),x451)
% 52.15/52.31 [49]P3(x491)+P4(f3(x491),x491)
% 52.15/52.31 [51]~P7(x511)+P4(f13(x511),x511)
% 52.15/52.31 [50]P7(x501)+~P4(x502,x501)
% 52.15/52.31 [53]~P3(x531)+~P4(x532,x531)
% 52.15/52.31 [54]~P4(x541,x542)+P5(x541,x542)
% 52.15/52.31 [55]~P2(x551,x552)+P5(x551,x552)
% 52.15/52.31 [56]~P2(x561,x562)+~P4(x561,x562)
% 52.15/52.31 [57]~P4(x571,x572)+~E(f4(x571,x572),x571)
% 52.15/52.31 [59]P1(x591,x592)+P5(f5(x591,x592),x591)
% 52.15/52.31 [63]~P4(x631,x632)+P4(f4(x631,x632),x632)
% 52.15/52.31 [70]P1(x701,x702)+~P5(f5(x701,x702),x702)
% 52.15/52.31 [77]~P2(x771,x772)+P6(x771,f15(x771,x772),f6(x771,x772))
% 52.15/52.31 [72]~P2(x721,x722)+E(f18(f15(x721,x722),f6(x721,x722)),x722)
% 52.15/52.31 [73]P5(x731,x732)+~P6(x731,x733,x732)
% 52.15/52.31 [74]P5(x741,x742)+~P6(x741,x742,x743)
% 52.15/52.31 [75]~P6(x753,x752,x751)+E(f9(x751,x752),f18(x752,x751))
% 52.15/52.31 [52]P7(x521)+~P1(x521,x522)+E(x521,x522)
% 52.15/52.31 [58]P2(x581,x582)+~P5(x581,x582)+P4(x581,x582)
% 52.15/52.31 [66]~P5(x661,x662)+P4(x661,x662)+P5(x661,f7(x662,x661))
% 52.15/52.31 [67]~P5(x671,x672)+P4(x671,x672)+P5(x671,f11(x672,x671))
% 52.15/52.31 [68]~P5(x681,x682)+P4(x681,x682)+P1(f7(x682,x681),x682)
% 52.15/52.31 [69]~P5(x691,x692)+P4(x691,x692)+P1(f11(x692,x691),x692)
% 52.15/52.31 [71]E(x711,x712)+P5(f8(x711,x712),x712)+P5(f8(x711,x712),x711)
% 52.15/52.31 [76]E(x761,x762)+~P5(f8(x761,x762),x762)+~P5(f8(x761,x762),x761)
% 52.15/52.31 [78]~P5(x781,x782)+P4(x781,x782)+~P1(f7(x782,x781),f11(x782,x781))
% 52.15/52.31 [79]~P5(x791,x792)+P4(x791,x792)+~P1(f11(x792,x791),f7(x792,x791))
% 52.15/52.31 [60]~P5(x601,x603)+P5(x601,x602)+~P1(x603,x602)
% 52.15/52.31 [88]~P5(f10(x883,x882,x881),x881)+~P5(f10(x883,x882,x881),x882)+E(x881,f18(x882,x883))
% 52.15/52.31 [89]~P5(f10(x893,x892,x891),x891)+~P5(f10(x893,x892,x891),x893)+E(x891,f18(x892,x893))
% 52.15/52.31 [61]~P5(x611,x614)+P5(x611,x612)+~E(x612,f18(x613,x614))
% 52.15/52.31 [62]~P5(x621,x623)+P5(x621,x622)+~E(x622,f18(x623,x624))
% 52.15/52.31 [84]~P5(x841,x843)+~P5(x841,x842)+P6(x841,x842,x843)+P5(f12(x843,x842,x841),x843)
% 52.15/52.31 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f12(x853,x852,x851),x852)
% 52.15/52.31 [87]P5(f10(x873,x872,x871),x871)+P5(f10(x873,x872,x871),x872)+P5(f10(x873,x872,x871),x873)+E(x871,f18(x872,x873))
% 52.15/52.31 [81]~P5(x811,x812)+P4(x811,x812)+~P6(x814,x813,x812)+~P5(x811,x813)
% 52.15/52.31 [82]~P5(x821,x822)+P4(x821,x822)+~P6(x824,x822,x823)+~P5(x821,x823)
% 52.15/52.31 [65]~P5(x651,x654)+P5(x651,x652)+P5(x651,x653)+~E(x654,f18(x653,x652))
% 52.15/52.31 [90]~P5(x901,x903)+~P5(x901,x902)+P6(x901,x902,x903)+~P4(f12(x903,x902,x901),x903)+~P4(f12(x903,x902,x901),x902)
% 52.15/52.31 [83]~P3(x834)+~P4(x831,x832)+P6(x831,x832,x833)+~P6(x835,x832,x833)+~E(x834,f18(x832,x833))
% 52.15/52.31 [64]E(x643,x641)+~P4(x641,x644)+~P4(x643,x644)+E(x641,x642)+E(x643,x642)+~P4(x642,x644)
% 52.15/52.31 [80]P1(x802,x801)+~P1(x802,x803)+~P5(x804,x802)+~P4(x804,x803)+P1(x801,x802)+~P1(x801,x803)+~P5(x804,x801)
% 52.15/52.31 [86]P1(x862,x861)+P1(x862,x863)+P1(x863,x861)+P1(x863,x862)+~P1(x862,x864)+~P1(x863,x864)+~P4(x865,x862)+~P4(x865,x863)+P1(x861,x862)+P1(x861,x863)+~P1(x861,x864)+~P4(x865,x861)
% 52.15/52.31 %EqnAxiom
% 52.15/52.31 [1]E(x11,x11)
% 52.15/52.31 [2]E(x22,x21)+~E(x21,x22)
% 52.15/52.31 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 52.15/52.31 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 52.15/52.31 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53))
% 52.15/52.31 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62))
% 52.15/52.31 [7]~E(x71,x72)+E(f12(x71,x73,x74),f12(x72,x73,x74))
% 52.15/52.31 [8]~E(x81,x82)+E(f12(x83,x81,x84),f12(x83,x82,x84))
% 52.15/52.31 [9]~E(x91,x92)+E(f12(x93,x94,x91),f12(x93,x94,x92))
% 52.15/52.31 [10]~E(x101,x102)+E(f3(x101),f3(x102))
% 52.15/52.31 [11]~E(x111,x112)+E(f13(x111),f13(x112))
% 52.15/52.31 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123))
% 52.15/52.31 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132))
% 52.15/52.31 [14]~E(x141,x142)+E(f5(x141,x143),f5(x142,x143))
% 52.15/52.31 [15]~E(x151,x152)+E(f5(x153,x151),f5(x153,x152))
% 52.15/52.31 [16]~E(x161,x162)+E(f10(x161,x163,x164),f10(x162,x163,x164))
% 52.15/52.31 [17]~E(x171,x172)+E(f10(x173,x171,x174),f10(x173,x172,x174))
% 52.15/52.31 [18]~E(x181,x182)+E(f10(x183,x184,x181),f10(x183,x184,x182))
% 52.15/52.31 [19]~E(x191,x192)+E(f7(x191,x193),f7(x192,x193))
% 52.15/52.31 [20]~E(x201,x202)+E(f7(x203,x201),f7(x203,x202))
% 52.15/52.31 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213))
% 52.15/52.31 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222))
% 52.15/52.31 [23]~E(x231,x232)+E(f9(x231,x233),f9(x232,x233))
% 52.15/52.31 [24]~E(x241,x242)+E(f9(x243,x241),f9(x243,x242))
% 52.15/52.31 [25]~E(x251,x252)+E(f8(x251,x253),f8(x252,x253))
% 52.15/52.31 [26]~E(x261,x262)+E(f8(x263,x261),f8(x263,x262))
% 52.15/52.31 [27]~E(x271,x272)+E(f6(x271,x273),f6(x272,x273))
% 52.15/52.31 [28]~E(x281,x282)+E(f6(x283,x281),f6(x283,x282))
% 52.15/52.31 [29]~E(x291,x292)+E(f15(x291,x293),f15(x292,x293))
% 52.15/52.31 [30]~E(x301,x302)+E(f15(x303,x301),f15(x303,x302))
% 52.15/52.31 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 52.15/52.31 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 52.15/52.31 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 52.15/52.31 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 52.15/52.31 [35]P6(x352,x353,x354)+~E(x351,x352)+~P6(x351,x353,x354)
% 52.15/52.31 [36]P6(x363,x362,x364)+~E(x361,x362)+~P6(x363,x361,x364)
% 52.15/52.31 [37]P6(x373,x374,x372)+~E(x371,x372)+~P6(x373,x374,x371)
% 52.15/52.31 [38]P5(x382,x383)+~E(x381,x382)+~P5(x381,x383)
% 52.15/52.31 [39]P5(x393,x392)+~E(x391,x392)+~P5(x393,x391)
% 52.15/52.31 [40]P4(x402,x403)+~E(x401,x402)+~P4(x401,x403)
% 52.15/52.31 [41]P4(x413,x412)+~E(x411,x412)+~P4(x413,x411)
% 52.15/52.31 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 52.15/52.31 [43]~P7(x431)+P7(x432)+~E(x431,x432)
% 52.15/52.31
% 52.15/52.31 %-------------------------------------------
% 52.15/52.32 cnf(91,plain,
% 52.15/52.32 (~P5(x911,x912)+P5(x911,f18(x913,x912))),
% 52.15/52.32 inference(equality_inference,[],[61])).
% 52.15/52.32 cnf(92,plain,
% 52.15/52.32 (~P5(x921,x922)+P5(x921,f18(x922,x923))),
% 52.15/52.32 inference(equality_inference,[],[62])).
% 52.15/52.32 cnf(93,plain,
% 52.15/52.32 (~P5(x931,f18(x932,x933))+P5(x931,x933)+P5(x931,x932)),
% 52.15/52.32 inference(equality_inference,[],[65])).
% 52.15/52.32 cnf(95,plain,
% 52.15/52.32 (~P5(x951,a1)+P5(x951,a16)),
% 52.15/52.32 inference(scs_inference,[],[44,60])).
% 52.15/52.32 cnf(321,plain,
% 52.15/52.32 (~E(x3211,f18(a14,a1))+P5(f5(x3211,f18(a14,a16)),x3211)),
% 52.15/52.32 inference(scs_inference,[],[48,59,31])).
% 52.15/52.32 cnf(322,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),f18(a14,a1))),
% 52.15/52.32 inference(equality_inference,[],[321])).
% 52.15/52.32 cnf(7680,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),a1)+P5(f5(f18(a14,a1),f18(a14,a16)),a14)),
% 52.15/52.32 inference(scs_inference,[],[322,93])).
% 52.15/52.32 cnf(8344,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),a14)+P5(f5(f18(a14,a1),f18(a14,a16)),a16)),
% 52.15/52.32 inference(scs_inference,[],[7680,95])).
% 52.15/52.32 cnf(8392,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),f18(x83921,a14))+P5(f5(f18(a14,a1),f18(a14,a16)),a16)),
% 52.15/52.32 inference(scs_inference,[],[8344,91])).
% 52.15/52.32 cnf(8498,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),f18(x84981,a16))+P5(f5(f18(a14,a1),f18(a14,a16)),f18(x84982,a14))),
% 52.15/52.32 inference(scs_inference,[],[8392,91])).
% 52.15/52.32 cnf(8514,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),f18(x85141,a14))),
% 52.15/52.32 inference(scs_inference,[],[48,8498,70])).
% 52.15/52.32 cnf(8530,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),x85301)+P5(f5(f18(a14,a1),f18(a14,a16)),a14)),
% 52.15/52.32 inference(scs_inference,[],[8514,93])).
% 52.15/52.32 cnf(8534,plain,
% 52.15/52.32 (P5(f5(f18(a14,a1),f18(a14,a16)),a14)),
% 52.15/52.32 inference(factoring_inference,[],[8530])).
% 52.15/52.32 cnf(8537,plain,
% 52.15/52.32 ($false),
% 52.15/52.32 inference(scs_inference,[],[48,8534,92,70]),
% 52.15/52.32 ['proof']).
% 52.15/52.32 % SZS output end Proof
% 52.15/52.32 % Total time :51.490000s
%------------------------------------------------------------------------------