%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO039-2 : 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 : n019.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:27 EDT 2024
% Result : Unsatisfiable 0.55s 0.93s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO039-2 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 08:28:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.51/0.59 start to proof:theBenchmark
% 0.55/0.93 %-------------------------------------------
% 0.55/0.93 % File :CSE---1.7
% 0.55/0.93 % Problem :theBenchmark
% 0.55/0.93 % Transform :cnf
% 0.55/0.93 % Format :tptp:raw
% 0.55/0.93 % Command :java -jar mcs_scs.jar %d %s
% 0.55/0.93
% 0.55/0.93 % Result :Theorem 0.300000s
% 0.55/0.93 % Output :CNFRefutation 0.300000s
% 0.55/0.93 %-------------------------------------------
% 0.55/0.93 %--------------------------------------------------------------------------
% 0.55/0.93 % File : GEO039-2 : TPTP v8.2.0. Released v1.0.0.
% 0.55/0.93 % Domain : Geometry
% 0.55/0.93 % Problem : Corollary the identity axiom for betweenness
% 0.55/0.93 % Version : [Qua89] axioms.
% 0.55/0.93 % English :
% 0.55/0.93
% 0.55/0.93 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 0.55/0.93 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 0.55/0.93 % Source : [TPTP]
% 0.55/0.93 % Names :
% 0.55/0.93
% 0.55/0.93 % Status : Unsatisfiable
% 0.55/0.93 % Rating : 0.15 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.29 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.30 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.15 v4.0.1, 0.18 v4.0.0, 0.27 v3.7.0, 0.10 v3.5.0, 0.18 v3.4.0, 0.17 v3.3.0, 0.21 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.10 v2.5.0, 0.08 v2.4.0, 0.00 v2.2.0, 0.22 v2.1.0, 0.22 v2.0.0
% 0.55/0.93 % Syntax : Number of clauses : 21 ( 9 unt; 5 nHn; 18 RR)
% 0.55/0.93 % Number of literals : 59 ( 8 equ; 35 neg)
% 0.55/0.93 % Maximal clause size : 8 ( 2 avg)
% 0.55/0.93 % Maximal term depth : 2 ( 1 avg)
% 0.55/0.93 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 0.55/0.93 % Number of functors : 12 ( 12 usr; 7 con; 0-6 aty)
% 0.55/0.93 % Number of variables : 71 ( 3 sgn)
% 0.55/0.93 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.55/0.93
% 0.55/0.93 % Comments : Proving corollaries from axioms is not usual.
% 0.55/0.93 %--------------------------------------------------------------------------
% 0.55/0.93 %----Include Tarski geometry axioms
% 0.55/0.93 include('Axioms/GEO002-0.ax').
% 0.55/0.93 %--------------------------------------------------------------------------
% 0.55/0.93 cnf(w_between_u_and_x,hypothesis,
% 0.55/0.93 between(u,w,x) ).
% 0.55/0.93
% 0.55/0.93 cnf(u_is_x,hypothesis,
% 0.55/0.93 u = x ).
% 0.55/0.93
% 0.55/0.93 cnf(prove_corollary,negated_conjecture,
% 0.55/0.93 ~ between(v,w,x) ).
% 0.55/0.93
% 0.55/0.93 %--------------------------------------------------------------------------
% 0.55/0.93 %-------------------------------------------
% 0.55/0.93 % Proof found
% 0.55/0.93 % SZS status Theorem for theBenchmark
% 0.55/0.93 % SZS output start Proof
% 0.55/0.94 %ClaNum:56(EqnAxiom:35)
% 0.55/0.94 %VarNum:211(SingletonVarNum:71)
% 0.55/0.94 %MaxLitNum:8
% 0.55/0.94 %MaxfuncDepth:1
% 0.55/0.94 %SharedTerms:13
% 0.55/0.94 %goalClause: 44
% 0.55/0.94 %singleGoalClaCount:1
% 0.55/0.94 [36]E(a1,a2)
% 0.55/0.94 [37]P1(a2,a11,a1)
% 0.55/0.94 [41]~P1(a7,a9,a10)
% 0.55/0.94 [42]~P1(a9,a10,a7)
% 0.55/0.94 [43]~P1(a10,a7,a9)
% 0.55/0.94 [44]~P1(a12,a11,a1)
% 0.55/0.94 [38]P2(x381,x382,x382,x381)
% 0.55/0.94 [39]P1(x391,x392,f3(x391,x392,x393,x394))
% 0.55/0.94 [40]P2(x401,f3(x402,x401,x403,x404),x403,x404)
% 0.55/0.94 [45]~P1(x451,x452,x451)+E(x451,x452)
% 0.55/0.94 [46]~P2(x461,x462,x463,x463)+E(x461,x462)
% 0.55/0.94 [50]~P1(x505,x501,x504)+~P1(x502,x503,x504)+P1(x501,f8(x502,x503,x504,x501,x505),x502)
% 0.55/0.94 [51]~P1(x515,x514,x513)+~P1(x512,x511,x513)+P1(x511,f8(x512,x511,x513,x514,x515),x515)
% 0.55/0.94 [47]~P2(x475,x476,x471,x472)+P2(x471,x472,x473,x474)+~P2(x475,x476,x473,x474)
% 0.55/0.94 [52]~P1(x524,x522,x523)+~P1(x521,x522,x525)+E(x521,x522)+P1(x521,x523,f4(x521,x524,x522,x523,x525))
% 0.55/0.94 [53]~P1(x533,x532,x534)+~P1(x531,x532,x535)+E(x531,x532)+P1(x531,x533,f5(x531,x533,x532,x534,x535))
% 0.55/0.94 [54]~P1(x543,x542,x544)+~P1(x541,x542,x545)+E(x541,x542)+P1(f5(x541,x543,x542,x544,x545),x545,f4(x541,x543,x542,x544,x545))
% 0.55/0.94 [55]~P1(x553,x554,x555)+~P1(x552,x553,x555)+~P2(x552,x555,x552,x556)+~P2(x552,x553,x552,x551)+P1(x551,f6(x552,x553,x551,x554,x555,x556),x556)
% 0.55/0.94 [56]~P1(x563,x562,x565)+~P1(x561,x563,x565)+~P2(x561,x565,x561,x566)+~P2(x561,x563,x561,x564)+P2(x561,x562,x561,f6(x561,x563,x564,x562,x565,x566))
% 0.55/0.94 [48]P1(x485,x483,x484)+P1(x484,x485,x483)+~P2(x483,x481,x483,x482)+~P2(x485,x481,x485,x482)+~P2(x484,x481,x484,x482)+E(x481,x482)+P1(x483,x484,x485)
% 0.55/0.94 [49]~P1(x491,x492,x493)+~P2(x492,x494,x498,x496)+~P2(x492,x493,x498,x495)+~P2(x491,x494,x497,x496)+~P2(x491,x492,x497,x498)+E(x491,x492)+P2(x493,x494,x495,x496)+~P1(x497,x498,x495)
% 0.55/0.94 %EqnAxiom
% 0.55/0.94 [1]E(x11,x11)
% 0.55/0.94 [2]E(x22,x21)+~E(x21,x22)
% 0.55/0.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.55/0.94 [4]~E(x41,x42)+E(f3(x41,x43,x44,x45),f3(x42,x43,x44,x45))
% 0.55/0.94 [5]~E(x51,x52)+E(f3(x53,x51,x54,x55),f3(x53,x52,x54,x55))
% 0.55/0.94 [6]~E(x61,x62)+E(f3(x63,x64,x61,x65),f3(x63,x64,x62,x65))
% 0.55/0.94 [7]~E(x71,x72)+E(f3(x73,x74,x75,x71),f3(x73,x74,x75,x72))
% 0.55/0.94 [8]~E(x81,x82)+E(f6(x81,x83,x84,x85,x86,x87),f6(x82,x83,x84,x85,x86,x87))
% 0.55/0.94 [9]~E(x91,x92)+E(f6(x93,x91,x94,x95,x96,x97),f6(x93,x92,x94,x95,x96,x97))
% 0.55/0.94 [10]~E(x101,x102)+E(f6(x103,x104,x101,x105,x106,x107),f6(x103,x104,x102,x105,x106,x107))
% 0.55/0.94 [11]~E(x111,x112)+E(f6(x113,x114,x115,x111,x116,x117),f6(x113,x114,x115,x112,x116,x117))
% 0.55/0.94 [12]~E(x121,x122)+E(f6(x123,x124,x125,x126,x121,x127),f6(x123,x124,x125,x126,x122,x127))
% 0.55/0.94 [13]~E(x131,x132)+E(f6(x133,x134,x135,x136,x137,x131),f6(x133,x134,x135,x136,x137,x132))
% 0.55/0.94 [14]~E(x141,x142)+E(f8(x141,x143,x144,x145,x146),f8(x142,x143,x144,x145,x146))
% 0.55/0.94 [15]~E(x151,x152)+E(f8(x153,x151,x154,x155,x156),f8(x153,x152,x154,x155,x156))
% 0.55/0.94 [16]~E(x161,x162)+E(f8(x163,x164,x161,x165,x166),f8(x163,x164,x162,x165,x166))
% 0.55/0.94 [17]~E(x171,x172)+E(f8(x173,x174,x175,x171,x176),f8(x173,x174,x175,x172,x176))
% 0.55/0.94 [18]~E(x181,x182)+E(f8(x183,x184,x185,x186,x181),f8(x183,x184,x185,x186,x182))
% 0.55/0.94 [19]~E(x191,x192)+E(f4(x191,x193,x194,x195,x196),f4(x192,x193,x194,x195,x196))
% 0.55/0.94 [20]~E(x201,x202)+E(f4(x203,x201,x204,x205,x206),f4(x203,x202,x204,x205,x206))
% 0.55/0.94 [21]~E(x211,x212)+E(f4(x213,x214,x211,x215,x216),f4(x213,x214,x212,x215,x216))
% 0.55/0.94 [22]~E(x221,x222)+E(f4(x223,x224,x225,x221,x226),f4(x223,x224,x225,x222,x226))
% 0.55/0.94 [23]~E(x231,x232)+E(f4(x233,x234,x235,x236,x231),f4(x233,x234,x235,x236,x232))
% 0.55/0.94 [24]~E(x241,x242)+E(f5(x241,x243,x244,x245,x246),f5(x242,x243,x244,x245,x246))
% 0.55/0.94 [25]~E(x251,x252)+E(f5(x253,x251,x254,x255,x256),f5(x253,x252,x254,x255,x256))
% 0.55/0.94 [26]~E(x261,x262)+E(f5(x263,x264,x261,x265,x266),f5(x263,x264,x262,x265,x266))
% 0.55/0.94 [27]~E(x271,x272)+E(f5(x273,x274,x275,x271,x276),f5(x273,x274,x275,x272,x276))
% 0.55/0.94 [28]~E(x281,x282)+E(f5(x283,x284,x285,x286,x281),f5(x283,x284,x285,x286,x282))
% 0.55/0.94 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 0.55/0.94 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 0.55/0.94 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 0.55/0.94 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 0.55/0.94 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 0.55/0.94 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 0.55/0.94 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 0.55/0.94
% 0.55/0.94 %-------------------------------------------
% 0.57/0.94 cnf(57,plain,
% 0.57/0.94 (E(a2,a1)),
% 0.57/0.94 inference(scs_inference,[],[36,2])).
% 0.57/0.94 cnf(58,plain,
% 0.57/0.94 (P1(a2,x581,f3(a1,x581,x582,x583))),
% 0.57/0.94 inference(scs_inference,[],[39,36,2,29])).
% 0.57/0.94 cnf(59,plain,
% 0.57/0.94 (P1(x591,x592,f3(x591,x592,x593,x594))),
% 0.57/0.94 inference(rename_variables,[],[39])).
% 0.57/0.94 cnf(60,plain,
% 0.57/0.94 (P1(x601,a2,f3(x601,a1,x602,x603))),
% 0.57/0.94 inference(scs_inference,[],[39,59,36,2,29,30])).
% 0.57/0.94 cnf(61,plain,
% 0.57/0.94 (P1(x611,x612,f3(x611,x612,x613,x614))),
% 0.57/0.94 inference(rename_variables,[],[39])).
% 0.57/0.94 cnf(62,plain,
% 0.57/0.94 (P2(x621,x622,x621,x622)),
% 0.57/0.94 inference(scs_inference,[],[38,39,59,36,2,29,30,47])).
% 0.57/0.94 cnf(66,plain,
% 0.57/0.94 (P2(a2,x661,x661,a1)),
% 0.57/0.94 inference(scs_inference,[],[44,38,39,59,61,36,2,29,30,47,31,32])).
% 0.57/0.94 cnf(67,plain,
% 0.57/0.94 (P2(x671,x672,x672,x671)),
% 0.57/0.94 inference(rename_variables,[],[38])).
% 0.57/0.94 cnf(68,plain,
% 0.57/0.94 (P2(x681,a2,a1,x681)),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,39,59,61,36,2,29,30,47,31,32,33])).
% 0.57/0.94 cnf(69,plain,
% 0.57/0.94 (P2(x691,x692,x692,x691)),
% 0.57/0.94 inference(rename_variables,[],[38])).
% 0.57/0.94 cnf(70,plain,
% 0.57/0.94 (P2(x701,a1,a2,x701)),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,69,39,59,61,36,2,29,30,47,31,32,33,34])).
% 0.57/0.94 cnf(71,plain,
% 0.57/0.94 (P2(x711,x712,x712,x711)),
% 0.57/0.94 inference(rename_variables,[],[38])).
% 0.57/0.94 cnf(72,plain,
% 0.57/0.94 (P2(a1,x721,x721,a2)),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,69,71,39,59,61,36,2,29,30,47,31,32,33,34,35])).
% 0.57/0.94 cnf(74,plain,
% 0.57/0.94 (~P1(f3(a12,a11,x741,x742),a1,f3(a12,a11,x741,x742))),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,69,71,39,59,61,36,2,29,30,47,31,32,33,34,35,45])).
% 0.57/0.94 cnf(76,plain,
% 0.57/0.94 (~P2(f3(a12,a11,x761,x762),a1,x763,x763)),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,69,71,39,59,61,36,2,29,30,47,31,32,33,34,35,45,46])).
% 0.57/0.94 cnf(78,plain,
% 0.57/0.94 (~E(f3(a12,a11,x781,x782),a2)),
% 0.57/0.94 inference(scs_inference,[],[44,38,67,69,71,39,59,61,36,2,29,30,47,31,32,33,34,35,45,46,3])).
% 0.57/0.94 cnf(85,plain,
% 0.57/0.94 (~P2(f3(a12,a11,x851,x852),a2,x853,x853)),
% 0.57/0.94 inference(scs_inference,[],[78,45,46])).
% 0.57/0.94 cnf(87,plain,
% 0.57/0.94 (~E(a1,f3(a12,a11,x871,x872))),
% 0.57/0.94 inference(scs_inference,[],[62,76,78,45,46,35])).
% 0.57/0.94 cnf(89,plain,
% 0.57/0.94 (~P2(f3(a12,a11,x891,x892),a1,x893,x893)),
% 0.57/0.94 inference(rename_variables,[],[76])).
% 0.57/0.94 cnf(90,plain,
% 0.57/0.94 (P1(a1,a2,f3(a2,a1,x901,x902))),
% 0.57/0.94 inference(scs_inference,[],[60,62,76,78,57,45,46,35,29])).
% 0.57/0.94 cnf(91,plain,
% 0.57/0.94 (P1(x911,a2,f3(x911,a1,x912,x913))),
% 0.57/0.94 inference(rename_variables,[],[60])).
% 0.57/0.94 cnf(92,plain,
% 0.57/0.94 (~E(f3(f3(a12,a11,x921,x922),a1,x923,x924),f3(a12,a11,x921,x922))),
% 0.57/0.94 inference(scs_inference,[],[60,91,62,76,78,57,45,46,35,29,31])).
% 0.57/0.94 cnf(94,plain,
% 0.57/0.94 (P2(x941,f3(x942,x941,a2,x943),a1,x943)),
% 0.57/0.94 inference(scs_inference,[],[60,91,62,40,76,78,57,45,46,35,29,31,34])).
% 0.57/0.94 cnf(95,plain,
% 0.57/0.94 (P2(x951,f3(x952,x951,x953,x954),x953,x954)),
% 0.57/0.94 inference(rename_variables,[],[40])).
% 0.57/0.94 cnf(96,plain,
% 0.57/0.94 (P2(a1,f3(x961,a2,x962,x963),x962,x963)),
% 0.57/0.94 inference(scs_inference,[],[60,91,62,40,95,76,78,57,45,46,35,29,31,34,32])).
% 0.57/0.94 cnf(97,plain,
% 0.57/0.94 (P2(x971,f3(x972,x971,x973,x974),x973,x974)),
% 0.57/0.94 inference(rename_variables,[],[40])).
% 0.57/0.94 cnf(98,plain,
% 0.57/0.94 (~E(f3(x981,f3(a12,a11,x982,x983),x984,x984),a1)),
% 0.57/0.94 inference(scs_inference,[],[60,91,62,40,95,97,76,89,78,57,45,46,35,29,31,34,32,33])).
% 0.57/0.94 cnf(100,plain,
% 0.57/0.95 (P1(a2,a1,f3(a1,a2,x1001,x1002))),
% 0.57/0.95 inference(scs_inference,[],[58,60,91,62,40,95,97,76,89,78,57,45,46,35,29,31,34,32,33,30])).
% 0.57/0.95 cnf(107,plain,
% 0.57/0.95 (~P2(f3(f3(a12,a11,x1071,x1072),a1,x1073,x1074),f3(a12,a11,x1071,x1072),x1075,x1075)),
% 0.57/0.95 inference(scs_inference,[],[92,46])).
% 0.57/0.95 cnf(109,plain,
% 0.57/0.95 (~P1(a1,f3(a12,a11,x1091,x1092),a1)),
% 0.57/0.95 inference(scs_inference,[],[92,87,46,45])).
% 0.57/0.95 cnf(111,plain,
% 0.57/0.95 (P2(a1,x1111,f3(x1112,a2,a2,x1111),a1)),
% 0.57/0.95 inference(scs_inference,[],[92,94,66,87,46,45,47])).
% 0.57/0.95 cnf(113,plain,
% 0.57/0.95 (P2(x1131,f3(x1132,x1131,a2,x1133),a1,x1133)),
% 0.57/0.95 inference(rename_variables,[],[94])).
% 0.57/0.95 cnf(115,plain,
% 0.57/0.95 (~E(f3(x1151,f3(a12,a11,x1152,x1153),x1154,x1154),a2)),
% 0.57/0.95 inference(scs_inference,[],[92,94,66,98,87,57,46,45,47,3])).
% 0.57/0.95 cnf(116,plain,
% 0.57/0.95 (P1(a1,a1,f3(a1,a2,x1161,x1162))),
% 0.57/0.95 inference(scs_inference,[],[100,92,94,66,98,87,57,46,45,47,3,29])).
% 0.57/0.95 cnf(117,plain,
% 0.57/0.95 (P1(a2,a11,a2)),
% 0.57/0.95 inference(scs_inference,[],[100,92,94,66,98,87,37,57,36,46,45,47,3,29,31])).
% 0.57/0.95 cnf(119,plain,
% 0.57/0.95 (P2(x1191,f3(x1192,x1191,a2,a2),a1,a1)),
% 0.57/0.95 inference(scs_inference,[],[90,100,92,94,113,66,98,87,37,57,36,46,45,47,3,29,31,30,35])).
% 0.57/0.95 cnf(120,plain,
% 0.57/0.95 (P2(x1201,f3(x1202,x1201,a2,x1203),a1,x1203)),
% 0.57/0.95 inference(rename_variables,[],[94])).
% 0.57/0.95 cnf(121,plain,
% 0.57/0.95 (P2(a1,f3(x1211,a2,a2,x1212),a1,x1212)),
% 0.57/0.95 inference(scs_inference,[],[90,100,92,94,113,96,66,98,87,37,57,36,46,45,47,3,29,31,30,35,34])).
% 0.57/0.95 cnf(123,plain,
% 0.57/0.95 (~E(f3(x1231,f3(a12,a11,x1232,x1233),a2,a1),a2)),
% 0.57/0.95 inference(scs_inference,[],[90,100,92,94,113,120,96,85,66,98,87,37,57,36,46,45,47,3,29,31,30,35,34,33])).
% 0.57/0.95 cnf(124,plain,
% 0.57/0.95 (P2(x1241,f3(x1242,x1241,a2,x1243),a1,x1243)),
% 0.57/0.95 inference(rename_variables,[],[94])).
% 0.57/0.95 cnf(126,plain,
% 0.57/0.95 (~E(a11,f3(f3(a12,a11,a2,a1),a1,x1261,x1262))),
% 0.57/0.95 inference(scs_inference,[],[90,100,92,94,113,120,124,96,85,66,98,87,37,57,36,46,45,47,3,29,31,30,35,34,33,32])).
% 0.57/0.95 cnf(140,plain,
% 0.57/0.95 (P2(a1,a1,a2,a2)),
% 0.57/0.95 inference(scs_inference,[],[68,72,115,126,45,46,47])).
% 0.57/0.95 cnf(146,plain,
% 0.57/0.95 (~E(a2,f3(a12,a11,x1461,x1462))),
% 0.57/0.95 inference(scs_inference,[],[60,68,70,72,115,126,76,36,45,46,47,29,34])).
% 0.57/0.95 cnf(149,plain,
% 0.57/0.95 (P2(a1,x1491,f3(x1492,a2,a2,x1491),a2)),
% 0.57/0.95 inference(scs_inference,[],[60,68,70,72,115,111,126,76,36,45,46,47,29,34,35])).
% 0.57/0.95 cnf(151,plain,
% 0.57/0.95 (P2(a1,x1511,f3(x1512,a2,a2,x1511),a1)),
% 0.57/0.95 inference(rename_variables,[],[111])).
% 0.57/0.95 cnf(152,plain,
% 0.57/0.95 (P2(a2,x1521,f3(x1522,a2,a2,x1521),a1)),
% 0.57/0.95 inference(scs_inference,[],[60,68,70,72,115,111,151,126,76,36,45,46,47,29,34,35,33,32])).
% 0.57/0.95 cnf(154,plain,
% 0.57/0.95 (P1(a2,x1541,a2)+~E(a11,x1541)),
% 0.57/0.95 inference(scs_inference,[],[116,60,68,70,72,115,111,151,126,117,76,36,45,46,47,29,34,35,33,32,31,30])).
% 0.57/0.95 cnf(160,plain,
% 0.57/0.95 (~P2(a2,f3(a12,a11,x1601,x1602),x1603,x1603)),
% 0.57/0.95 inference(scs_inference,[],[146,46])).
% 0.57/0.95 cnf(165,plain,
% 0.57/0.95 (P2(a1,a1,f3(x1651,a2,a2,f3(x1652,a1,a2,a2)),a2)),
% 0.57/0.95 inference(scs_inference,[],[36,119,149,146,123,46,45,3,47])).
% 0.57/0.95 cnf(166,plain,
% 0.57/0.95 (P2(a1,x1661,f3(x1662,a2,a2,x1661),a2)),
% 0.57/0.95 inference(rename_variables,[],[149])).
% 0.57/0.95 cnf(167,plain,
% 0.57/0.95 (P2(x1671,f3(x1672,x1671,a2,a2),a1,a1)),
% 0.57/0.95 inference(rename_variables,[],[119])).
% 0.57/0.95 cnf(169,plain,
% 0.57/0.95 (P1(a1,x1691,f3(a2,x1691,x1692,x1693))),
% 0.57/0.95 inference(scs_inference,[],[57,36,39,119,149,146,123,46,45,3,47,29])).
% 0.57/0.95 cnf(170,plain,
% 0.57/0.95 (P1(x1701,x1702,f3(x1701,x1702,x1703,x1704))),
% 0.57/0.95 inference(rename_variables,[],[39])).
% 0.57/0.95 cnf(171,plain,
% 0.57/0.95 (~E(f3(a1,f3(a12,a11,x1711,x1712),x1713,x1714),a2)),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,119,149,146,123,46,45,3,47,29,31])).
% 0.57/0.95 cnf(173,plain,
% 0.57/0.95 (P2(x1731,f3(x1732,x1731,a2,a2),a2,a1)),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,119,167,149,146,123,46,45,3,47,29,31,34])).
% 0.57/0.95 cnf(176,plain,
% 0.57/0.95 (P1(x1761,a1,f3(x1761,a2,x1762,x1763))),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,170,119,167,121,149,146,123,46,45,3,47,29,31,34,35,30])).
% 0.57/0.95 cnf(178,plain,
% 0.57/0.95 (~E(a11,f3(f3(a12,a11,a2,a2),a1,x1781,x1782))),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,170,107,119,167,121,149,146,123,46,45,3,47,29,31,34,35,30,32])).
% 0.57/0.95 cnf(181,plain,
% 0.57/0.95 (P2(a1,a1,f3(x1811,a2,a2,a2),a2)),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,170,107,119,167,121,149,166,146,123,46,45,3,47,29,31,34,35,30,32,33])).
% 0.57/0.95 cnf(183,plain,
% 0.57/0.95 (~E(a11,f3(a12,a11,x1831,x1832))),
% 0.57/0.95 inference(scs_inference,[],[58,57,36,39,170,107,119,167,121,149,166,146,123,46,45,3,47,29,31,34,35,30,32,33,154])).
% 0.57/0.95 cnf(194,plain,
% 0.57/0.95 (P2(f3(x1941,a2,a2,f3(x1942,a2,a2,a2)),a1,a2,a1)),
% 0.57/0.95 inference(scs_inference,[],[152,173,171,178,45,46,47])).
% 0.57/0.95 cnf(196,plain,
% 0.57/0.95 (P2(a2,x1961,f3(x1962,a2,a2,x1961),a1)),
% 0.57/0.95 inference(rename_variables,[],[152])).
% 0.57/0.95 cnf(198,plain,
% 0.57/0.95 (~E(f3(a1,f3(a12,a11,x1981,x1982),x1983,x1984),a1)),
% 0.57/0.95 inference(scs_inference,[],[36,152,173,171,178,45,46,47,3])).
% 0.57/0.95 cnf(201,plain,
% 0.57/0.95 (~E(f3(a2,f3(a12,a11,x2011,x2012),x2013,x2014),a1)),
% 0.57/0.95 inference(scs_inference,[],[169,176,57,36,152,173,171,178,109,45,46,47,3,29,31])).
% 0.57/0.95 cnf(204,plain,
% 0.57/0.95 (P2(a2,x2041,f3(x2042,a2,a2,x2041),a1)),
% 0.57/0.95 inference(rename_variables,[],[152])).
% 0.57/0.95 cnf(205,plain,
% 0.57/0.95 (~P2(a2,f3(a12,a11,x2051,x2052),x2053,x2053)),
% 0.57/0.95 inference(rename_variables,[],[160])).
% 0.57/0.95 cnf(206,plain,
% 0.57/0.95 (~E(a1,f3(x2061,a2,a2,f3(a12,a11,x2062,x2063)))),
% 0.57/0.95 inference(scs_inference,[],[169,176,57,36,160,205,152,196,204,173,171,178,109,45,46,47,3,29,31,34,35])).
% 0.57/0.95 cnf(222,plain,
% 0.57/0.95 (~P2(f3(a1,f3(a12,a11,x2221,x2222),x2223,x2224),a1,x2225,x2225)),
% 0.57/0.95 inference(scs_inference,[],[198,46])).
% 0.57/0.95 cnf(226,plain,
% 0.57/0.95 (P2(f3(x2261,a2,a2,f3(x2262,a1,a2,a2)),a2,a1,a1)),
% 0.57/0.95 inference(scs_inference,[],[198,183,165,62,46,45,47])).
% 0.57/0.95 cnf(229,plain,
% 0.57/0.95 (P1(a1,a11,a2)),
% 0.57/0.95 inference(scs_inference,[],[57,198,183,165,62,117,46,45,47,29])).
% 0.57/0.95 cnf(230,plain,
% 0.57/0.95 (~E(f3(f3(a12,a11,x2301,x2302),a2,x2303,x2304),f3(a12,a11,x2301,x2302))),
% 0.57/0.95 inference(scs_inference,[],[176,57,198,183,165,62,117,74,46,45,47,29,31])).
% 0.57/0.95 cnf(232,plain,
% 0.57/0.95 (P2(a2,a1,f3(x2321,a2,a2,f3(x2322,a1,a2,a2)),a2)),
% 0.57/0.95 inference(scs_inference,[],[176,36,57,198,183,165,62,117,74,46,45,47,29,31,32])).
% 0.57/0.95 cnf(233,plain,
% 0.57/0.95 (P2(a1,a1,f3(x2331,a2,a2,f3(x2332,a1,a2,a2)),a1)),
% 0.57/0.95 inference(scs_inference,[],[176,36,57,198,183,165,62,117,74,46,45,47,29,31,32,35])).
% 0.57/0.95 cnf(234,plain,
% 0.57/0.95 (P2(f3(x2341,a2,a2,f3(x2342,a2,a2,a2)),a1,a1,a1)),
% 0.57/0.95 inference(scs_inference,[],[176,36,57,198,183,165,194,62,117,74,46,45,47,29,31,32,35,34])).
% 0.57/0.95 cnf(235,plain,
% 0.57/0.95 (P2(a1,a2,f3(x2351,a2,a2,f3(x2352,a1,a2,a2)),a2)),
% 0.57/0.95 inference(scs_inference,[],[176,36,57,198,183,165,194,62,117,74,46,45,47,29,31,32,35,34,33])).
% 0.57/0.95 cnf(244,plain,
% 0.57/0.95 (~P1(a1,f3(x2441,a2,a2,f3(a12,a11,x2442,x2443)),a1)),
% 0.57/0.95 inference(scs_inference,[],[206,45])).
% 0.57/0.95 cnf(248,plain,
% 0.57/0.95 (~E(f3(a2,f3(a12,a11,x2481,x2482),x2483,x2484),a2)),
% 0.57/0.95 inference(scs_inference,[],[57,230,201,206,45,46,3])).
% 0.57/0.95 cnf(249,plain,
% 0.57/0.95 (P2(a1,a1,a1,f3(x2491,a2,a2,f3(x2492,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[57,230,201,206,226,68,45,46,3,47])).
% 0.57/0.95 cnf(252,plain,
% 0.57/0.95 (~E(a2,a12)),
% 0.57/0.95 inference(scs_inference,[],[44,57,37,230,201,206,226,68,45,46,3,47,29])).
% 0.57/0.95 cnf(253,plain,
% 0.57/0.95 (P1(a1,a11,a1)),
% 0.57/0.95 inference(scs_inference,[],[44,229,57,37,230,201,206,226,68,45,46,3,47,29,31])).
% 0.57/0.95 cnf(256,plain,
% 0.57/0.95 (P2(a2,a2,f3(x2561,a2,a2,f3(x2562,a1,a2,a2)),a2)),
% 0.57/0.95 inference(scs_inference,[],[44,229,36,57,37,230,201,206,226,232,233,68,45,46,3,47,29,31,32,34,33])).
% 0.57/0.95 cnf(257,plain,
% 0.57/0.95 (P2(f3(x2571,a2,a2,f3(x2572,a1,a2,a2)),a2,a1,a2)),
% 0.57/0.95 inference(scs_inference,[],[44,229,36,57,37,230,201,206,226,232,233,68,45,46,3,47,29,31,32,34,33,35])).
% 0.57/0.95 cnf(274,plain,
% 0.57/0.95 (~E(a1,a12)),
% 0.57/0.95 inference(scs_inference,[],[44,252,234,253,70,46,45,47,29])).
% 0.57/0.95 cnf(275,plain,
% 0.57/0.95 (~E(a11,f3(x2751,a2,a2,f3(a12,a11,x2752,x2753)))),
% 0.57/0.95 inference(scs_inference,[],[44,252,244,234,253,70,46,45,47,29,30])).
% 0.57/0.95 cnf(277,plain,
% 0.57/0.95 (P2(a1,a1,a2,f3(x2771,a2,a2,f3(x2772,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[44,252,36,244,234,249,253,70,46,45,47,29,30,33,34])).
% 0.57/0.95 cnf(278,plain,
% 0.57/0.95 (P2(a2,a1,a1,f3(x2781,a2,a2,f3(x2782,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[44,252,36,244,234,249,253,70,46,45,47,29,30,33,34,32])).
% 0.57/0.95 cnf(280,plain,
% 0.57/0.95 (~E(a11,a12)),
% 0.57/0.95 inference(scs_inference,[],[44,252,36,244,234,249,253,70,46,45,47,29,30,33,34,32,35,154])).
% 0.57/0.95 cnf(289,plain,
% 0.57/0.95 (~P1(a1,a12,a1)),
% 0.57/0.95 inference(scs_inference,[],[274,45])).
% 0.57/0.95 cnf(293,plain,
% 0.57/0.95 (P2(f3(x2931,a2,a2,f3(x2932,a1,a2,a2)),a2,a2,a2)),
% 0.57/0.95 inference(scs_inference,[],[274,235,72,45,46,47])).
% 0.57/0.95 cnf(308,plain,
% 0.57/0.95 (P2(a2,f3(x3081,a2,a2,f3(x3082,a1,a2,a2)),f3(x3083,a2,a2,a1),a2)),
% 0.57/0.95 inference(scs_inference,[],[280,277,149,46,45,47])).
% 0.57/0.95 cnf(311,plain,
% 0.57/0.95 (P2(f3(x3111,a2,a2,f3(x3112,a1,a2,a2)),a1,a1,a2)),
% 0.57/0.95 inference(scs_inference,[],[57,280,257,277,149,46,45,47,33])).
% 0.57/0.95 cnf(312,plain,
% 0.57/0.95 (~E(f3(a2,a12,x3121,x3122),a1)),
% 0.57/0.95 inference(scs_inference,[],[169,57,280,257,277,289,149,46,45,47,33,31])).
% 0.57/0.95 cnf(314,plain,
% 0.57/0.95 (P2(a2,a2,f3(x3141,a2,a2,f3(x3142,a1,a2,a2)),a1)),
% 0.57/0.95 inference(scs_inference,[],[169,57,280,256,257,277,289,149,46,45,47,33,31,35])).
% 0.57/0.95 cnf(322,plain,
% 0.57/0.95 (~P1(f3(a2,a12,x3221,x3222),a1,f3(a2,a12,x3221,x3222))),
% 0.57/0.95 inference(scs_inference,[],[312,45])).
% 0.57/0.95 cnf(326,plain,
% 0.57/0.95 (~E(f3(a2,a12,x3261,x3262),a2)),
% 0.57/0.95 inference(scs_inference,[],[57,248,312,45,46,3])).
% 0.57/0.95 cnf(327,plain,
% 0.57/0.95 (P2(f3(x3271,a2,a2,a1),a2,a2,f3(x3272,a2,a2,f3(x3273,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[57,248,312,308,62,45,46,3,47])).
% 0.57/0.95 cnf(330,plain,
% 0.57/0.95 (P2(a2,a2,a1,f3(x3301,a2,a2,f3(x3302,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[57,36,248,312,308,278,62,45,46,3,47,33])).
% 0.57/0.95 cnf(332,plain,
% 0.57/0.95 (P2(a1,f3(x3321,a2,a2,f3(x3322,a1,a2,a2)),f3(x3323,a2,a2,a1),a2)),
% 0.57/0.95 inference(scs_inference,[],[57,36,248,312,308,278,62,45,46,3,47,33,35,32])).
% 0.57/0.95 cnf(333,plain,
% 0.57/0.95 (P2(f3(x3331,a2,a2,f3(x3332,a1,a2,a2)),a1,a2,a2)),
% 0.57/0.95 inference(scs_inference,[],[57,36,248,312,308,278,311,62,45,46,3,47,33,35,32,34])).
% 0.57/0.95 cnf(338,plain,
% 0.57/0.95 (~P2(f3(a2,a12,x3381,x3382),a2,x3383,x3383)),
% 0.57/0.95 inference(scs_inference,[],[326,46])).
% 0.57/0.95 cnf(340,plain,
% 0.57/0.95 (~P1(f3(a2,a12,x3401,x3402),a2,f3(a2,a12,x3401,x3402))),
% 0.57/0.95 inference(scs_inference,[],[326,46,45])).
% 0.57/0.95 cnf(345,plain,
% 0.57/0.95 (P2(f3(x3451,a2,a2,a1),a1,a2,f3(x3452,a2,a2,f3(x3453,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[57,326,332,327,121,46,45,47,33])).
% 0.57/0.95 cnf(346,plain,
% 0.57/0.95 (~E(f3(f3(a2,a12,x3461,x3462),a2,x3463,x3464),f3(a2,a12,x3461,x3462))),
% 0.57/0.95 inference(scs_inference,[],[176,57,322,326,332,327,121,46,45,47,33,31])).
% 0.57/0.95 cnf(348,plain,
% 0.57/0.95 (P2(a1,f3(x3481,a2,a2,f3(x3482,a1,a2,a2)),f3(x3483,a2,a2,a1),a1)),
% 0.57/0.95 inference(scs_inference,[],[176,57,322,326,332,327,121,46,45,47,33,31,35])).
% 0.57/0.95 cnf(349,plain,
% 0.57/0.95 (P2(f3(x3491,a2,a2,a1),a2,a1,f3(x3492,a2,a2,f3(x3493,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[176,57,322,326,332,327,121,46,45,47,33,31,35,34])).
% 0.57/0.95 cnf(362,plain,
% 0.57/0.95 (P2(f3(x3621,a2,a2,f3(x3622,a1,a2,a2)),a1,f3(x3623,a2,a2,a2),a1)),
% 0.57/0.95 inference(scs_inference,[],[346,275,314,152,45,46,47])).
% 0.57/0.95 cnf(366,plain,
% 0.57/0.95 (~E(f3(f3(a2,a12,x3661,x3662),a1,x3663,x3664),f3(a2,a12,x3661,x3662))),
% 0.57/0.95 inference(scs_inference,[],[60,57,346,340,275,349,314,152,45,46,47,33,31])).
% 0.57/0.95 cnf(369,plain,
% 0.57/0.95 (~E(f3(x3691,a2,a2,f3(x3692,a1,a2,a2)),f3(a2,a12,x3693,x3694))),
% 0.57/0.95 inference(scs_inference,[],[60,57,346,338,340,275,349,293,314,181,152,45,46,47,33,31,35,32])).
% 0.57/0.95 cnf(387,plain,
% 0.57/0.95 (P2(a2,a2,a2,f3(x3871,a2,a2,f3(x3872,a1,a2,a2)))),
% 0.57/0.95 inference(scs_inference,[],[36,366,348,362,330,96,46,47,33,35,34])).
% 0.57/0.95 cnf(388,plain,
% 0.57/0.95 (~E(a1,f3(a1,f3(a12,a11,x3881,x3882),x3883,x3884))),
% 0.57/0.95 inference(scs_inference,[],[36,366,348,362,330,140,222,96,46,47,33,35,34,32])).
% 0.57/0.95 cnf(397,plain,
% 0.57/0.95 (~P2(f3(x3971,a2,a2,f3(x3972,a1,a2,a2)),f3(a2,a12,x3973,x3974),x3975,x3975)),
% 0.57/0.95 inference(scs_inference,[],[369,46])).
% 0.57/0.95 cnf(399,plain,
% 0.57/0.95 (P2(a2,f3(x3991,a2,a2,f3(x3992,a1,a2,a2)),a2,a1)),
% 0.57/0.95 inference(scs_inference,[],[369,387,66,46,47])).
% 0.57/0.95 cnf(413,plain,
% 0.57/0.95 (E(f3(a1,x4131,x4132,x4133),f3(a2,x4131,x4132,x4133))),
% 0.57/0.95 inference(scs_inference,[],[57,4,2])).
% 0.57/0.95 cnf(417,plain,
% 0.57/0.95 (~E(f3(x4171,a2,a2,f3(x4172,a1,a2,a2)),f3(a1,a12,x4173,x4174))),
% 0.57/0.95 inference(scs_inference,[],[369,413,388,2,46,3])).
% 0.57/0.95 cnf(419,plain,
% 0.57/0.95 (P2(a2,f3(x4191,a2,a2,f3(x4192,a1,a2,a2)),a2,f3(x4193,a2,a2,a1))),
% 0.57/0.95 inference(scs_inference,[],[369,413,388,345,70,2,46,3,47])).
% 0.57/0.95 cnf(425,plain,
% 0.57/0.95 (P2(a2,f3(x4251,a2,a2,f3(x4252,a1,a2,a2)),a2,a2)),
% 0.57/0.95 inference(scs_inference,[],[36,369,413,397,388,345,333,399,70,2,46,3,47,33,35])).
% 0.57/0.95 cnf(426,plain,
% 0.57/0.95 (P2(a2,f3(x4261,a2,a2,f3(x4262,a1,a2,a2)),a1,a1)),
% 0.57/0.95 inference(scs_inference,[],[57,36,369,413,397,388,345,333,399,70,2,46,3,47,33,35,34])).
% 0.57/0.95 cnf(427,plain,
% 0.57/0.95 (P2(a1,f3(x4271,a2,a2,f3(x4272,a1,a2,a2)),a2,a1)),
% 0.57/0.95 inference(scs_inference,[],[57,36,369,413,397,388,345,333,399,70,2,46,3,47,33,35,34,32])).
% 0.57/0.95 cnf(428,plain,
% 0.57/0.95 (~P1(a1,f3(a2,a12,x4281,x4282),a1)),
% 0.57/0.95 inference(scs_inference,[],[57,36,369,413,397,388,345,333,399,70,2,46,3,47,33,35,34,32,45])).
% 0.57/0.95 cnf(442,plain,
% 0.57/0.95 (~E(f3(x4421,a2,a2,f3(x4422,a1,a2,a2)),f3(a12,a11,x4423,x4424))),
% 0.57/0.95 inference(scs_inference,[],[169,253,417,428,425,427,160,121,46,47,30,31,33])).
% 0.57/0.95 cnf(447,plain,
% 0.57/0.95 (~E(a2,a11)),
% 0.57/0.95 inference(scs_inference,[],[169,36,57,253,417,419,428,425,426,427,160,121,46,47,30,31,33,35,34,32,5])).
% 0.57/0.95 cnf(456,plain,
% 0.57/0.95 ($false),
% 0.57/0.95 inference(scs_inference,[],[117,442,447,46,45]),
% 0.57/0.95 ['proof']).
% 0.57/0.95 % SZS output end Proof
% 0.57/0.95 % Total time :0.300000s
%------------------------------------------------------------------------------