%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO039-3 : 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 : n027.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 1.53s 1.64s
% Output : CNFRefutation 1.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : GEO039-3 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n027.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Fri Jun 21 08:25:54 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.52 start to proof:theBenchmark
% 1.53/1.63 %-------------------------------------------
% 1.53/1.63 % File :CSE---1.7
% 1.53/1.63 % Problem :theBenchmark
% 1.53/1.63 % Transform :cnf
% 1.53/1.63 % Format :tptp:raw
% 1.53/1.63 % Command :java -jar mcs_scs.jar %d %s
% 1.53/1.63
% 1.53/1.63 % Result :Theorem 1.070000s
% 1.53/1.63 % Output :CNFRefutation 1.070000s
% 1.53/1.63 %-------------------------------------------
% 1.53/1.63 %--------------------------------------------------------------------------
% 1.53/1.63 % File : GEO039-3 : TPTP v8.2.0. Released v1.0.0.
% 1.53/1.63 % Domain : Geometry
% 1.53/1.63 % Problem : Corollary the identity axiom for betweenness
% 1.53/1.64 % Version : [Qua89] axioms : Augmented.
% 1.53/1.64 % English :
% 1.53/1.64
% 1.53/1.64 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 1.53/1.64 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 1.53/1.64 % Source : [Qua89]
% 1.53/1.64 % Names : B1 [Qua89]
% 1.53/1.64
% 1.53/1.64 % Status : Unsatisfiable
% 1.53/1.64 % Rating : 0.10 v8.2.0, 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.06 v5.0.0, 0.00 v4.0.1, 0.09 v3.7.0, 0.00 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.17 v2.6.0, 0.10 v2.5.0, 0.08 v2.4.0, 0.11 v2.2.1, 0.00 v2.2.0, 0.11 v2.1.0, 0.11 v2.0.0
% 1.53/1.64 % Syntax : Number of clauses : 47 ( 19 unt; 9 nHn; 32 RR)
% 1.53/1.64 % Number of literals : 110 ( 25 equ; 56 neg)
% 1.53/1.64 % Maximal clause size : 8 ( 2 avg)
% 1.53/1.64 % Maximal term depth : 3 ( 1 avg)
% 1.53/1.64 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 1.53/1.64 % Number of functors : 13 ( 13 usr; 7 con; 0-6 aty)
% 1.53/1.64 % Number of variables : 155 ( 7 sgn)
% 1.53/1.64 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.53/1.64
% 1.53/1.64 % Comments :
% 1.53/1.64 %--------------------------------------------------------------------------
% 1.53/1.64 %----Include Tarski geometry axioms
% 1.53/1.64 include('Axioms/GEO002-0.ax').
% 1.53/1.64 %----Include definition of reflection
% 1.53/1.64 include('Axioms/GEO002-2.ax').
% 1.53/1.64 %--------------------------------------------------------------------------
% 1.53/1.64 cnf(d1,axiom,
% 1.53/1.64 equidistant(U,V,U,V) ).
% 1.53/1.64
% 1.53/1.64 cnf(d2,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(W,X,U,V) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d3,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(V,U,W,X) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d4_1,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(U,V,X,W) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d4_2,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(V,U,X,W) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d4_3,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(W,X,V,U) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d4_4,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(X,W,U,V) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d4_5,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | equidistant(X,W,V,U) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d5,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,W,X)
% 1.53/1.64 | ~ equidistant(W,X,Y,Z)
% 1.53/1.64 | equidistant(U,V,Y,Z) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(e1,axiom,
% 1.53/1.64 V = extension(U,V,W,W) ).
% 1.53/1.64
% 1.53/1.64 cnf(b0,axiom,
% 1.53/1.64 ( Y != extension(U,V,W,X)
% 1.53/1.64 | between(U,V,Y) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(r2_1,axiom,
% 1.53/1.64 between(U,V,reflection(U,V)) ).
% 1.53/1.64
% 1.53/1.64 cnf(r2_2,axiom,
% 1.53/1.64 equidistant(V,reflection(U,V),U,V) ).
% 1.53/1.64
% 1.53/1.64 cnf(r3_1,axiom,
% 1.53/1.64 ( U != V
% 1.53/1.64 | V = reflection(U,V) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(r3_2,axiom,
% 1.53/1.64 U = reflection(U,U) ).
% 1.53/1.64
% 1.53/1.64 cnf(r4,axiom,
% 1.53/1.64 ( V != reflection(U,V)
% 1.53/1.64 | U = V ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d7,axiom,
% 1.53/1.64 equidistant(U,U,V,V) ).
% 1.53/1.64
% 1.53/1.64 cnf(d8,axiom,
% 1.53/1.64 ( ~ equidistant(U,V,U1,V1)
% 1.53/1.64 | ~ equidistant(V,W,V1,W1)
% 1.53/1.64 | ~ between(U,V,W)
% 1.53/1.64 | ~ between(U1,V1,W1)
% 1.53/1.64 | equidistant(U,W,U1,W1) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d9,axiom,
% 1.53/1.64 ( ~ between(U,V,W)
% 1.53/1.64 | ~ between(U,V,X)
% 1.53/1.64 | ~ equidistant(V,W,V,X)
% 1.53/1.64 | U = V
% 1.53/1.64 | W = X ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d10_1,axiom,
% 1.53/1.64 ( ~ between(U,V,W)
% 1.53/1.64 | U = V
% 1.53/1.64 | W = extension(U,V,V,W) ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d10_2,axiom,
% 1.53/1.64 ( ~ equidistant(W,X,Y,Z)
% 1.53/1.64 | extension(U,V,W,X) = extension(U,V,Y,Z)
% 1.53/1.64 | U = V ) ).
% 1.53/1.64
% 1.53/1.64 cnf(d10_3,axiom,
% 1.53/1.64 ( extension(U,V,U,V) = extension(U,V,V,U)
% 1.53/1.64 | U = V ) ).
% 1.53/1.64
% 1.53/1.64 cnf(r5,axiom,
% 1.53/1.64 equidistant(V,U,V,reflection(reflection(U,V),V)) ).
% 1.53/1.64
% 1.53/1.64 cnf(r6,axiom,
% 1.53/1.64 U = reflection(reflection(U,V),V) ).
% 1.53/1.64
% 1.53/1.64 cnf(t3,axiom,
% 1.53/1.64 between(U,V,V) ).
% 1.53/1.64
% 1.53/1.64 cnf(w_between_u_and_x,hypothesis,
% 1.53/1.64 between(u,w,x) ).
% 1.53/1.64
% 1.53/1.64 cnf(u_is_x,hypothesis,
% 1.53/1.64 u = x ).
% 1.53/1.64
% 1.53/1.64 cnf(prove_corollary,negated_conjecture,
% 1.53/1.64 ~ between(v,w,x) ).
% 1.53/1.64
% 1.53/1.64 %--------------------------------------------------------------------------
% 1.53/1.64 %-------------------------------------------
% 1.53/1.64 % Proof found
% 1.53/1.64 % SZS status Theorem for theBenchmark
% 1.53/1.64 % SZS output start Proof
% 1.53/1.64 %ClaNum:81(EqnAxiom:35)
% 1.53/1.64 %VarNum:407(SingletonVarNum:148)
% 1.53/1.64 %MaxLitNum:8
% 1.53/1.64 %MaxfuncDepth:2
% 1.53/1.64 %SharedTerms:13
% 1.53/1.64 %goalClause: 53
% 1.53/1.64 %singleGoalClaCount:1
% 1.53/1.64 [36]E(a1,a2)
% 1.53/1.64 [37]P1(a2,a11,a1)
% 1.53/1.64 [50]~P1(a7,a9,a10)
% 1.53/1.64 [51]~P1(a9,a10,a7)
% 1.53/1.64 [52]~P1(a10,a7,a9)
% 1.53/1.64 [53]~P1(a12,a11,a1)
% 1.53/1.64 [38]P1(x381,x382,x382)
% 1.53/1.64 [39]P2(x391,x392,x392,x391)
% 1.53/1.64 [40]P2(x401,x402,x401,x402)
% 1.53/1.64 [41]P2(x411,x411,x412,x412)
% 1.53/1.64 [48]E(f3(f3(x481,x482,x481,x482),x482,f3(x481,x482,x481,x482),x482),x481)
% 1.53/1.64 [49]P2(x491,x492,x491,f3(f3(x492,x491,x492,x491),x491,f3(x492,x491,x492,x491),x491))
% 1.53/1.64 [42]E(f3(x421,x422,x423,x423),x422)
% 1.53/1.64 [44]P1(x441,x442,f3(x441,x442,x443,x444))
% 1.53/1.64 [46]P2(x461,f3(x462,x461,x463,x464),x463,x464)
% 1.53/1.64 [54]~P1(x541,x542,x541)+E(x541,x542)
% 1.53/1.64 [55]~E(x551,x552)+E(f3(x551,x552,x551,x552),x552)
% 1.53/1.64 [58]E(x581,x582)+~E(f3(x582,x581,x582,x581),x581)
% 1.53/1.64 [60]E(x601,x602)+E(f3(x601,x602,x601,x602),f3(x601,x602,x602,x601))
% 1.53/1.64 [57]~P2(x571,x572,x573,x573)+E(x571,x572)
% 1.53/1.64 [62]~P2(x624,x623,x622,x621)+P2(x621,x622,x623,x624)
% 1.53/1.64 [63]~P2(x633,x634,x632,x631)+P2(x631,x632,x633,x634)
% 1.53/1.64 [64]~P2(x644,x643,x641,x642)+P2(x641,x642,x643,x644)
% 1.53/1.64 [65]~P2(x653,x654,x651,x652)+P2(x651,x652,x653,x654)
% 1.53/1.64 [66]~P2(x662,x661,x664,x663)+P2(x661,x662,x663,x664)
% 1.53/1.64 [67]~P2(x672,x671,x673,x674)+P2(x671,x672,x673,x674)
% 1.53/1.64 [68]~P2(x681,x682,x684,x683)+P2(x681,x682,x683,x684)
% 1.53/1.64 [59]P1(x591,x592,x593)+~E(x593,f3(x591,x592,x594,x595))
% 1.53/1.64 [56]~P1(x561,x562,x563)+E(x561,x562)+E(f3(x561,x562,x562,x563),x563)
% 1.53/1.64 [75]~P1(x755,x751,x754)+~P1(x752,x753,x754)+P1(x751,f8(x752,x753,x754,x751,x755),x752)
% 1.53/1.64 [76]~P1(x765,x764,x763)+~P1(x762,x761,x763)+P1(x761,f8(x762,x761,x763,x764,x765),x765)
% 1.53/1.64 [70]~P2(x705,x706,x701,x702)+P2(x701,x702,x703,x704)+~P2(x705,x706,x703,x704)
% 1.53/1.64 [71]~P2(x711,x712,x715,x716)+P2(x711,x712,x713,x714)+~P2(x715,x716,x713,x714)
% 1.53/1.64 [69]~P2(x693,x694,x695,x696)+E(x691,x692)+E(f3(x691,x692,x693,x694),f3(x691,x692,x695,x696))
% 1.53/1.64 [77]~P1(x774,x772,x773)+~P1(x771,x772,x775)+E(x771,x772)+P1(x771,x773,f4(x771,x774,x772,x773,x775))
% 1.53/1.64 [78]~P1(x783,x782,x784)+~P1(x781,x782,x785)+E(x781,x782)+P1(x781,x783,f5(x781,x783,x782,x784,x785))
% 1.53/1.64 [79]~P1(x793,x792,x794)+~P1(x791,x792,x795)+E(x791,x792)+P1(f5(x791,x793,x792,x794,x795),x795,f4(x791,x793,x792,x794,x795))
% 1.53/1.64 [61]~P1(x613,x614,x612)+~P1(x613,x614,x611)+~P2(x614,x611,x614,x612)+E(x611,x612)+E(x613,x614)
% 1.53/1.64 [72]~P2(x726,x722,x725,x724)+~P2(x721,x726,x723,x725)+P2(x721,x722,x723,x724)+~P1(x723,x725,x724)+~P1(x721,x726,x722)
% 1.53/1.64 [80]~P1(x803,x804,x805)+~P1(x802,x803,x805)+~P2(x802,x805,x802,x806)+~P2(x802,x803,x802,x801)+P1(x801,f6(x802,x803,x801,x804,x805,x806),x806)
% 1.53/1.64 [81]~P1(x813,x812,x815)+~P1(x811,x813,x815)+~P2(x811,x815,x811,x816)+~P2(x811,x813,x811,x814)+P2(x811,x812,x811,f6(x811,x813,x814,x812,x815,x816))
% 1.53/1.64 [73]P1(x735,x733,x734)+P1(x734,x735,x733)+~P2(x733,x731,x733,x732)+~P2(x735,x731,x735,x732)+~P2(x734,x731,x734,x732)+E(x731,x732)+P1(x733,x734,x735)
% 1.53/1.64 [74]~P1(x741,x742,x743)+~P2(x742,x744,x748,x746)+~P2(x742,x743,x748,x745)+~P2(x741,x744,x747,x746)+~P2(x741,x742,x747,x748)+E(x741,x742)+P2(x743,x744,x745,x746)+~P1(x747,x748,x745)
% 1.53/1.64 %EqnAxiom
% 1.53/1.64 [1]E(x11,x11)
% 1.53/1.64 [2]E(x22,x21)+~E(x21,x22)
% 1.53/1.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.53/1.64 [4]~E(x41,x42)+E(f3(x41,x43,x44,x45),f3(x42,x43,x44,x45))
% 1.53/1.64 [5]~E(x51,x52)+E(f3(x53,x51,x54,x55),f3(x53,x52,x54,x55))
% 1.53/1.64 [6]~E(x61,x62)+E(f3(x63,x64,x61,x65),f3(x63,x64,x62,x65))
% 1.53/1.64 [7]~E(x71,x72)+E(f3(x73,x74,x75,x71),f3(x73,x74,x75,x72))
% 1.53/1.64 [8]~E(x81,x82)+E(f6(x81,x83,x84,x85,x86,x87),f6(x82,x83,x84,x85,x86,x87))
% 1.53/1.64 [9]~E(x91,x92)+E(f6(x93,x91,x94,x95,x96,x97),f6(x93,x92,x94,x95,x96,x97))
% 1.53/1.64 [10]~E(x101,x102)+E(f6(x103,x104,x101,x105,x106,x107),f6(x103,x104,x102,x105,x106,x107))
% 1.53/1.64 [11]~E(x111,x112)+E(f6(x113,x114,x115,x111,x116,x117),f6(x113,x114,x115,x112,x116,x117))
% 1.53/1.64 [12]~E(x121,x122)+E(f6(x123,x124,x125,x126,x121,x127),f6(x123,x124,x125,x126,x122,x127))
% 1.53/1.64 [13]~E(x131,x132)+E(f6(x133,x134,x135,x136,x137,x131),f6(x133,x134,x135,x136,x137,x132))
% 1.53/1.64 [14]~E(x141,x142)+E(f8(x141,x143,x144,x145,x146),f8(x142,x143,x144,x145,x146))
% 1.53/1.64 [15]~E(x151,x152)+E(f8(x153,x151,x154,x155,x156),f8(x153,x152,x154,x155,x156))
% 1.53/1.64 [16]~E(x161,x162)+E(f8(x163,x164,x161,x165,x166),f8(x163,x164,x162,x165,x166))
% 1.53/1.64 [17]~E(x171,x172)+E(f8(x173,x174,x175,x171,x176),f8(x173,x174,x175,x172,x176))
% 1.53/1.64 [18]~E(x181,x182)+E(f8(x183,x184,x185,x186,x181),f8(x183,x184,x185,x186,x182))
% 1.53/1.64 [19]~E(x191,x192)+E(f4(x191,x193,x194,x195,x196),f4(x192,x193,x194,x195,x196))
% 1.53/1.64 [20]~E(x201,x202)+E(f4(x203,x201,x204,x205,x206),f4(x203,x202,x204,x205,x206))
% 1.53/1.64 [21]~E(x211,x212)+E(f4(x213,x214,x211,x215,x216),f4(x213,x214,x212,x215,x216))
% 1.53/1.64 [22]~E(x221,x222)+E(f4(x223,x224,x225,x221,x226),f4(x223,x224,x225,x222,x226))
% 1.53/1.64 [23]~E(x231,x232)+E(f4(x233,x234,x235,x236,x231),f4(x233,x234,x235,x236,x232))
% 1.53/1.64 [24]~E(x241,x242)+E(f5(x241,x243,x244,x245,x246),f5(x242,x243,x244,x245,x246))
% 1.53/1.64 [25]~E(x251,x252)+E(f5(x253,x251,x254,x255,x256),f5(x253,x252,x254,x255,x256))
% 1.53/1.64 [26]~E(x261,x262)+E(f5(x263,x264,x261,x265,x266),f5(x263,x264,x262,x265,x266))
% 1.53/1.64 [27]~E(x271,x272)+E(f5(x273,x274,x275,x271,x276),f5(x273,x274,x275,x272,x276))
% 1.53/1.64 [28]~E(x281,x282)+E(f5(x283,x284,x285,x286,x281),f5(x283,x284,x285,x286,x282))
% 1.53/1.64 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 1.53/1.64 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 1.53/1.64 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 1.53/1.64 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 1.53/1.64 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 1.53/1.65 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 1.53/1.65 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 1.53/1.65
% 1.53/1.65 %-------------------------------------------
% 1.53/1.65 cnf(84,plain,
% 1.53/1.65 (P1(x841,x842,f3(x843,f3(x841,x842,x844,x845),x846,x846))),
% 1.53/1.65 inference(scs_inference,[],[42,59])).
% 1.53/1.65 cnf(85,plain,
% 1.53/1.65 (E(f3(x851,x852,x853,x853),x852)),
% 1.53/1.65 inference(rename_variables,[],[42])).
% 1.53/1.65 cnf(90,plain,
% 1.53/1.65 (E(x901,f3(x902,x901,x903,x903))),
% 1.53/1.65 inference(scs_inference,[],[42,85,48,59,58,2])).
% 1.53/1.65 cnf(91,plain,
% 1.53/1.65 (P1(x911,x912,f3(f3(x913,x911,x914,x914),x912,x915,x916))),
% 1.53/1.65 inference(scs_inference,[],[44,42,85,48,59,58,2,29])).
% 1.53/1.65 cnf(94,plain,
% 1.53/1.65 (P1(x941,x942,x942)),
% 1.53/1.65 inference(rename_variables,[],[38])).
% 1.53/1.65 cnf(95,plain,
% 1.53/1.65 (P2(f3(x951,x952,x953,x954),x952,x953,x954)),
% 1.53/1.65 inference(scs_inference,[],[53,39,38,46,44,42,85,48,59,58,2,29,30,70])).
% 1.53/1.65 cnf(97,plain,
% 1.53/1.65 (P2(x971,x972,x972,x971)),
% 1.53/1.65 inference(rename_variables,[],[39])).
% 1.53/1.65 cnf(99,plain,
% 1.53/1.65 (P2(x991,x992,x992,f3(f3(x991,x992,x991,x992),x992,f3(x991,x992,x991,x992),x992))),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,38,46,44,42,85,49,48,59,58,2,29,30,70,71])).
% 1.53/1.65 cnf(102,plain,
% 1.53/1.65 (~E(a1,f3(x1021,a11,x1022,x1022))),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,38,46,44,42,85,49,48,59,58,2,29,30,70,71,3])).
% 1.53/1.65 cnf(103,plain,
% 1.53/1.65 (E(f3(x1031,x1032,x1033,x1033),x1032)),
% 1.53/1.65 inference(rename_variables,[],[42])).
% 1.53/1.65 cnf(104,plain,
% 1.53/1.65 (~E(a11,a1)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,38,94,46,44,42,85,49,48,59,58,2,29,30,70,71,3,31])).
% 1.53/1.65 cnf(106,plain,
% 1.53/1.65 (P2(x1061,x1062,x1062,f3(x1063,x1061,x1064,x1064))),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32])).
% 1.53/1.65 cnf(107,plain,
% 1.53/1.65 (P2(x1071,x1072,x1072,x1071)),
% 1.53/1.65 inference(rename_variables,[],[39])).
% 1.53/1.65 cnf(108,plain,
% 1.53/1.65 (P2(x1081,x1082,f3(x1083,x1082,x1084,x1084),x1081)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33])).
% 1.53/1.65 cnf(109,plain,
% 1.53/1.65 (P2(x1091,x1092,x1092,x1091)),
% 1.53/1.65 inference(rename_variables,[],[39])).
% 1.53/1.65 cnf(110,plain,
% 1.53/1.65 (P2(x1101,f3(x1102,x1103,x1104,x1104),x1103,x1101)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34])).
% 1.53/1.65 cnf(111,plain,
% 1.53/1.65 (P2(x1111,x1112,x1112,x1111)),
% 1.53/1.65 inference(rename_variables,[],[39])).
% 1.53/1.65 cnf(112,plain,
% 1.53/1.65 (P2(f3(x1121,x1122,x1123,x1123),x1124,x1124,x1122)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,111,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34,35])).
% 1.53/1.65 cnf(116,plain,
% 1.53/1.65 (~P2(a1,a11,x1161,x1161)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,111,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34,35,54,57])).
% 1.53/1.65 cnf(118,plain,
% 1.53/1.65 (~P2(x1181,x1181,a11,a1)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,111,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34,35,54,57,62])).
% 1.53/1.65 cnf(120,plain,
% 1.53/1.65 (~P2(a11,a1,x1201,x1201)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,111,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34,35,54,57,62,63])).
% 1.53/1.65 cnf(122,plain,
% 1.53/1.65 (~P2(x1221,x1221,a1,a11)),
% 1.53/1.65 inference(scs_inference,[],[53,39,97,107,109,111,38,94,46,44,42,85,103,49,48,59,58,2,29,30,70,71,3,31,32,33,34,35,54,57,62,63,64])).
% 1.53/1.65 cnf(132,plain,
% 1.53/1.65 (~P2(a1,f3(x1321,a11,x1322,x1322),x1323,x1323)),
% 1.53/1.65 inference(scs_inference,[],[102,57])).
% 1.53/1.65 cnf(134,plain,
% 1.53/1.65 (~P1(a1,f3(x1341,a11,x1342,x1342),a1)),
% 1.53/1.65 inference(scs_inference,[],[102,57,54])).
% 1.53/1.65 cnf(136,plain,
% 1.53/1.65 (~P2(x1361,x1361,a1,f3(x1362,a11,x1363,x1363))),
% 1.53/1.65 inference(scs_inference,[],[102,57,54,64])).
% 1.53/1.65 cnf(138,plain,
% 1.53/1.65 (~P2(x1381,x1381,f3(x1382,a11,x1383,x1383),a1)),
% 1.53/1.65 inference(scs_inference,[],[102,57,54,64,62])).
% 1.53/1.65 cnf(140,plain,
% 1.53/1.65 (E(a2,a1)),
% 1.53/1.65 inference(scs_inference,[],[102,36,57,54,64,62,2])).
% 1.53/1.65 cnf(142,plain,
% 1.53/1.65 (P2(f3(x1421,x1422,x1423,x1424),x1422,x1423,x1424)),
% 1.53/1.65 inference(rename_variables,[],[95])).
% 1.53/1.65 cnf(143,plain,
% 1.53/1.65 (P2(f3(x1431,x1432,x1433,x1434),x1432,x1433,f3(x1435,x1434,x1436,x1436))),
% 1.53/1.65 inference(scs_inference,[],[95,142,90,116,102,36,57,54,64,62,2,32,35])).
% 1.53/1.65 cnf(144,plain,
% 1.53/1.65 (P2(f3(x1441,x1442,x1443,x1444),x1442,x1443,x1444)),
% 1.53/1.65 inference(rename_variables,[],[95])).
% 1.53/1.65 cnf(145,plain,
% 1.53/1.65 (E(f3(x1451,a1,x1452,x1452),a2)),
% 1.53/1.65 inference(scs_inference,[],[95,142,90,116,102,36,42,57,54,64,62,2,32,35,3])).
% 1.53/1.65 cnf(147,plain,
% 1.53/1.65 (P1(f3(x1471,x1472,x1473,x1473),x1474,f3(x1475,f3(x1472,x1474,x1476,x1477),x1478,x1478))),
% 1.53/1.65 inference(scs_inference,[],[84,95,142,90,116,102,36,42,57,54,64,62,2,32,35,3,29])).
% 1.53/1.65 cnf(148,plain,
% 1.53/1.65 (P1(x1481,x1482,f3(x1483,f3(x1481,x1482,x1484,x1485),x1486,x1486))),
% 1.53/1.65 inference(rename_variables,[],[84])).
% 1.53/1.65 cnf(149,plain,
% 1.53/1.65 (P1(x1491,f3(x1492,x1493,x1494,x1494),f3(x1495,f3(x1491,x1493,x1496,x1497),x1498,x1498))),
% 1.53/1.65 inference(scs_inference,[],[84,148,95,142,90,116,102,36,42,57,54,64,62,2,32,35,3,29,30])).
% 1.53/1.65 cnf(150,plain,
% 1.53/1.65 (P1(x1501,x1502,f3(x1503,f3(x1501,x1502,x1504,x1505),x1506,x1506))),
% 1.53/1.65 inference(rename_variables,[],[84])).
% 1.53/1.65 cnf(151,plain,
% 1.53/1.65 (P2(f3(x1511,x1512,x1513,x1514),x1512,f3(x1515,x1513,x1516,x1516),x1514)),
% 1.53/1.65 inference(scs_inference,[],[84,148,95,142,144,90,116,102,36,42,57,54,64,62,2,32,35,3,29,30,34])).
% 1.53/1.65 cnf(152,plain,
% 1.53/1.65 (P2(f3(x1521,x1522,x1523,x1524),x1522,x1523,x1524)),
% 1.53/1.65 inference(rename_variables,[],[95])).
% 1.53/1.65 cnf(155,plain,
% 1.53/1.65 (~E(x1551,f3(x1552,x1551,a11,a1))),
% 1.53/1.65 inference(scs_inference,[],[53,84,148,150,95,142,144,152,90,116,118,102,36,42,57,54,64,62,2,32,35,3,29,30,34,31,33])).
% 1.53/1.65 cnf(158,plain,
% 1.53/1.65 (~P2(f3(x1581,a11,x1582,x1582),a1,x1583,x1583)),
% 1.53/1.65 inference(scs_inference,[],[53,84,148,150,95,142,144,152,90,116,118,102,36,42,57,54,64,62,2,32,35,3,29,30,34,31,33,67])).
% 1.53/1.65 cnf(164,plain,
% 1.53/1.65 (~P1(a11,a1,a11)),
% 1.53/1.65 inference(scs_inference,[],[104,54])).
% 1.53/1.65 cnf(166,plain,
% 1.53/1.65 (~P2(x1661,f3(x1662,x1661,a11,a1),x1663,x1663)),
% 1.53/1.65 inference(scs_inference,[],[104,155,54,57])).
% 1.53/1.65 cnf(168,plain,
% 1.53/1.65 (~P2(x1681,x1681,f3(x1682,x1683,a11,a1),x1683)),
% 1.53/1.65 inference(scs_inference,[],[104,155,54,57,62])).
% 1.53/1.65 cnf(170,plain,
% 1.53/1.65 (E(a2,f3(x1701,a1,x1702,x1702))),
% 1.53/1.65 inference(scs_inference,[],[104,155,145,54,57,62,2])).
% 1.53/1.65 cnf(171,plain,
% 1.53/1.65 (P2(f3(x1711,x1712,x1713,x1713),x1714,f3(x1715,x1712,x1716,x1716),x1714)),
% 1.53/1.65 inference(scs_inference,[],[108,112,104,155,145,54,57,62,2,71])).
% 1.53/1.65 cnf(172,plain,
% 1.53/1.65 (P2(x1721,x1722,f3(x1723,x1722,x1724,x1724),x1721)),
% 1.53/1.65 inference(rename_variables,[],[108])).
% 1.53/1.65 cnf(174,plain,
% 1.53/1.65 (P2(f3(x1741,x1742,x1743,x1743),f3(x1744,x1745,x1746,x1746),x1742,x1745)),
% 1.53/1.65 inference(scs_inference,[],[108,172,112,104,155,145,54,57,62,2,71,70])).
% 1.53/1.65 cnf(176,plain,
% 1.53/1.65 (P2(x1761,x1762,f3(x1763,x1762,x1764,x1764),x1761)),
% 1.53/1.65 inference(rename_variables,[],[108])).
% 1.53/1.65 cnf(179,plain,
% 1.53/1.65 (P2(x1791,x1792,f3(x1793,x1792,x1794,x1794),x1791)),
% 1.53/1.65 inference(rename_variables,[],[108])).
% 1.53/1.65 cnf(180,plain,
% 1.53/1.65 (~P2(a1,f3(x1801,a11,x1802,x1802),x1803,x1803)),
% 1.53/1.65 inference(rename_variables,[],[132])).
% 1.53/1.65 cnf(181,plain,
% 1.53/1.65 (P1(x1811,a2,f3(f3(x1812,x1811,x1813,x1813),f3(x1814,a1,x1815,x1815),x1816,x1817))),
% 1.53/1.65 inference(scs_inference,[],[91,108,172,176,112,104,155,132,145,54,57,62,2,71,70,35,30])).
% 1.53/1.65 cnf(182,plain,
% 1.53/1.65 (P1(x1821,x1822,f3(f3(x1823,x1821,x1824,x1824),x1822,x1825,x1826))),
% 1.53/1.65 inference(rename_variables,[],[91])).
% 1.53/1.65 cnf(186,plain,
% 1.53/1.65 (~P2(a1,f3(x1861,a11,x1862,x1862),x1863,x1863)),
% 1.53/1.65 inference(rename_variables,[],[132])).
% 1.53/1.65 cnf(187,plain,
% 1.53/1.65 (~E(f3(x1871,a1,x1872,x1872),f3(x1873,a11,x1874,x1874))),
% 1.53/1.65 inference(scs_inference,[],[91,108,172,176,179,112,106,104,155,132,180,186,145,140,54,57,62,2,71,70,35,30,3,32,33])).
% 1.53/1.65 cnf(188,plain,
% 1.53/1.65 (P2(x1881,x1882,x1882,f3(x1883,x1881,x1884,x1884))),
% 1.53/1.65 inference(rename_variables,[],[106])).
% 1.53/1.65 cnf(189,plain,
% 1.53/1.65 (~P2(a1,f3(x1891,a11,x1892,x1892),x1893,x1893)),
% 1.53/1.65 inference(rename_variables,[],[132])).
% 1.53/1.65 cnf(192,plain,
% 1.53/1.65 (~E(f3(f3(x1921,a12,x1922,x1922),a11,x1923,x1924),a1)),
% 1.53/1.65 inference(scs_inference,[],[53,91,182,147,108,172,176,179,112,106,104,155,132,180,186,145,140,54,57,62,2,71,70,35,30,3,32,33,29,31])).
% 1.53/1.65 cnf(194,plain,
% 1.53/1.65 (~E(f3(x1941,a11,x1942,x1942),f3(x1943,a1,x1944,x1944))),
% 1.53/1.65 inference(scs_inference,[],[53,91,182,147,108,172,176,179,112,106,188,104,155,132,180,186,189,145,140,54,57,62,2,71,70,35,30,3,32,33,29,31,34])).
% 1.53/1.65 cnf(197,plain,
% 1.53/1.65 (~P2(x1971,x1971,x1972,f3(x1973,x1972,a11,a1))),
% 1.53/1.65 inference(scs_inference,[],[53,91,182,147,108,172,176,179,112,106,188,104,155,132,180,186,189,145,140,54,57,62,2,71,70,35,30,3,32,33,29,31,34,68])).
% 1.53/1.65 cnf(199,plain,
% 1.53/1.65 (~P2(f3(x1991,x1992,a11,a1),x1992,x1993,x1993)),
% 1.53/1.65 inference(scs_inference,[],[53,91,182,147,108,172,176,179,112,106,188,104,155,132,180,186,189,145,140,54,57,62,2,71,70,35,30,3,32,33,29,31,34,68,65])).
% 1.53/1.65 cnf(201,plain,
% 1.53/1.65 (P1(x2011,a1,a2)),
% 1.53/1.65 inference(scs_inference,[],[53,91,182,147,108,172,176,179,112,106,188,104,155,132,180,186,189,145,140,54,57,62,2,71,70,35,30,3,32,33,29,31,34,68,65,59])).
% 1.53/1.65 cnf(216,plain,
% 1.53/1.65 (~P2(x2161,x2161,f3(x2162,a11,x2163,x2163),f3(x2164,a1,x2165,x2165))),
% 1.53/1.65 inference(scs_inference,[],[155,187,57,54,62])).
% 1.53/1.65 cnf(218,plain,
% 1.53/1.65 (E(x2181,f3(f3(x2181,x2182,x2181,x2182),x2182,f3(x2181,x2182,x2181,x2182),x2182))),
% 1.53/1.65 inference(scs_inference,[],[155,48,187,57,54,62,2])).
% 1.53/1.65 cnf(219,plain,
% 1.53/1.65 (P2(f3(x2191,x2192,x2193,x2193),x2194,x2192,f3(x2195,x2194,x2196,x2196))),
% 1.53/1.65 inference(scs_inference,[],[110,108,155,48,187,57,54,62,2,71])).
% 1.53/1.65 cnf(220,plain,
% 1.53/1.65 (P2(x2201,f3(x2202,x2203,x2204,x2204),x2203,x2201)),
% 1.53/1.65 inference(rename_variables,[],[110])).
% 1.53/1.65 cnf(221,plain,
% 1.53/1.65 (P2(x2211,x2212,f3(x2213,x2212,x2214,x2214),x2211)),
% 1.53/1.65 inference(rename_variables,[],[108])).
% 1.53/1.65 cnf(223,plain,
% 1.53/1.65 (P2(x2231,x2232,f3(x2233,f3(x2234,x2231,x2235,x2235),x2236,x2236),x2232)),
% 1.53/1.65 inference(scs_inference,[],[110,220,108,221,155,48,187,57,54,62,2,71,70])).
% 1.53/1.65 cnf(227,plain,
% 1.53/1.65 (P2(f3(x2271,x2272,x2273,x2274),x2272,x2273,f3(x2275,x2274,x2276,x2276))),
% 1.53/1.65 inference(rename_variables,[],[143])).
% 1.53/1.65 cnf(228,plain,
% 1.53/1.65 (~P2(f3(x2281,x2282,a11,a1),x2282,x2283,x2283)),
% 1.53/1.65 inference(rename_variables,[],[199])).
% 1.53/1.65 cnf(229,plain,
% 1.53/1.65 (~E(x2291,f3(x2292,x2291,a1,f3(x2293,a11,x2294,x2294)))),
% 1.53/1.65 inference(scs_inference,[],[136,110,220,108,221,155,46,48,143,199,187,57,54,62,2,71,70,35,32])).
% 1.53/1.65 cnf(231,plain,
% 1.53/1.65 (~P2(x2311,x2311,a1,f3(x2312,a11,x2313,x2313))),
% 1.53/1.65 inference(rename_variables,[],[136])).
% 1.53/1.65 cnf(233,plain,
% 1.53/1.65 (P1(x2331,a1,a2)),
% 1.53/1.65 inference(rename_variables,[],[201])).
% 1.53/1.65 cnf(237,plain,
% 1.53/1.65 (P2(f3(x2371,x2372,x2373,x2374),x2372,x2373,f3(x2375,x2374,x2376,x2376))),
% 1.53/1.65 inference(rename_variables,[],[143])).
% 1.53/1.65 cnf(239,plain,
% 1.53/1.65 (~E(a2,a11)),
% 1.53/1.65 inference(scs_inference,[],[201,233,136,110,220,108,221,155,46,48,143,227,199,228,187,194,170,164,57,54,62,2,71,70,35,32,30,3,34,31])).
% 1.53/1.65 cnf(240,plain,
% 1.53/1.65 (P1(x2401,a1,a2)),
% 1.53/1.65 inference(rename_variables,[],[201])).
% 1.53/1.65 cnf(241,plain,
% 1.53/1.65 (~E(a2,a12)),
% 1.53/1.65 inference(scs_inference,[],[53,201,233,136,110,220,108,221,155,46,48,143,227,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29])).
% 1.53/1.65 cnf(242,plain,
% 1.53/1.65 (~E(x2421,f3(x2422,x2421,a1,a11))),
% 1.53/1.65 inference(scs_inference,[],[53,201,233,136,231,110,220,108,221,155,46,48,143,227,237,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33])).
% 1.53/1.65 cnf(245,plain,
% 1.53/1.65 (~P2(a2,f3(f3(x2451,f3(x2452,a1,x2453,x2453),x2454,x2454),f3(x2452,a1,x2453,x2453),a11,a1),a1,a2)),
% 1.53/1.65 inference(scs_inference,[],[53,201,233,240,181,136,231,110,220,108,221,112,155,46,48,143,227,237,166,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33,72])).
% 1.53/1.65 cnf(253,plain,
% 1.53/1.65 (~P2(a1,a2,f3(f3(x2531,f3(x2532,a1,x2533,x2533),x2534,x2534),f3(x2532,a1,x2533,x2533),a11,a1),a2)),
% 1.53/1.65 inference(scs_inference,[],[53,201,233,240,181,136,231,110,220,108,221,112,155,46,48,143,227,237,166,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33,72,66,63])).
% 1.53/1.66 cnf(257,plain,
% 1.53/1.66 (~P2(f3(f3(x2571,f3(x2572,a1,x2573,x2573),x2574,x2574),f3(x2572,a1,x2573,x2573),a11,a1),a2,a1,a2)),
% 1.53/1.66 inference(scs_inference,[],[53,201,233,240,181,136,231,110,220,108,221,112,155,46,48,143,227,237,166,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33,72,66,63,68,67])).
% 1.53/1.66 cnf(261,plain,
% 1.53/1.66 (P1(f3(x2611,x2612,x2611,x2612),x2612,x2611)),
% 1.53/1.66 inference(scs_inference,[],[53,201,233,240,181,136,231,110,220,108,221,112,155,46,48,143,227,237,166,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33,72,66,63,68,67,65,59])).
% 1.53/1.66 cnf(263,plain,
% 1.53/1.66 (~P2(a2,a1,a2,f3(f3(x2631,f3(x2632,a1,x2633,x2633),x2634,x2634),f3(x2632,a1,x2633,x2633),a11,a1))),
% 1.53/1.66 inference(scs_inference,[],[53,201,233,240,181,136,231,110,220,108,221,112,155,46,48,143,227,237,166,199,228,187,194,170,37,164,57,54,62,2,71,70,35,32,30,3,34,31,29,33,72,66,63,68,67,65,59,64])).
% 1.53/1.66 cnf(288,plain,
% 1.53/1.66 (P2(x2881,f3(x2882,x2883,x2884,x2884),f3(x2885,x2881,x2886,x2886),x2883)),
% 1.53/1.66 inference(scs_inference,[],[241,110,108,253,257,263,63,66,68,54,57,64,62,71])).
% 1.53/1.66 cnf(291,plain,
% 1.53/1.66 (P2(x2911,x2912,f3(x2913,x2911,x2914,x2914),f3(x2915,x2912,x2916,x2916))),
% 1.53/1.66 inference(scs_inference,[],[241,110,108,106,253,257,263,63,66,68,54,57,64,62,71,70])).
% 1.53/1.66 cnf(294,plain,
% 1.53/1.66 (~E(f3(f3(a11,a1,a11,a1),a1,f3(a11,a1,a11,a1),a1),a1)),
% 1.53/1.66 inference(scs_inference,[],[241,120,110,108,99,106,253,257,263,63,66,68,54,57,64,62,71,70,35])).
% 1.53/1.66 cnf(295,plain,
% 1.53/1.66 (P2(x2951,x2952,x2952,f3(f3(x2951,x2952,x2951,x2952),x2952,f3(x2951,x2952,x2951,x2952),x2952))),
% 1.53/1.66 inference(rename_variables,[],[99])).
% 1.53/1.66 cnf(296,plain,
% 1.53/1.66 (~P2(a11,a1,x2961,x2961)),
% 1.53/1.66 inference(rename_variables,[],[120])).
% 1.53/1.66 cnf(299,plain,
% 1.53/1.66 (~P2(a11,a1,x2991,x2991)),
% 1.53/1.66 inference(rename_variables,[],[120])).
% 1.53/1.66 cnf(302,plain,
% 1.53/1.66 (P1(x3021,f3(f3(a2,x3022,a2,x3022),x3022,f3(a2,x3022,a2,x3022),x3022),f3(f3(x3023,x3021,x3024,x3024),f3(x3025,a1,x3026,x3026),x3027,x3028))),
% 1.53/1.66 inference(scs_inference,[],[241,181,120,296,110,108,48,99,106,151,218,253,257,263,63,66,68,54,57,64,62,71,70,35,32,3,30])).
% 1.53/1.66 cnf(304,plain,
% 1.53/1.66 (~E(f3(a1,a11,a1,a11),a12)),
% 1.53/1.66 inference(scs_inference,[],[53,261,241,181,120,296,110,108,48,99,106,151,218,253,257,263,63,66,68,54,57,64,62,71,70,35,32,3,30,29])).
% 1.53/1.66 cnf(311,plain,
% 1.53/1.66 (~E(f3(a11,a1,a11,a1),a1)),
% 1.53/1.66 inference(scs_inference,[],[53,261,149,241,181,120,296,299,110,108,48,99,295,106,151,218,253,257,263,134,63,66,68,54,57,64,62,71,70,35,32,3,30,29,31,34,55])).
% 1.53/1.66 cnf(334,plain,
% 1.53/1.66 (P2(f3(x3341,x3342,x3343,x3343),x3344,x3344,x3342)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(337,plain,
% 1.53/1.66 (P2(f3(x3371,f3(x3372,x3373,x3374,x3374),x3375,x3376),x3373,x3375,x3376)),
% 1.53/1.66 inference(scs_inference,[],[304,112,334,110,46,54,57,64,71,70])).
% 1.53/1.66 cnf(343,plain,
% 1.53/1.66 (~P2(f3(x3431,a11,x3432,x3432),a1,x3433,x3433)),
% 1.53/1.66 inference(rename_variables,[],[158])).
% 1.53/1.66 cnf(346,plain,
% 1.53/1.66 (~E(f3(x3461,f3(x3462,a1,x3463,x3463),x3464,x3464),f3(x3465,a11,x3466,x3466))),
% 1.53/1.66 inference(scs_inference,[],[304,158,343,112,334,110,46,170,219,99,291,54,57,64,71,70,35,33,32])).
% 1.53/1.66 cnf(349,plain,
% 1.53/1.66 (P1(f3(x3491,a2,x3491,a2),f3(x3492,a1,x3493,x3493),x3491)),
% 1.53/1.66 inference(scs_inference,[],[261,304,158,343,112,334,110,46,170,219,99,291,54,57,64,71,70,35,33,32,30])).
% 1.53/1.66 cnf(350,plain,
% 1.53/1.66 (P1(f3(x3501,x3502,x3501,x3502),x3502,x3501)),
% 1.53/1.66 inference(rename_variables,[],[261])).
% 1.53/1.66 cnf(353,plain,
% 1.53/1.66 (P1(f3(a2,x3531,a2,x3531),x3531,f3(x3532,a1,x3533,x3533))),
% 1.53/1.66 inference(scs_inference,[],[261,350,304,158,343,112,334,110,46,170,42,219,99,291,54,57,64,71,70,35,33,32,30,3,31])).
% 1.53/1.66 cnf(355,plain,
% 1.53/1.66 (P1(f3(x3551,a1,x3552,x3552),x3553,f3(x3554,f3(a2,x3553,x3555,x3556),x3557,x3557))),
% 1.53/1.66 inference(scs_inference,[],[261,350,84,304,158,343,112,334,110,46,170,42,219,99,291,54,57,64,71,70,35,33,32,30,3,31,29])).
% 1.53/1.66 cnf(382,plain,
% 1.53/1.66 (~P1(f3(f3(x3821,a12,x3822,x3822),a11,x3823,x3824),a1,f3(f3(x3821,a12,x3822,x3822),a11,x3823,x3824))),
% 1.53/1.66 inference(scs_inference,[],[192,57,54])).
% 1.53/1.66 cnf(390,plain,
% 1.53/1.66 (P2(f3(x3901,x3902,x3903,x3903),x3904,x3904,x3902)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(392,plain,
% 1.53/1.66 (P2(f3(x3921,x3922,x3923,x3923),x3922,x3924,x3924)),
% 1.53/1.66 inference(scs_inference,[],[192,112,390,110,41,57,54,64,62,71,70])).
% 1.53/1.66 cnf(397,plain,
% 1.53/1.66 (P2(x3971,x3972,f3(x3973,f3(x3974,x3971,x3975,x3975),x3976,x3976),x3972)),
% 1.53/1.66 inference(rename_variables,[],[223])).
% 1.53/1.66 cnf(398,plain,
% 1.53/1.66 (~P2(a1,a11,x3981,x3981)),
% 1.53/1.66 inference(rename_variables,[],[116])).
% 1.53/1.66 cnf(401,plain,
% 1.53/1.66 (~P2(a1,a11,x4011,x4011)),
% 1.53/1.66 inference(rename_variables,[],[116])).
% 1.53/1.66 cnf(407,plain,
% 1.53/1.66 (P1(f3(x4071,f3(x4072,a1,x4073,x4073),x4074,x4074),x4075,f3(x4076,f3(a2,x4075,x4077,x4078),x4079,x4079))),
% 1.53/1.66 inference(scs_inference,[],[355,304,116,398,401,192,48,112,390,90,110,41,223,397,143,57,54,64,62,71,70,35,33,3,32,29])).
% 1.53/1.66 cnf(435,plain,
% 1.53/1.66 (~P1(f3(x4351,a11,x4352,x4352),f3(x4353,a1,x4354,x4354),f3(x4351,a11,x4352,x4352))),
% 1.53/1.66 inference(scs_inference,[],[194,54])).
% 1.53/1.66 cnf(441,plain,
% 1.53/1.66 (P2(x4411,f3(x4412,x4411,x4413,x4414),f3(x4415,x4414,x4416,x4416),x4413)),
% 1.53/1.66 inference(scs_inference,[],[108,46,194,229,54,57,62,71])).
% 1.53/1.66 cnf(442,plain,
% 1.53/1.66 (P2(x4421,x4422,f3(x4423,x4422,x4424,x4424),x4421)),
% 1.53/1.66 inference(rename_variables,[],[108])).
% 1.53/1.66 cnf(444,plain,
% 1.53/1.66 (P2(f3(x4441,f3(x4442,x4443,x4444,x4445),x4446,x4446),x4443,x4444,x4445)),
% 1.53/1.66 inference(scs_inference,[],[108,442,46,194,229,54,57,62,71,70])).
% 1.53/1.66 cnf(445,plain,
% 1.53/1.66 (P2(x4451,f3(x4452,x4451,x4453,x4454),x4453,x4454)),
% 1.53/1.66 inference(rename_variables,[],[46])).
% 1.53/1.66 cnf(449,plain,
% 1.53/1.66 (P2(x4491,x4492,x4492,f3(f3(x4491,x4492,x4491,x4492),x4492,f3(x4491,x4492,x4491,x4492),x4492))),
% 1.53/1.66 inference(rename_variables,[],[99])).
% 1.53/1.66 cnf(450,plain,
% 1.53/1.66 (~P2(x4501,x4501,a1,a11)),
% 1.53/1.66 inference(rename_variables,[],[122])).
% 1.53/1.66 cnf(451,plain,
% 1.53/1.66 (~E(f3(x4511,x4512,a1,a11),x4512)),
% 1.53/1.66 inference(scs_inference,[],[122,450,108,442,46,445,194,229,99,54,57,62,71,70,35,33])).
% 1.53/1.66 cnf(463,plain,
% 1.53/1.66 (~E(f3(f3(x4631,a11,x4632,x4632),a2,f3(x4631,a11,x4632,x4632),a2),f3(x4631,a11,x4632,x4632))),
% 1.53/1.66 inference(scs_inference,[],[84,201,349,241,122,450,170,108,442,46,445,42,194,229,99,449,392,382,54,57,62,71,70,35,33,32,3,31,34,30,29])).
% 1.53/1.66 cnf(494,plain,
% 1.53/1.66 (P2(f3(x4941,x4942,x4943,x4943),f3(x4944,x4945,x4946,x4946),f3(x4947,x4945,x4948,x4948),x4942)),
% 1.53/1.66 inference(scs_inference,[],[463,112,171,57,54,62,64,71])).
% 1.53/1.66 cnf(496,plain,
% 1.53/1.66 (P2(f3(x4961,x4962,x4963,x4963),x4964,x4964,x4962)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(498,plain,
% 1.53/1.66 (P2(x4981,x4982,x4981,f3(x4983,x4982,x4984,x4984))),
% 1.53/1.66 inference(scs_inference,[],[463,112,496,171,39,57,54,62,64,71,70])).
% 1.53/1.66 cnf(549,plain,
% 1.53/1.66 (P2(f3(x5491,x5492,x5493,x5493),f3(x5494,x5492,x5495,x5496),x5495,x5496)),
% 1.53/1.66 inference(scs_inference,[],[242,108,95,106,54,57,62,64,71,70])).
% 1.53/1.66 cnf(553,plain,
% 1.53/1.66 (P2(f3(x5531,x5532,x5533,x5533),x5532,a2,f3(x5534,a1,x5535,x5535))),
% 1.53/1.66 inference(scs_inference,[],[170,242,108,95,392,106,54,57,62,64,71,70,35])).
% 1.53/1.66 cnf(556,plain,
% 1.53/1.66 (P2(x5561,f3(x5562,x5563,x5564,x5564),x5563,x5561)),
% 1.53/1.66 inference(rename_variables,[],[110])).
% 1.53/1.66 cnf(560,plain,
% 1.53/1.66 (P2(x5601,f3(x5602,x5601,x5603,x5604),x5603,x5604)),
% 1.53/1.66 inference(rename_variables,[],[46])).
% 1.53/1.66 cnf(562,plain,
% 1.53/1.66 (P1(f3(x5621,x5622,x5623,x5623),f3(x5624,a1,x5625,x5625),f3(x5626,f3(x5622,a2,x5627,x5628),x5629,x5629))),
% 1.53/1.66 inference(scs_inference,[],[147,349,245,138,170,242,108,110,46,95,392,106,54,57,62,64,71,70,35,33,31,32,30])).
% 1.53/1.66 cnf(567,plain,
% 1.53/1.66 (P1(f3(x5671,a1,x5672,x5672),f3(x5673,x5674,x5675,x5675),f3(x5676,f3(a2,x5674,x5677,x5678),x5679,x5679))),
% 1.53/1.66 inference(scs_inference,[],[147,149,349,245,138,168,170,242,108,110,556,46,95,392,106,54,57,62,64,71,70,35,33,31,32,30,34,29])).
% 1.53/1.66 cnf(569,plain,
% 1.53/1.66 (~E(f3(f3(x5691,a12,x5692,x5692),a11,x5693,x5694),a2)),
% 1.53/1.66 inference(scs_inference,[],[147,149,349,245,138,168,170,192,242,140,108,110,556,46,95,392,106,54,57,62,64,71,70,35,33,31,32,30,34,29,3])).
% 1.53/1.66 cnf(570,plain,
% 1.53/1.66 (~P1(f3(a1,a11,a1,a11),a11,f3(f3(x5701,a12,x5702,x5702),a11,a11,a1))),
% 1.53/1.66 inference(scs_inference,[],[261,147,149,349,245,138,168,170,192,242,140,108,110,556,46,560,451,95,392,106,54,57,62,64,71,70,35,33,31,32,30,34,29,3,61])).
% 1.53/1.66 cnf(594,plain,
% 1.53/1.66 (~P1(f3(a11,a1,a11,a1),a1,f3(a11,a1,a11,a1))),
% 1.53/1.66 inference(scs_inference,[],[311,294,57,54])).
% 1.53/1.66 cnf(602,plain,
% 1.53/1.66 (P2(x6021,x6021,x6022,f3(x6023,x6022,x6024,x6024))),
% 1.53/1.66 inference(scs_inference,[],[311,294,108,143,57,54,65,67,62,71])).
% 1.53/1.66 cnf(604,plain,
% 1.53/1.66 (P2(x6041,x6042,f3(x6043,x6042,x6044,x6044),x6041)),
% 1.53/1.66 inference(rename_variables,[],[108])).
% 1.53/1.66 cnf(610,plain,
% 1.53/1.66 (P2(f3(x6101,f3(x6102,x6103,x6104,x6105),x6106,x6106),x6103,x6104,x6105)),
% 1.53/1.66 inference(rename_variables,[],[444])).
% 1.53/1.66 cnf(611,plain,
% 1.53/1.66 (~E(f3(x6111,x6112,a11,a1),f3(x6113,x6112,x6114,x6114))),
% 1.53/1.66 inference(scs_inference,[],[118,170,311,294,108,604,174,143,549,444,57,54,65,67,62,71,70,35,33])).
% 1.53/1.66 cnf(623,plain,
% 1.53/1.66 (P2(f3(x6231,f3(x6232,x6233,a2,x6234),x6235,x6235),x6233,f3(x6236,a1,x6237,x6237),x6234)),
% 1.53/1.66 inference(scs_inference,[],[261,302,118,197,170,36,311,294,108,604,451,171,174,143,549,444,610,570,57,54,65,67,62,71,70,35,33,32,31,29,3,34])).
% 1.53/1.66 cnf(639,plain,
% 1.53/1.66 (~P1(x6391,f3(x6392,x6391,a1,f3(x6393,a11,x6394,x6394)),x6391)),
% 1.53/1.66 inference(scs_inference,[],[229,54])).
% 1.53/1.66 cnf(649,plain,
% 1.53/1.66 (P2(f3(x6491,x6492,x6493,x6493),x6494,x6494,x6492)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(658,plain,
% 1.53/1.66 (~P2(x6581,x6581,f3(x6582,a11,x6583,x6583),f3(x6584,a1,x6585,x6585))),
% 1.53/1.66 inference(rename_variables,[],[216])).
% 1.53/1.66 cnf(662,plain,
% 1.53/1.66 (P2(f3(x6621,x6622,x6623,x6623),x6622,f3(x6624,a1,x6625,x6625),f3(x6626,a1,x6627,x6627))),
% 1.53/1.66 inference(scs_inference,[],[216,658,170,229,112,649,46,346,219,498,623,553,54,57,64,62,71,70,35,33,32,34])).
% 1.53/1.66 cnf(667,plain,
% 1.53/1.66 (P1(x6671,f3(x6672,a1,x6673,x6673),f3(f3(x6674,x6671,x6675,x6675),a2,x6676,x6677))),
% 1.53/1.66 inference(scs_inference,[],[261,91,216,658,170,145,229,112,649,46,346,451,219,498,623,553,594,54,57,64,62,71,70,35,33,32,34,31,3,30])).
% 1.53/1.66 cnf(737,plain,
% 1.53/1.66 (~P1(f3(f3(a11,a1,a11,a1),a1,f3(a11,a1,a11,a1),a1),a1,f3(f3(a11,a1,a11,a1),a1,f3(a11,a1,a11,a1),a1))),
% 1.53/1.66 inference(scs_inference,[],[294,54])).
% 1.53/1.66 cnf(741,plain,
% 1.53/1.66 (~P2(x7411,x7411,f3(x7412,x7413,x7414,x7414),f3(x7415,x7413,a11,a1))),
% 1.53/1.66 inference(scs_inference,[],[294,611,54,57,62])).
% 1.53/1.66 cnf(746,plain,
% 1.53/1.66 (P2(f3(x7461,x7462,x7463,x7463),x7464,x7464,x7462)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(755,plain,
% 1.53/1.66 (P2(f3(x7551,x7552,x7553,x7553),f3(x7554,x7552,x7555,x7556),x7555,x7556)),
% 1.53/1.66 inference(rename_variables,[],[549])).
% 1.53/1.66 cnf(756,plain,
% 1.53/1.66 (~P2(x7561,x7561,a1,a11)),
% 1.53/1.66 inference(rename_variables,[],[122])).
% 1.53/1.66 cnf(773,plain,
% 1.53/1.66 (~P2(a2,a1,f3(x7731,a1,x7732,x7732),f3(x7733,a2,a11,a1))),
% 1.53/1.66 inference(scs_inference,[],[201,407,562,667,181,122,756,170,294,611,112,746,494,662,549,755,174,435,337,639,54,57,62,64,71,70,35,33,32,29,30,31,72,5,63])).
% 1.53/1.66 cnf(777,plain,
% 1.53/1.66 (~P2(f3(x7771,a1,x7772,x7772),f3(x7773,a2,a11,a1),a1,a2)),
% 1.53/1.66 inference(scs_inference,[],[201,407,562,667,181,122,756,170,294,611,112,746,494,662,549,755,174,435,337,639,54,57,62,64,71,70,35,33,32,29,30,31,72,5,63,68,66])).
% 1.53/1.66 cnf(795,plain,
% 1.53/1.66 (~P1(f3(x7951,a1,x7952,x7952),f3(x7953,a11,x7954,x7954),f3(x7951,a1,x7952,x7952))),
% 1.53/1.66 inference(scs_inference,[],[187,569,741,773,63,66,57,54])).
% 1.53/1.66 cnf(807,plain,
% 1.53/1.66 (P2(x8071,x8072,f3(x8073,x8072,x8074,x8074),x8071)),
% 1.53/1.66 inference(rename_variables,[],[108])).
% 1.53/1.66 cnf(819,plain,
% 1.53/1.66 (~E(f3(a11,a1,a11,a1),f3(f3(a11,a1,a11,a1),a1,f3(a11,a1,a11,a1),a1))),
% 1.53/1.66 inference(scs_inference,[],[120,136,145,187,108,807,569,99,143,549,288,741,737,773,777,44,63,66,57,54,65,67,64,62,71,70,33,32,3,29])).
% 1.53/1.66 cnf(846,plain,
% 1.53/1.66 (P2(f3(x8461,x8462,x8463,x8463),x8464,x8464,x8462)),
% 1.53/1.66 inference(rename_variables,[],[112])).
% 1.53/1.66 cnf(856,plain,
% 1.53/1.66 (P2(x8561,x8561,x8562,f3(x8563,x8562,x8564,x8564))),
% 1.53/1.66 inference(rename_variables,[],[602])).
% 1.53/1.66 cnf(873,plain,
% 1.53/1.66 ($false),
% 1.53/1.66 inference(scs_inference,[],[819,567,91,181,170,218,112,846,46,451,602,856,441,795,353,239,37,38,54,57,67,64,65,71,70,35,34,32,33,3,29,31,30,61,5,2,56]),
% 1.53/1.66 ['proof']).
% 1.53/1.66 % SZS output end Proof
% 1.53/1.66 % Total time :1.070000s
%------------------------------------------------------------------------------