%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO076-4 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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 116.17s 116.23s
% Output : CNFRefutation 116.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO076-4 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.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:04:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 116.17/116.22 %-------------------------------------------
% 116.17/116.22 % File :CSE---1.7
% 116.17/116.22 % Problem :theBenchmark
% 116.17/116.22 % Transform :cnf
% 116.17/116.22 % Format :tptp:raw
% 116.17/116.22 % Command :java -jar mcs_scs.jar %d %s
% 116.17/116.22
% 116.17/116.22 % Result :Theorem 115.620000s
% 116.17/116.22 % Output :CNFRefutation 115.620000s
% 116.17/116.22 %-------------------------------------------
% 116.17/116.23 %--------------------------------------------------------------------------
% 116.17/116.23 % File : GEO076-4 : TPTP v8.2.0. Released v1.0.0.
% 116.17/116.23 % Domain : Geometry (Hilbert)
% 116.17/116.23 % Problem : There is no point on every line
% 116.17/116.23 % Version : [Ben92] axioms.
% 116.17/116.23 % English :
% 116.17/116.23
% 116.17/116.23 % Refs : [Ben92] Benanav (1992), Recognising Unnecessary Clauses in Res
% 116.17/116.23 % Source : [Ben92]
% 116.17/116.23 % Names : G15 [Ben92]
% 116.17/116.23
% 116.17/116.23 % Status : Unsatisfiable
% 116.17/116.23 % Rating : 0.15 v8.2.0, 0.14 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.36 v6.0.0, 0.40 v5.5.0, 0.55 v5.3.0, 0.61 v5.2.0, 0.56 v5.1.0, 0.59 v5.0.0, 0.43 v4.1.0, 0.38 v4.0.1, 0.45 v4.0.0, 0.36 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.42 v3.3.0, 0.43 v3.2.0, 0.46 v3.1.0, 0.45 v2.7.0, 0.42 v2.6.0, 0.30 v2.5.0, 0.58 v2.4.0, 0.44 v2.2.1, 0.67 v2.2.0, 0.78 v2.1.0, 0.89 v2.0.0
% 116.17/116.23 % Syntax : Number of clauses : 33 ( 2 unt; 18 nHn; 33 RR)
% 116.17/116.23 % Number of literals : 177 ( 43 equ; 104 neg)
% 116.17/116.23 % Maximal clause size : 16 ( 5 avg)
% 116.17/116.23 % Maximal term depth : 2 ( 1 avg)
% 116.17/116.23 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty)
% 116.17/116.23 % Number of functors : 11 ( 11 usr; 2 con; 0-3 aty)
% 116.17/116.23 % Number of variables : 71 ( 0 sgn)
% 116.17/116.23 % SPC : CNF_UNS_RFO_SEQ_NHN
% 116.17/116.23
% 116.17/116.23 % Comments :
% 116.17/116.23 %--------------------------------------------------------------------------
% 116.17/116.23 %----Include axioms for Hilbert geometry
% 116.17/116.23 include('Axioms/GEO003-0.ax').
% 116.17/116.23 %--------------------------------------------------------------------------
% 116.17/116.23 cnf(there_is_a_point,hypothesis,
% 116.17/116.23 point(a_point) ).
% 116.17/116.23
% 116.17/116.23 cnf(prove_point_is_not_on_every_line,negated_conjecture,
% 116.17/116.23 ( ~ line(Line)
% 116.17/116.23 | on(a_point,Line) ) ).
% 116.17/116.23
% 116.17/116.23 %--------------------------------------------------------------------------
% 116.17/116.23 %-------------------------------------------
% 116.17/116.23 % Proof found
% 116.17/116.23 % SZS status Theorem for theBenchmark
% 116.17/116.23 % SZS output start Proof
% 116.17/116.23 %ClaNum:60(EqnAxiom:27)
% 116.17/116.23 %VarNum:306(SingletonVarNum:71)
% 116.17/116.23 %MaxLitNum:16
% 116.17/116.23 %MaxfuncDepth:1
% 116.17/116.23 %SharedTerms:4
% 116.17/116.23 %goalClause: 35
% 116.17/116.23 [28]P1(a1)
% 116.17/116.23 [29]P2(a2)
% 116.17/116.23 [35]~P2(x351)+P5(a1,x351)
% 116.17/116.23 [30]~P2(x301)+P1(f3(x301))
% 116.17/116.23 [31]~P2(x311)+P1(f8(x311))
% 116.17/116.23 [32]~P2(x321)+P1(f9(x321))
% 116.17/116.23 [33]~P4(x331)+P1(f10(x331))
% 116.17/116.23 [34]~P4(x341)+P1(f11(x341))
% 116.17/116.24 [36]~P2(x361)+~E(f8(x361),f3(x361))
% 116.17/116.24 [37]~P2(x371)+P5(f3(x371),x371)
% 116.17/116.24 [38]~P2(x381)+P5(f8(x381),x381)
% 116.17/116.24 [39]~P4(x391)+P5(f10(x391),x391)
% 116.17/116.24 [40]~P2(x401)+~P5(f9(x401),x401)
% 116.17/116.24 [41]~P4(x411)+~P5(f11(x411),x411)
% 116.17/116.24 [42]~P1(x422)+~P1(x421)+E(x421,x422)+P2(f4(x421,x422))
% 116.17/116.24 [43]~P1(x432)+~P1(x431)+E(x431,x432)+P5(x431,f4(x432,x431))
% 116.17/116.24 [44]~P1(x442)+~P1(x441)+E(x441,x442)+P5(x441,f4(x441,x442))
% 116.17/116.24 [47]~P1(x473)+~P4(x472)+~P4(x471)+~P5(x473,x472)+~P5(x473,x471)+E(x471,x472)+~E(f5(x471,x472,x473),x473)
% 116.17/116.24 [49]~P1(x493)+~P4(x492)+~P4(x491)+~P5(x493,x492)+~P5(x493,x491)+E(x491,x492)+P1(f5(x491,x492,x493))
% 116.17/116.24 [50]~P1(x503)+~P4(x502)+~P4(x501)+~P5(x503,x502)+~P5(x503,x501)+E(x501,x502)+P5(f5(x501,x502,x503),x502)
% 116.17/116.24 [51]~P1(x513)+~P4(x512)+~P4(x511)+~P5(x513,x512)+~P5(x513,x511)+E(x511,x512)+P5(f5(x511,x512,x513),x511)
% 116.17/116.24 [52]E(x523,x521)+P3(x523,x521,x522)+~P1(x522)+~P1(x521)+~P1(x523)+E(x521,x522)+E(x523,x522)+P4(f6(x523,x521,x522))
% 116.17/116.24 [53]E(x533,x531)+P3(x531,x532,x533)+~P1(x532)+~P1(x531)+~P1(x533)+E(x531,x532)+E(x533,x532)+P5(x533,f6(x531,x532,x533))
% 116.17/116.24 [54]E(x543,x541)+P3(x541,x543,x542)+~P1(x542)+~P1(x541)+~P1(x543)+E(x541,x542)+E(x543,x542)+P5(x543,f6(x541,x543,x542))
% 116.17/116.24 [55]E(x553,x551)+P3(x553,x551,x552)+~P1(x552)+~P1(x551)+~P1(x553)+E(x551,x552)+E(x553,x552)+P5(x553,f6(x553,x551,x552))
% 116.17/116.24 [56]E(x563,x561)+~P1(x562)+~P1(x561)+~P1(x563)+~P3(x563,x561,x562)+E(x561,x562)+E(x563,x562)+P2(f7(x563,x561,x562))
% 116.17/116.24 [57]E(x573,x571)+~P1(x572)+~P1(x571)+~P1(x573)+~P3(x573,x571,x572)+E(x571,x572)+E(x573,x572)+P5(x572,f7(x573,x571,x572))
% 116.17/116.24 [58]E(x583,x581)+~P1(x582)+~P1(x581)+~P1(x583)+~P3(x583,x581,x582)+E(x581,x582)+E(x583,x582)+P5(x581,f7(x583,x581,x582))
% 116.17/116.24 [59]E(x593,x591)+~P1(x592)+~P1(x591)+~P1(x593)+~P3(x593,x591,x592)+E(x591,x592)+E(x593,x592)+P5(x593,f7(x593,x591,x592))
% 116.17/116.24 [45]~P1(x454)+~P1(x453)+~P2(x452)+~P2(x451)+~P5(x454,x452)+~P5(x454,x451)+~P5(x453,x452)+~P5(x453,x451)+E(x451,x452)+E(x453,x454)
% 116.17/116.24 [46]~P1(x462)+~P1(x461)+~P2(x463)+~P4(x464)+~P5(x462,x464)+~P5(x462,x463)+~P5(x461,x464)+~P5(x461,x463)+E(x461,x462)+P5(x463,x464)
% 116.17/116.24 [48]E(x483,x481)+P3(x483,x481,x482)+~P1(x482)+~P1(x481)+~P1(x483)+~P5(x482,x484)+~P5(x481,x484)+~P5(x483,x484)+E(x481,x482)+E(x483,x482)+~P2(x484)
% 116.17/116.24 [60]E(x605,x603)+P3(x605,x603,x604)+~P1(x604)+~P1(x603)+~P1(x605)+~P4(x602)+~P4(x601)+~P5(x604,x602)+~P5(x604,x601)+~P5(x603,x602)+~P5(x603,x601)+~P5(x605,x602)+~P5(x605,x601)+E(x601,x602)+E(x603,x604)+E(x605,x604)
% 116.17/116.24 %EqnAxiom
% 116.17/116.24 [1]E(x11,x11)
% 116.17/116.24 [2]E(x22,x21)+~E(x21,x22)
% 116.17/116.24 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 116.17/116.24 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 116.17/116.24 [5]~E(x51,x52)+E(f8(x51),f8(x52))
% 116.17/116.24 [6]~E(x61,x62)+E(f9(x61),f9(x62))
% 116.17/116.24 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 116.17/116.24 [8]~E(x81,x82)+E(f11(x81),f11(x82))
% 116.17/116.24 [9]~E(x91,x92)+E(f7(x91,x93,x94),f7(x92,x93,x94))
% 116.17/116.24 [10]~E(x101,x102)+E(f7(x103,x101,x104),f7(x103,x102,x104))
% 116.17/116.24 [11]~E(x111,x112)+E(f7(x113,x114,x111),f7(x113,x114,x112))
% 116.17/116.24 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 116.17/116.24 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 116.17/116.24 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 116.17/116.24 [15]~E(x151,x152)+E(f5(x151,x153,x154),f5(x152,x153,x154))
% 116.17/116.24 [16]~E(x161,x162)+E(f5(x163,x161,x164),f5(x163,x162,x164))
% 116.17/116.24 [17]~E(x171,x172)+E(f5(x173,x174,x171),f5(x173,x174,x172))
% 116.17/116.24 [18]~E(x181,x182)+E(f4(x181,x183),f4(x182,x183))
% 116.17/116.24 [19]~E(x191,x192)+E(f4(x193,x191),f4(x193,x192))
% 116.17/116.24 [20]~P1(x201)+P1(x202)+~E(x201,x202)
% 116.17/116.24 [21]~P2(x211)+P2(x212)+~E(x211,x212)
% 116.17/116.24 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223)
% 116.17/116.24 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231)
% 116.17/116.24 [24]~P4(x241)+P4(x242)+~E(x241,x242)
% 116.17/116.24 [25]P3(x252,x253,x254)+~E(x251,x252)+~P3(x251,x253,x254)
% 116.17/116.24 [26]P3(x263,x262,x264)+~E(x261,x262)+~P3(x263,x261,x264)
% 116.17/116.24 [27]P3(x273,x274,x272)+~E(x271,x272)+~P3(x273,x274,x271)
% 116.17/116.24
% 116.17/116.24 %-------------------------------------------
% 116.17/116.24 cnf(61,plain,
% 116.17/116.24 (~E(a2,x611)+P1(f3(x611))),
% 116.17/116.24 inference(scs_inference,[],[29,30,21])).
% 116.17/116.24 cnf(62,plain,
% 116.17/116.24 (P1(f3(a2))),
% 116.17/116.24 inference(equality_inference,[],[61])).
% 116.17/116.24 cnf(63,plain,
% 116.17/116.24 (~E(a2,x631)+P1(f8(x631))),
% 116.17/116.24 inference(scs_inference,[],[29,31,21])).
% 116.17/116.24 cnf(64,plain,
% 116.17/116.25 (P1(f8(a2))),
% 116.17/116.25 inference(equality_inference,[],[63])).
% 116.17/116.25 cnf(65,plain,
% 116.17/116.25 (~E(a2,x651)+P1(f9(x651))),
% 116.17/116.25 inference(scs_inference,[],[29,32,21])).
% 116.17/116.25 cnf(66,plain,
% 116.17/116.25 (P1(f9(a2))),
% 116.17/116.25 inference(equality_inference,[],[65])).
% 116.17/116.25 cnf(71,plain,
% 116.17/116.25 (~E(a2,x711)+P5(a1,x711)),
% 116.17/116.25 inference(scs_inference,[],[29,35,21])).
% 116.17/116.25 cnf(72,plain,
% 116.17/116.25 (P5(a1,a2)),
% 116.17/116.25 inference(equality_inference,[],[71])).
% 116.17/116.25 cnf(73,plain,
% 116.17/116.25 (P5(x731,a2)+~E(a1,x731)),
% 116.17/116.25 inference(scs_inference,[],[72,22])).
% 116.17/116.25 cnf(77,plain,
% 116.17/116.25 (E(f3(x771),f3(x772))+~E(x772,x771)),
% 116.17/116.25 inference(scs_inference,[],[2,4])).
% 116.17/116.25 cnf(79,plain,
% 116.17/116.25 (~E(a2,x791)+P5(f3(x791),x791)),
% 116.17/116.25 inference(scs_inference,[],[29,37,21])).
% 116.17/116.25 cnf(80,plain,
% 116.17/116.25 (P5(f3(a2),a2)),
% 116.17/116.25 inference(equality_inference,[],[79])).
% 116.17/116.25 cnf(81,plain,
% 116.17/116.25 (P5(f3(a2),x811)+~E(a2,x811)),
% 116.17/116.25 inference(scs_inference,[],[80,23])).
% 116.17/116.25 cnf(82,plain,
% 116.17/116.25 (P5(x821,a2)+~E(f3(a2),x821)),
% 116.17/116.25 inference(scs_inference,[],[80,23,22])).
% 116.17/116.25 cnf(87,plain,
% 116.17/116.25 (~E(a2,x871)+P5(f8(x871),x871)),
% 116.17/116.25 inference(scs_inference,[],[29,38,21])).
% 116.17/116.25 cnf(88,plain,
% 116.17/116.25 (P5(f8(a2),a2)),
% 116.17/116.25 inference(equality_inference,[],[87])).
% 116.17/116.25 cnf(89,plain,
% 116.17/116.25 (P5(x891,a2)+~E(f8(a2),x891)),
% 116.17/116.25 inference(scs_inference,[],[88,22])).
% 116.17/116.25 cnf(100,plain,
% 116.17/116.25 (~E(a2,x1001)+~E(f8(x1001),f3(x1001))),
% 116.17/116.25 inference(scs_inference,[],[29,36,21])).
% 116.17/116.25 cnf(105,plain,
% 116.17/116.25 (~E(x1051,x1052)+E(f10(f11(x1051)),f10(f11(x1052)))),
% 116.17/116.25 inference(scs_inference,[],[7,8])).
% 116.17/116.25 cnf(107,plain,
% 116.17/116.25 (~E(f3(x1071),f8(x1071))+~E(a2,x1071)),
% 116.17/116.25 inference(scs_inference,[],[100,2])).
% 116.17/116.25 cnf(108,plain,
% 116.17/116.25 (P2(f4(f3(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,62,107,42])).
% 116.17/116.25 cnf(111,plain,
% 116.17/116.25 (~E(x1111,x1112)+E(f4(x1113,f7(x1114,x1111,x1115)),f4(x1113,f7(x1114,x1112,x1115)))),
% 116.17/116.25 inference(scs_inference,[],[19,10])).
% 116.17/116.25 cnf(115,plain,
% 116.17/116.25 (~E(x1151,x1152)+E(f6(x1153,f6(x1154,x1155,x1151),x1156),f6(x1153,f6(x1154,x1155,x1152),x1156))),
% 116.17/116.25 inference(scs_inference,[],[13,14])).
% 116.17/116.25 cnf(119,plain,
% 116.17/116.25 (~E(x1191,x1192)+E(f5(x1193,x1194,f3(x1192)),f5(x1193,x1194,f3(x1191)))),
% 116.17/116.25 inference(scs_inference,[],[17,77])).
% 116.17/116.25 cnf(308,plain,
% 116.17/116.25 (~E(f3(a2),f8(a2))),
% 116.17/116.25 inference(scs_inference,[],[29,2,36])).
% 116.17/116.25 cnf(501,plain,
% 116.17/116.25 (~E(x5011,a1)+P5(x5011,a2)),
% 116.17/116.25 inference(scs_inference,[],[2,73])).
% 116.17/116.25 cnf(552,plain,
% 116.17/116.25 (~E(x5521,f3(a2))+P5(x5521,a2)),
% 116.17/116.25 inference(scs_inference,[],[2,82])).
% 116.17/116.25 cnf(586,plain,
% 116.17/116.25 (~E(x5861,f8(a2))+P5(x5861,a2)),
% 116.17/116.25 inference(scs_inference,[],[2,89])).
% 116.17/116.25 cnf(620,plain,
% 116.17/116.25 (~E(x6201,a2)+~E(f8(x6201),f3(x6201))),
% 116.17/116.25 inference(scs_inference,[],[2,100])).
% 116.17/116.25 cnf(636,plain,
% 116.17/116.25 (~E(f3(x6361),f8(x6361))+~E(x6361,a2)),
% 116.17/116.25 inference(scs_inference,[],[620,2])).
% 116.17/116.25 cnf(652,plain,
% 116.17/116.25 (P5(f3(a2),f4(f8(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,62,636,43])).
% 116.17/116.25 cnf(653,plain,
% 116.17/116.25 (P5(x6531,f4(f8(a2),f3(a2)))+~E(f3(a2),x6531)),
% 116.17/116.25 inference(scs_inference,[],[652,22])).
% 116.17/116.25 cnf(838,plain,
% 116.17/116.25 (~E(x8381,f3(a2))+P5(x8381,f4(f8(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[2,653])).
% 116.17/116.25 cnf(872,plain,
% 116.17/116.25 (~E(x8721,f3(a2))+~E(x8721,f8(a2))),
% 116.17/116.25 inference(scs_inference,[],[308,2,3])).
% 116.17/116.25 cnf(982,plain,
% 116.17/116.25 (~E(f8(a2),x9821)+~E(x9821,f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[2,872])).
% 116.17/116.25 cnf(998,plain,
% 116.17/116.25 (~E(x9981,a2)+~E(f8(a2),f3(x9981))),
% 116.17/116.25 inference(scs_inference,[],[982,4])).
% 116.17/116.25 cnf(1014,plain,
% 116.17/116.25 (~E(f3(x10141),f8(a2))+~E(x10141,a2)),
% 116.17/116.25 inference(scs_inference,[],[998,2])).
% 116.17/116.25 cnf(1030,plain,
% 116.17/116.25 (P5(f3(a2),f4(f3(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,62,1014,44])).
% 116.17/116.25 cnf(1031,plain,
% 116.17/116.25 (P5(x10311,f4(f3(a2),f8(a2)))+~E(f3(a2),x10311)),
% 116.17/116.25 inference(scs_inference,[],[1030,22])).
% 116.17/116.25 cnf(1051,plain,
% 116.17/116.25 (~E(f3(f4(f3(a2),f8(a2))),f8(f4(f3(a2),f8(a2))))),
% 116.17/116.25 inference(scs_inference,[],[108,2,36])).
% 116.17/116.25 cnf(1224,plain,
% 116.17/116.25 (~E(x12241,f3(a2))+P5(x12241,f4(f3(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[2,1031])).
% 116.17/116.25 cnf(1368,plain,
% 116.17/116.25 (~E(x13681,a2)+P2(x13681)),
% 116.17/116.25 inference(scs_inference,[],[29,2,21])).
% 116.17/116.25 cnf(1385,plain,
% 116.17/116.25 (~P5(f9(x13851),x13851)+~E(x13851,a2)),
% 116.17/116.25 inference(scs_inference,[],[1368,40])).
% 116.17/116.25 cnf(1386,plain,
% 116.17/116.25 (~P5(f9(a2),a2)),
% 116.17/116.25 inference(equality_inference,[],[1385])).
% 116.17/116.25 cnf(1387,plain,
% 116.17/116.25 (~E(f3(a2),f9(a2))),
% 116.17/116.25 inference(scs_inference,[],[1386,82])).
% 116.17/116.25 cnf(1388,plain,
% 116.17/116.25 (~E(f8(a2),f9(a2))),
% 116.17/116.25 inference(scs_inference,[],[1386,82,89])).
% 116.17/116.25 cnf(1389,plain,
% 116.17/116.25 (~E(f9(a2),a1)),
% 116.17/116.25 inference(scs_inference,[],[1386,82,89,501])).
% 116.17/116.25 cnf(1390,plain,
% 116.17/116.25 (~E(f9(a2),f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[1386,82,89,501,552])).
% 116.17/116.25 cnf(1391,plain,
% 116.17/116.25 (~E(f9(a2),f8(a2))),
% 116.17/116.25 inference(scs_inference,[],[1386,82,89,501,552,586])).
% 116.17/116.25 cnf(1392,plain,
% 116.17/116.25 (~E(a1,f9(a2))),
% 116.17/116.25 inference(scs_inference,[],[72,1386,82,89,501,552,586,22])).
% 116.17/116.25 cnf(2095,plain,
% 116.17/116.25 (~P5(f9(f4(f8(a2),f9(a2))),f4(f8(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1388,66,64,40,42])).
% 116.17/116.25 cnf(2111,plain,
% 116.17/116.25 (~P5(f9(a2),x21111)+~E(x21111,a2)),
% 116.17/116.25 inference(scs_inference,[],[29,40,23])).
% 116.17/116.25 cnf(2223,plain,
% 116.17/116.25 (~P5(f9(f4(f9(a2),a1)),f4(f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[1389,28,66,40,42])).
% 116.17/116.25 cnf(2650,plain,
% 116.17/116.25 (P5(f9(a2),f4(f3(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1390,66,61,43])).
% 116.17/116.25 cnf(2651,plain,
% 116.17/116.25 (~E(f4(f3(a2),f9(a2)),a2)),
% 116.17/116.25 inference(scs_inference,[],[1386,2650,23])).
% 116.17/116.25 cnf(2781,plain,
% 116.17/116.25 (P5(f9(a2),f4(f9(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1390,66,61,44])).
% 116.17/116.25 cnf(2782,plain,
% 116.17/116.25 (~E(f4(f9(a2),f3(a2)),a2)),
% 116.17/116.25 inference(scs_inference,[],[1386,2781,23])).
% 116.17/116.25 cnf(3124,plain,
% 116.17/116.25 (P5(f3(a2),f4(f3(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1387,66,61,44])).
% 116.17/116.25 cnf(3495,plain,
% 116.17/116.25 (P2(f4(f3(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1387,66,61,42])).
% 116.17/116.25 cnf(3701,plain,
% 116.17/116.25 (~E(a2,f4(f9(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[2782,2])).
% 116.17/116.25 cnf(3707,plain,
% 116.17/116.25 (~E(f8(a2),f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[308,2])).
% 116.17/116.25 cnf(3720,plain,
% 116.17/116.25 (~E(x37201,f4(f9(a2),f3(a2)))+~E(a2,x37201)),
% 116.17/116.25 inference(scs_inference,[],[3701,3])).
% 116.17/116.25 cnf(3737,plain,
% 116.17/116.25 (~E(x37371,f8(a2))+~E(f9(a2),x37371)),
% 116.17/116.25 inference(scs_inference,[],[1391,3])).
% 116.17/116.25 cnf(3738,plain,
% 116.17/116.25 (~E(f9(x37381),f8(a2))+~E(a2,x37381)),
% 116.17/116.25 inference(scs_inference,[],[1391,3,6])).
% 116.17/116.25 cnf(3748,plain,
% 116.17/116.25 (~E(x37481,f9(a2))+~E(f8(a2),x37481)),
% 116.17/116.25 inference(scs_inference,[],[1388,3])).
% 116.17/116.25 cnf(3749,plain,
% 116.17/116.25 (~E(f8(x37491),f9(a2))+~E(a2,x37491)),
% 116.17/116.25 inference(scs_inference,[],[1388,3,5])).
% 116.17/116.25 cnf(3753,plain,
% 116.17/116.25 (~E(x37531,f9(a2))+~E(a1,x37531)),
% 116.17/116.25 inference(scs_inference,[],[1392,3])).
% 116.17/116.25 cnf(3754,plain,
% 116.17/116.25 (~E(x37541,a1)+~E(x37541,f9(a2))),
% 116.17/116.25 inference(scs_inference,[],[1392,3,2])).
% 116.17/116.25 cnf(3796,plain,
% 116.17/116.25 (~E(x37961,a2)+~E(a1,f9(x37961))),
% 116.17/116.25 inference(scs_inference,[],[3753,6])).
% 116.17/116.25 cnf(3812,plain,
% 116.17/116.25 (P5(a1,f4(a1,f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[66,28,3754,44])).
% 116.17/116.25 cnf(3844,plain,
% 116.17/116.25 (P5(a1,f4(f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[66,28,3796,43])).
% 116.17/116.25 cnf(3860,plain,
% 116.17/116.25 (~E(x38601,f9(a2))+~E(x38601,f8(a2))),
% 116.17/116.25 inference(scs_inference,[],[3737,2])).
% 116.17/116.25 cnf(3876,plain,
% 116.17/116.25 (~E(f8(a2),f9(x38761))+~E(a2,x38761)),
% 116.17/116.25 inference(scs_inference,[],[3738,2])).
% 116.17/116.25 cnf(3940,plain,
% 116.17/116.25 (~E(x39401,a2)+~E(f8(a2),f9(x39401))),
% 116.17/116.25 inference(scs_inference,[],[3748,6])).
% 116.17/116.25 cnf(3956,plain,
% 116.17/116.25 (~E(f9(a2),f8(x39561))+~E(a2,x39561)),
% 116.17/116.25 inference(scs_inference,[],[3749,2])).
% 116.17/116.25 cnf(4004,plain,
% 116.17/116.25 (~E(x40041,a2)+~E(f8(x40041),f9(a2))),
% 116.17/116.25 inference(scs_inference,[],[3860,5])).
% 116.17/116.25 cnf(4020,plain,
% 116.17/116.25 (P5(f8(a2),f4(f9(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[66,64,3876,43])).
% 116.17/116.25 cnf(4084,plain,
% 116.17/116.25 (~E(f9(x40841),f8(a2))+~E(x40841,a2)),
% 116.17/116.25 inference(scs_inference,[],[3940,2])).
% 116.17/116.25 cnf(4100,plain,
% 116.17/116.25 (P5(f9(a2),f4(f9(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,66,3956,44])).
% 116.17/116.25 cnf(4132,plain,
% 116.17/116.25 (~E(f9(a2),f8(x41321))+~E(x41321,a2)),
% 116.17/116.25 inference(scs_inference,[],[4004,2])).
% 116.17/116.25 cnf(4164,plain,
% 116.17/116.25 (P5(f9(a2),f4(f8(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,66,4084,43])).
% 116.17/116.25 cnf(4180,plain,
% 116.17/116.25 (P2(f4(f9(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[64,66,4132,42])).
% 116.17/116.25 cnf(4244,plain,
% 116.17/116.25 (~E(x42441,f3(a2))+~E(a2,f4(f9(a2),x42441))),
% 116.17/116.25 inference(scs_inference,[],[3720,19])).
% 116.17/116.25 cnf(5705,plain,
% 116.17/116.25 (P5(f8(a2),f4(f8(a2),f9(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1388,64,65,44])).
% 116.17/116.25 cnf(7215,plain,
% 116.17/116.25 (P5(x72151,f4(f9(a2),a1))+~E(a1,x72151)),
% 116.17/116.25 inference(scs_inference,[],[3844,22])).
% 116.17/116.25 cnf(7225,plain,
% 116.17/116.25 (P5(x72251,f4(a1,f9(a2)))+~E(a1,x72251)),
% 116.17/116.25 inference(scs_inference,[],[3812,22])).
% 116.17/116.25 cnf(7233,plain,
% 116.17/116.25 (P5(x72331,f4(f8(a2),f9(a2)))+~E(f9(a2),x72331)),
% 116.17/116.25 inference(scs_inference,[],[4164,22])).
% 116.17/116.25 cnf(7241,plain,
% 116.17/116.25 (P5(x72411,f4(f8(a2),f9(a2)))+~E(f8(a2),x72411)),
% 116.17/116.25 inference(scs_inference,[],[5705,22])).
% 116.17/116.25 cnf(8209,plain,
% 116.17/116.25 (E(f8(a2),a1)+P3(f8(a2),f9(a2),a1)+~P5(a1,f4(f9(a2),f8(a2)))),
% 116.17/116.25 inference(scs_inference,[],[4100,72,29,4180,1389,1388,66,4020,64,28,48])).
% 116.17/116.25 cnf(8210,plain,
% 116.17/116.25 (E(f8(a2),a1)+P3(f8(a2),f9(a2),a1)),
% 116.17/116.25 inference(scs_inference,[],[4180,8209,35])).
% 116.17/116.25 cnf(9857,plain,
% 116.17/116.25 (~P5(a1,f4(f3(a2),f9(a2)))+E(a1,f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[3124,72,2651,62,28,29,3495,81,45])).
% 116.17/116.25 cnf(9873,plain,
% 116.17/116.25 (E(a1,f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[3495,9857,35])).
% 116.17/116.25 cnf(9875,plain,
% 116.17/116.25 (~E(f8(a2),a1)),
% 116.17/116.25 inference(scs_inference,[],[9873,838,982])).
% 116.17/116.25 cnf(9877,plain,
% 116.17/116.25 (P5(f3(a2),f4(f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[9873,838,982,1224,7215])).
% 116.17/116.25 cnf(9879,plain,
% 116.17/116.25 (P3(f8(a2),f9(a2),a1)),
% 116.17/116.25 inference(scs_inference,[],[9873,838,982,1224,7215,7225,8210])).
% 116.17/116.25 cnf(9881,plain,
% 116.17/116.25 (E(f3(a2),a1)),
% 116.17/116.25 inference(scs_inference,[],[9873,838,982,1224,7215,7225,8210,77,2])).
% 116.17/116.25 cnf(9883,plain,
% 116.17/116.25 (P3(f8(a2),f9(a2),f3(a2))),
% 116.17/116.25 inference(scs_inference,[],[9873,3124,838,982,1224,7215,7225,8210,77,2,22,27])).
% 116.17/116.25 cnf(9884,plain,
% 116.17/116.25 (~E(a1,f8(a2))),
% 116.17/116.25 inference(scs_inference,[],[9873,3124,308,838,982,1224,7215,7225,8210,77,2,22,27,3])).
% 116.17/116.25 cnf(9904,plain,
% 116.17/116.25 (E(f3(a1),f3(f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[9881,77])).
% 116.17/116.25 cnf(11358,plain,
% 116.17/116.25 (P2(f7(f8(a2),f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[1386,9879,1389,28,9875,66,64,89,56])).
% 116.17/116.25 cnf(11381,plain,
% 116.17/116.25 (P5(f9(a2),f7(f8(a2),f9(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1386,64,62,3707,9883,1390,66,89,58])).
% 116.17/116.25 cnf(11392,plain,
% 116.17/116.25 (P2(f7(f8(a2),f9(a2),f3(a2)))),
% 116.17/116.25 inference(scs_inference,[],[1386,62,9883,64,66,1390,3707,89,56])).
% 116.17/116.25 cnf(11402,plain,
% 116.17/116.25 (P5(a1,f7(f8(a2),f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[1386,9879,66,28,1389,9875,64,89,57])).
% 116.17/116.25 cnf(11413,plain,
% 116.17/116.25 (P5(f8(a2),f7(f8(a2),f9(a2),a1))),
% 116.17/116.25 inference(scs_inference,[],[1386,9879,66,28,1389,64,9875,89,59])).
% 116.17/116.25 cnf(11815,plain,
% 116.17/116.25 (~E(f7(f8(a2),f9(a2),a1),a2)),
% 116.17/116.25 inference(scs_inference,[],[1389,64,9879,9875,1388,28,66,2111,58])).
% 116.17/116.25 cnf(13779,plain,
% 116.17/116.25 (E(f3(f7(f3(a2),x137791,x137792)),f3(f7(a1,x137791,x137792)))),
% 116.17/116.25 inference(scs_inference,[],[9881,4,9])).
% 116.17/116.25 cnf(13813,plain,
% 116.17/116.25 ($false),
% 116.17/116.25 inference(scs_inference,[],[1051,11381,11402,11413,11392,11358,11815,2095,13779,2223,9877,9904,64,28,9873,72,29,9875,9884,88,2111,105,12,14,16,4244,119,7233,7241,111,115,30,35,40,2,77,6,22,42,43,45]),
% 116.17/116.25 ['proof']).
% 116.17/116.25 % SZS output end Proof
% 116.17/116.25 % Total time :115.620000s
%------------------------------------------------------------------------------