%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN009-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 07:26:51 EDT 2024
% Result : Unsatisfiable 11.68s 11.77s
% Output : CNFRefutation 11.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : HEN009-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.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sat Jun 22 05:34:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.50/0.57 start to proof:theBenchmark
% 11.68/11.77 %-------------------------------------------
% 11.68/11.77 % File :CSE---1.7
% 11.68/11.77 % Problem :theBenchmark
% 11.68/11.77 % Transform :cnf
% 11.68/11.77 % Format :tptp:raw
% 11.68/11.77 % Command :java -jar mcs_scs.jar %d %s
% 11.68/11.77
% 11.68/11.77 % Result :Theorem 11.160000s
% 11.68/11.77 % Output :CNFRefutation 11.160000s
% 11.68/11.77 %-------------------------------------------
% 11.68/11.77 %--------------------------------------------------------------------------
% 11.68/11.77 % File : HEN009-2 : TPTP v8.2.0. Released v1.0.0.
% 11.68/11.77 % Domain : Henkin Models
% 11.68/11.77 % Problem : Define X' as identity/X. Then X' = X'''
% 11.68/11.77 % Version : [MOW76] axioms : Augmented.
% 11.68/11.77 % English :
% 11.68/11.77
% 11.68/11.77 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 11.68/11.77 % Source : [MOW76]
% 11.68/11.77 % Names : H9 [MOW76]
% 11.68/11.77 % : hp9.ver1.in [ANL]
% 11.68/11.77
% 11.68/11.77 % Status : Unsatisfiable
% 11.68/11.77 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.00 v2.4.0, 0.17 v2.3.0, 0.00 v2.1.0, 0.00 v2.0.0
% 11.68/11.77 % Syntax : Number of clauses : 21 ( 11 unt; 0 nHn; 14 RR)
% 11.68/11.77 % Number of literals : 44 ( 3 equ; 24 neg)
% 11.68/11.77 % Maximal clause size : 6 ( 2 avg)
% 11.68/11.77 % Maximal term depth : 2 ( 1 avg)
% 11.68/11.77 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 11.68/11.77 % Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% 11.68/11.77 % Number of variables : 47 ( 5 sgn)
% 11.68/11.77 % SPC : CNF_UNS_RFO_SEQ_HRN
% 11.68/11.77
% 11.68/11.77 % Comments :
% 11.68/11.77 %--------------------------------------------------------------------------
% 11.68/11.77 %----Include Henkin model axioms
% 11.68/11.77 include('Axioms/HEN001-0.ax').
% 11.68/11.77 %--------------------------------------------------------------------------
% 11.68/11.77 %----McCharen uses these earlier results too. I don't
% 11.68/11.77 cnf(everything_divide_identity_is_zero,axiom,
% 11.68/11.77 quotient(X,identity,zero) ).
% 11.68/11.77
% 11.68/11.77 cnf(zero_divide_anything_is_zero,axiom,
% 11.68/11.77 quotient(zero,X,zero) ).
% 11.68/11.77
% 11.68/11.77 cnf(x_divide_x_is_zero,axiom,
% 11.68/11.77 quotient(X,X,zero) ).
% 11.68/11.77
% 11.68/11.77 cnf(x_divde_zero_is_x,axiom,
% 11.68/11.77 quotient(X,zero,X) ).
% 11.68/11.77
% 11.68/11.77 cnf(transitivity_of_less_equal,axiom,
% 11.68/11.77 ( ~ less_equal(X,Y)
% 11.68/11.77 | ~ less_equal(Y,Z)
% 11.68/11.77 | less_equal(X,Z) ) ).
% 11.68/11.77
% 11.68/11.77 cnf(xQyLEz_implies_xQzLEy,axiom,
% 11.68/11.77 ( ~ quotient(X,Y,W1)
% 11.68/11.77 | ~ less_equal(W1,Z)
% 11.68/11.77 | ~ quotient(X,Z,W2)
% 11.68/11.77 | less_equal(W2,Y) ) ).
% 11.68/11.77
% 11.68/11.77 cnf(xLEy_implies_zQyLEzQx,axiom,
% 11.68/11.77 ( ~ less_equal(X,Y)
% 11.68/11.77 | ~ quotient(Z,Y,W1)
% 11.68/11.77 | ~ quotient(Z,X,W2)
% 11.68/11.77 | less_equal(W1,W2) ) ).
% 11.68/11.77
% 11.68/11.77 cnf(xLEy_implies_xQzLEyQz,axiom,
% 11.68/11.77 ( ~ less_equal(X,Y)
% 11.68/11.77 | ~ quotient(X,Z,W1)
% 11.68/11.77 | ~ quotient(Y,Z,W2)
% 11.68/11.77 | less_equal(W1,W2) ) ).
% 11.68/11.77
% 11.68/11.77 cnf(identity_divide_a,hypothesis,
% 11.68/11.77 quotient(identity,a,idQa) ).
% 11.68/11.77
% 11.68/11.77 cnf(identity_divide_idQa,hypothesis,
% 11.68/11.77 quotient(identity,idQa,idQ_idQa) ).
% 11.68/11.77
% 11.68/11.77 cnf(identity_divide_idQ_idQa,hypothesis,
% 11.68/11.77 quotient(identity,idQ_idQa,idQ__idQ_idQa) ).
% 11.68/11.77
% 11.68/11.77 cnf(prove_one_inversion_equals_three,negated_conjecture,
% 11.68/11.77 idQa != idQ__idQ_idQa ).
% 11.68/11.77
% 11.68/11.77 %--------------------------------------------------------------------------
% 11.68/11.77 %-------------------------------------------
% 11.68/11.77 % Proof found
% 11.68/11.77 % SZS status Theorem for theBenchmark
% 11.68/11.77 % SZS output start Proof
% 11.68/11.77 %ClaNum:31(EqnAxiom:10)
% 11.68/11.77 %VarNum:92(SingletonVarNum:47)
% 11.68/11.77 %MaxLitNum:6
% 11.68/11.77 %MaxfuncDepth:1
% 11.68/11.77 %SharedTerms:10
% 11.68/11.77 %goalClause: 21
% 11.68/11.77 %singleGoalClaCount:1
% 11.68/11.77 [13]P2(a1,a2,a3)
% 11.68/11.77 [14]P2(a1,a3,a4)
% 11.68/11.77 [15]P2(a1,a4,a5)
% 11.68/11.77 [21]~E(a5,a3)
% 11.68/11.77 [11]P1(x111,a1)
% 11.68/11.77 [12]P1(a7,x121)
% 11.68/11.78 [16]P2(x161,a1,a7)
% 11.68/11.78 [17]P2(a7,x171,a7)
% 11.68/11.78 [18]P2(x181,x181,a7)
% 11.68/11.78 [19]P2(x191,a7,x191)
% 11.68/11.78 [20]P2(x201,x202,f6(x201,x202))
% 11.68/11.78 [24]~P1(x241,x242)+P2(x241,x242,a7)
% 11.68/11.78 [25]P1(x251,x252)+~P2(x251,x252,a7)
% 11.68/11.78 [26]P1(x261,x262)+~P2(x262,x263,x261)
% 11.68/11.78 [22]~P1(x222,x221)+~P1(x221,x222)+E(x221,x222)
% 11.68/11.78 [23]~P1(x231,x233)+P1(x231,x232)+~P1(x233,x232)
% 11.68/11.78 [27]~P2(x273,x274,x271)+E(x271,x272)+~P2(x273,x274,x272)
% 11.68/11.78 [28]~P2(x285,x282,x283)+P1(x281,x282)+~P2(x285,x284,x281)+~P1(x283,x284)
% 11.68/11.78 [29]~P2(x295,x293,x292)+P1(x291,x292)+~P2(x295,x294,x291)+~P1(x293,x294)
% 11.68/11.78 [30]~P2(x303,x305,x301)+P1(x301,x302)+~P2(x304,x305,x302)+~P1(x303,x304)
% 11.68/11.78 [31]~P2(x318,x317,x315)+P1(x311,x312)+~P2(x313,x314,x311)+~P2(x315,x316,x312)+~P2(x317,x316,x314)+~P2(x318,x316,x313)
% 11.68/11.78 %EqnAxiom
% 11.68/11.78 [1]E(x11,x11)
% 11.68/11.78 [2]E(x22,x21)+~E(x21,x22)
% 11.68/11.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 11.68/11.78 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 11.68/11.78 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 11.68/11.78 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 11.68/11.78 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 11.68/11.78 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 11.68/11.78 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 11.68/11.78 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 11.68/11.78
% 11.68/11.78 %-------------------------------------------
% 11.68/11.78 cnf(32,plain,
% 11.68/11.78 (P1(x321,x321)),
% 11.68/11.78 inference(scs_inference,[],[18,25])).
% 11.68/11.78 cnf(34,plain,
% 11.68/11.78 (E(a7,f6(x341,x341))),
% 11.68/11.78 inference(scs_inference,[],[18,20,25,27])).
% 11.68/11.78 cnf(35,plain,
% 11.68/11.78 (P2(x351,x352,f6(x351,x352))),
% 11.68/11.78 inference(rename_variables,[],[20])).
% 11.68/11.78 cnf(37,plain,
% 11.68/11.78 (P1(f6(x371,x371),x372)),
% 11.68/11.78 inference(scs_inference,[],[18,20,12,25,27,6])).
% 11.68/11.78 cnf(39,plain,
% 11.68/11.78 (P2(x391,x391,a7)),
% 11.68/11.78 inference(rename_variables,[],[18])).
% 11.68/11.78 cnf(40,plain,
% 11.68/11.78 (P2(x401,f6(a7,a7),x401)),
% 11.68/11.78 inference(scs_inference,[],[18,19,20,12,25,27,6,8,9])).
% 11.68/11.78 cnf(41,plain,
% 11.68/11.78 (P2(x411,x411,f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[18,39,19,20,12,25,27,6,8,9,10])).
% 11.68/11.78 cnf(42,plain,
% 11.68/11.78 (P1(f6(a7,f6(a7,a7)),a7)),
% 11.68/11.78 inference(scs_inference,[],[18,39,19,20,35,12,25,27,6,8,9,10,31])).
% 11.68/11.78 cnf(48,plain,
% 11.68/11.78 (E(f6(a7,a7),a7)),
% 11.68/11.78 inference(scs_inference,[],[18,39,19,20,35,12,25,27,6,8,9,10,31,2])).
% 11.68/11.78 cnf(49,plain,
% 11.68/11.78 (E(f6(a7,f6(a7,a7)),a7)),
% 11.68/11.78 inference(scs_inference,[],[18,39,19,20,35,12,25,27,6,8,9,10,31,2,22])).
% 11.68/11.78 cnf(55,plain,
% 11.68/11.78 (E(a7,f6(a7,f6(a7,a7)))),
% 11.68/11.78 inference(scs_inference,[],[49,2])).
% 11.68/11.78 cnf(56,plain,
% 11.68/11.78 (E(f6(a7,a7),f6(x561,x561))),
% 11.68/11.78 inference(scs_inference,[],[49,41,20,2,27])).
% 11.68/11.78 cnf(59,plain,
% 11.68/11.78 (P2(a7,f6(a7,f6(a7,a7)),f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[49,41,20,2,27,8])).
% 11.68/11.78 cnf(60,plain,
% 11.68/11.78 (P2(x601,x601,f6(a7,a7))),
% 11.68/11.78 inference(rename_variables,[],[41])).
% 11.68/11.78 cnf(61,plain,
% 11.68/11.78 (P2(f6(a7,f6(a7,a7)),f6(a7,a7),a7)),
% 11.68/11.78 inference(scs_inference,[],[49,41,40,20,2,27,8,10])).
% 11.68/11.78 cnf(63,plain,
% 11.68/11.78 (P2(f6(a7,f6(a7,a7)),a7,f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[49,41,60,40,20,2,27,8,10,9])).
% 11.68/11.78 cnf(66,plain,
% 11.68/11.78 (E(f6(a7,f6(a7,a7)),f6(x661,x661))),
% 11.68/11.78 inference(scs_inference,[],[49,34,41,60,40,42,20,2,27,8,10,9,7,3])).
% 11.68/11.78 cnf(69,plain,
% 11.68/11.78 (P2(x691,a7,x691)),
% 11.68/11.78 inference(rename_variables,[],[19])).
% 11.68/11.78 cnf(71,plain,
% 11.68/11.78 (P2(a7,f6(a7,f6(a7,a7)),f6(x711,x711))),
% 11.68/11.78 inference(scs_inference,[],[56,59,63,19,2,27,10])).
% 11.68/11.78 cnf(72,plain,
% 11.68/11.78 (P1(f6(a7,f6(a7,a7)),x721)),
% 11.68/11.78 inference(scs_inference,[],[56,55,59,63,19,12,2,27,10,6])).
% 11.68/11.78 cnf(73,plain,
% 11.68/11.78 (P2(a7,f6(x731,x731),f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[56,66,55,59,63,19,12,2,27,10,6,9])).
% 11.68/11.78 cnf(74,plain,
% 11.68/11.78 (P2(f6(x741,x741),f6(a7,a7),a7)),
% 11.68/11.78 inference(scs_inference,[],[56,66,55,59,61,63,19,12,2,27,10,6,9,8])).
% 11.68/11.78 cnf(75,plain,
% 11.68/11.78 (P1(a4,a2)),
% 11.68/11.78 inference(scs_inference,[],[56,66,55,13,14,32,59,61,63,19,12,2,27,10,6,9,8,28])).
% 11.68/11.78 cnf(78,plain,
% 11.68/11.78 (P1(a3,a5)),
% 11.68/11.78 inference(scs_inference,[],[56,66,55,13,14,15,32,59,61,63,19,12,2,27,10,6,9,8,28,29])).
% 11.68/11.78 cnf(80,plain,
% 11.68/11.78 (P1(f6(a3,a7),a3)),
% 11.68/11.78 inference(scs_inference,[],[56,66,55,13,14,15,32,59,61,63,17,19,69,20,12,2,27,10,6,9,8,28,29,31])).
% 11.68/11.78 cnf(91,plain,
% 11.68/11.78 (E(f6(x911,x911),f6(a7,f6(a7,a7)))),
% 11.68/11.78 inference(scs_inference,[],[66,2])).
% 11.68/11.78 cnf(92,plain,
% 11.68/11.78 (E(a4,f6(a1,a3))),
% 11.68/11.78 inference(scs_inference,[],[66,14,20,2,27])).
% 11.68/11.78 cnf(93,plain,
% 11.68/11.78 (P2(x931,x932,f6(x931,x932))),
% 11.68/11.78 inference(rename_variables,[],[20])).
% 11.68/11.78 cnf(95,plain,
% 11.68/11.78 (P1(f6(a1,a3),a2)),
% 11.68/11.78 inference(scs_inference,[],[66,14,75,20,2,27,6])).
% 11.68/11.78 cnf(96,plain,
% 11.68/11.78 (P2(a1,f6(a1,a3),a5)),
% 11.68/11.78 inference(scs_inference,[],[66,14,15,75,20,2,27,6,9])).
% 11.68/11.78 cnf(97,plain,
% 11.68/11.78 (P2(f6(a7,f6(a7,a7)),f6(x971,x971),f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[55,66,14,15,73,75,20,2,27,6,9,8])).
% 11.68/11.78 cnf(98,plain,
% 11.68/11.78 (P2(x981,a1,f6(a7,f6(a7,a7)))),
% 11.68/11.78 inference(scs_inference,[],[55,66,14,15,16,73,75,20,2,27,6,9,8,10])).
% 11.68/11.78 cnf(99,plain,
% 11.68/11.78 (P1(f6(f6(a3,a7),a3),f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[55,66,14,15,16,73,80,75,40,20,93,2,27,6,9,8,10,28])).
% 11.68/11.78 cnf(101,plain,
% 11.68/11.78 (P2(x1011,x1012,f6(x1011,x1012))),
% 11.68/11.78 inference(rename_variables,[],[20])).
% 11.68/11.78 cnf(103,plain,
% 11.68/11.78 (P1(f6(f6(a3,a7),a3),a7)),
% 11.68/11.78 inference(scs_inference,[],[55,66,14,15,16,18,73,80,75,40,20,93,101,2,27,6,9,8,10,28,29])).
% 11.68/11.78 cnf(104,plain,
% 11.68/11.78 (P2(x1041,x1041,a7)),
% 11.68/11.78 inference(rename_variables,[],[18])).
% 11.68/11.78 cnf(105,plain,
% 11.68/11.78 (P2(x1051,x1052,f6(x1051,x1052))),
% 11.68/11.78 inference(rename_variables,[],[20])).
% 11.68/11.78 cnf(107,plain,
% 11.68/11.78 (P1(a4,f6(a4,a3))),
% 11.68/11.78 inference(scs_inference,[],[55,66,14,15,16,18,104,73,80,75,40,19,20,93,101,105,2,27,6,9,8,10,28,29,31])).
% 11.68/11.78 cnf(117,plain,
% 11.68/11.78 (E(f6(x1171,x1171),a7)),
% 11.68/11.78 inference(scs_inference,[],[34,2])).
% 11.68/11.78 cnf(118,plain,
% 11.68/11.78 (E(a7,f6(x1181,a1))),
% 11.68/11.78 inference(scs_inference,[],[34,16,20,2,27])).
% 11.68/11.78 cnf(119,plain,
% 11.68/11.78 (P2(x1191,x1192,f6(x1191,x1192))),
% 11.68/11.78 inference(rename_variables,[],[20])).
% 11.68/11.78 cnf(122,plain,
% 11.68/11.78 (E(f6(f6(a3,a7),a3),f6(a7,a7))),
% 11.68/11.78 inference(scs_inference,[],[48,34,37,16,74,99,20,2,27,9,22])).
% 11.68/11.78 cnf(125,plain,
% 11.68/11.78 (P2(x1251,a1,f6(x1252,x1252))),
% 11.68/11.78 inference(scs_inference,[],[48,34,37,16,74,99,20,2,27,9,22,10])).
% 11.68/11.78 cnf(126,plain,
% 11.68/11.78 (P2(f6(x1261,x1261),x1262,a7)),
% 11.68/11.79 inference(scs_inference,[],[48,34,37,16,74,17,99,20,2,27,9,22,10,8])).
% 11.68/11.79 cnf(127,plain,
% 11.68/11.79 (P1(f6(a1,a3),f6(a4,a3))),
% 11.68/11.79 inference(scs_inference,[],[48,34,92,37,16,74,17,99,107,20,2,27,9,22,10,8,6])).
% 11.68/11.79 cnf(128,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),a3),f6(x1281,x1281))),
% 11.68/11.79 inference(scs_inference,[],[48,34,92,37,16,74,17,99,103,107,20,2,27,9,22,10,8,6,7])).
% 11.68/11.79 cnf(129,plain,
% 11.68/11.79 (E(f6(a7,a7),f6(x1291,a1))),
% 11.68/11.79 inference(scs_inference,[],[48,34,92,37,16,74,17,99,103,107,20,2,27,9,22,10,8,6,7,3])).
% 11.68/11.79 cnf(130,plain,
% 11.68/11.79 (P1(f6(a1,a5),a2)),
% 11.68/11.79 inference(scs_inference,[],[48,34,92,37,16,13,74,78,17,99,103,107,20,119,2,27,9,22,10,8,6,7,3,28])).
% 11.68/11.79 cnf(131,plain,
% 11.68/11.79 (P2(x1311,x1312,f6(x1311,x1312))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(133,plain,
% 11.68/11.79 (P1(f6(a1,a5),a4)),
% 11.68/11.79 inference(scs_inference,[],[48,34,92,37,16,13,14,74,78,17,99,103,107,20,119,131,2,27,9,22,10,8,6,7,3,28,29])).
% 11.68/11.79 cnf(137,plain,
% 11.68/11.79 (E(a5,f6(a1,a4))),
% 11.68/11.79 inference(scs_inference,[],[122,15,20,2,27])).
% 11.68/11.79 cnf(138,plain,
% 11.68/11.79 (P2(x1381,x1382,f6(x1381,x1382))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(140,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),a3),f6(x1401,x1401))),
% 11.68/11.79 inference(scs_inference,[],[122,37,15,128,20,2,27,22])).
% 11.68/11.79 cnf(144,plain,
% 11.68/11.79 (P2(a7,x1441,f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[55,122,37,15,17,128,20,2,27,22,10])).
% 11.68/11.79 cnf(145,plain,
% 11.68/11.79 (P2(f6(a7,f6(a7,a7)),x1451,a7)),
% 11.68/11.79 inference(scs_inference,[],[55,122,37,15,17,128,20,2,27,22,10,8])).
% 11.68/11.79 cnf(146,plain,
% 11.68/11.79 (P2(a7,f6(x1461,x1461),f6(x1462,x1462))),
% 11.68/11.79 inference(scs_inference,[],[66,55,122,37,15,17,128,71,20,2,27,22,10,8,9])).
% 11.68/11.79 cnf(147,plain,
% 11.68/11.79 (P1(a3,f6(a1,a4))),
% 11.68/11.79 inference(scs_inference,[],[66,55,122,37,15,17,78,128,71,20,2,27,22,10,8,9,7])).
% 11.68/11.79 cnf(148,plain,
% 11.68/11.79 (E(f6(x1481,x1481),f6(x1482,x1482))),
% 11.68/11.79 inference(scs_inference,[],[66,55,34,122,117,37,15,17,78,128,71,20,2,27,22,10,8,9,7,3])).
% 11.68/11.79 cnf(149,plain,
% 11.68/11.79 (P1(f6(f6(a1,a3),f6(a4,a3)),f6(a7,a7))),
% 11.68/11.79 inference(scs_inference,[],[66,55,34,122,117,37,15,17,78,128,127,71,40,20,138,2,27,22,10,8,9,7,3,28])).
% 11.68/11.79 cnf(151,plain,
% 11.68/11.79 (P2(x1511,x1512,f6(x1511,x1512))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(153,plain,
% 11.68/11.79 (P1(f6(a7,a3),a7)),
% 11.68/11.79 inference(scs_inference,[],[66,55,34,122,117,37,15,17,78,80,128,127,71,40,20,138,151,2,27,22,10,8,9,7,3,28,29])).
% 11.68/11.79 cnf(154,plain,
% 11.68/11.79 (P2(a7,x1541,a7)),
% 11.68/11.79 inference(rename_variables,[],[17])).
% 11.68/11.79 cnf(155,plain,
% 11.68/11.79 (P2(x1551,x1552,f6(x1551,x1552))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(157,plain,
% 11.68/11.79 (P1(f6(a5,a7),a5)),
% 11.68/11.79 inference(scs_inference,[],[66,55,34,122,117,37,15,17,154,78,80,128,127,71,40,19,20,138,151,155,2,27,22,10,8,9,7,3,28,29,31])).
% 11.68/11.79 cnf(162,plain,
% 11.68/11.79 (P1(x1621,a5)+~E(a3,x1621)),
% 11.68/11.79 inference(scs_inference,[],[66,55,34,122,117,37,15,17,154,78,80,128,127,71,40,19,20,138,151,155,2,27,22,10,8,9,7,3,28,29,31,6])).
% 11.68/11.79 cnf(167,plain,
% 11.68/11.79 (E(f6(x1671,x1671),f6(f6(a3,a7),a3))),
% 11.68/11.79 inference(scs_inference,[],[140,2])).
% 11.68/11.79 cnf(168,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),a3),a7)),
% 11.68/11.79 inference(scs_inference,[],[140,12,103,2,22])).
% 11.68/11.79 cnf(171,plain,
% 11.68/11.79 (P2(x1711,x1711,f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[55,140,12,18,103,2,22,10])).
% 11.68/11.79 cnf(172,plain,
% 11.68/11.79 (P2(f6(x1721,x1721),f6(x1722,x1722),f6(a7,a7))),
% 11.68/11.79 inference(scs_inference,[],[66,55,140,12,18,103,97,2,22,10,8])).
% 11.68/11.79 cnf(173,plain,
% 11.68/11.79 (P2(x1731,f6(x1732,x1732),x1731)),
% 11.68/11.79 inference(scs_inference,[],[66,55,148,140,12,18,103,97,40,2,22,10,8,9])).
% 11.68/11.79 cnf(175,plain,
% 11.68/11.79 (P1(f6(a1,a5),f6(a1,a3))),
% 11.68/11.79 inference(scs_inference,[],[66,55,148,140,92,12,133,18,103,97,40,2,22,10,8,9,7])).
% 11.68/11.79 cnf(176,plain,
% 11.68/11.79 (E(f6(a7,f6(a7,a7)),f6(x1761,a1))),
% 11.68/11.79 inference(scs_inference,[],[66,55,148,140,129,92,12,133,18,103,97,40,2,22,10,8,9,7,3])).
% 11.68/11.79 cnf(178,plain,
% 11.68/11.79 (P1(f6(f6(a1,a3),a2),f6(a7,a7))),
% 11.68/11.79 inference(scs_inference,[],[66,55,148,140,129,92,12,95,133,18,103,97,40,20,2,22,10,8,9,7,3,28])).
% 11.68/11.79 cnf(180,plain,
% 11.68/11.79 (P2(x1801,x1802,f6(x1801,x1802))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(182,plain,
% 11.68/11.79 (P1(f6(a4,a2),a7)),
% 11.68/11.79 inference(scs_inference,[],[66,55,148,140,129,92,12,75,95,133,18,103,97,40,20,180,2,22,10,8,9,7,3,28,29])).
% 11.68/11.79 cnf(189,plain,
% 11.68/11.79 (E(f6(f6(a1,a3),f6(a4,a3)),f6(a7,a7))),
% 11.68/11.79 inference(scs_inference,[],[176,37,149,2,22])).
% 11.68/11.79 cnf(193,plain,
% 11.68/11.79 (P2(x1931,f6(a7,f6(a7,a7)),x1931)),
% 11.68/11.79 inference(scs_inference,[],[55,176,37,146,19,149,2,22,8,9])).
% 11.68/11.79 cnf(194,plain,
% 11.68/11.79 (P2(f6(x1941,x1941),x1942,f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[55,176,37,126,146,19,149,2,22,8,9,10])).
% 11.68/11.79 cnf(195,plain,
% 11.68/11.79 (P1(f6(a5,a7),f6(a1,a4))),
% 11.68/11.79 inference(scs_inference,[],[55,176,137,37,126,146,157,19,149,2,22,8,9,10,7])).
% 11.68/11.79 cnf(196,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),a3),f6(x1961,a1))),
% 11.68/11.79 inference(scs_inference,[],[55,176,168,118,137,37,126,146,157,19,149,2,22,8,9,10,7,3])).
% 11.68/11.79 cnf(197,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),a2),a7)),
% 11.68/11.79 inference(scs_inference,[],[55,176,168,118,137,37,130,126,146,157,19,149,20,2,22,8,9,10,7,3,28])).
% 11.68/11.79 cnf(199,plain,
% 11.68/11.79 (P2(x1991,x1992,f6(x1991,x1992))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(201,plain,
% 11.68/11.79 (P1(f6(f6(x2011,x2011),a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[55,176,168,118,137,78,37,130,126,146,157,19,149,20,199,2,22,8,9,10,7,3,28,29])).
% 11.68/11.79 cnf(210,plain,
% 11.68/11.79 (E(f6(a7,a7),f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[189,2])).
% 11.68/11.79 cnf(211,plain,
% 11.68/11.79 (P1(f6(a3,a7),a5)),
% 11.68/11.79 inference(scs_inference,[],[189,78,80,2,23])).
% 11.68/11.79 cnf(218,plain,
% 11.68/11.79 (P2(a7,x2181,f6(x2182,x2182))),
% 11.68/11.79 inference(scs_inference,[],[34,91,189,78,80,17,37,172,178,2,23,22,9,10])).
% 11.68/11.79 cnf(219,plain,
% 11.68/11.79 (P2(f6(x2191,x2191),f6(x2192,x2192),f6(x2193,x2193))),
% 11.68/11.79 inference(scs_inference,[],[34,91,189,78,80,17,37,146,172,178,2,23,22,9,10,8])).
% 11.68/11.79 cnf(220,plain,
% 11.68/11.79 (P1(f6(f6(x2201,x2201),a5),f6(x2202,x2202))),
% 11.68/11.79 inference(scs_inference,[],[34,91,189,78,80,17,37,146,172,178,201,2,23,22,9,10,8,7])).
% 11.68/11.79 cnf(221,plain,
% 11.68/11.79 (P1(f6(x2211,a1),f6(x2212,x2212))),
% 11.68/11.79 inference(scs_inference,[],[34,91,189,196,78,80,17,37,146,172,128,178,201,2,23,22,9,10,8,7,6])).
% 11.68/11.79 cnf(222,plain,
% 11.68/11.79 (E(f6(x2221,x2221),f6(x2222,a1))),
% 11.68/11.79 inference(scs_inference,[],[34,91,167,189,196,78,80,17,37,146,172,128,178,201,2,23,22,9,10,8,7,6,3])).
% 11.68/11.79 cnf(223,plain,
% 11.68/11.79 (P1(f6(f6(a1,a3),a2),f6(x2231,x2231))),
% 11.68/11.79 inference(scs_inference,[],[34,91,167,189,196,78,80,17,95,37,173,146,172,128,178,201,20,2,23,22,9,10,8,7,6,3,28])).
% 11.68/11.79 cnf(228,plain,
% 11.68/11.79 (P1(f6(a1,a5),f6(a4,a3))),
% 11.68/11.79 inference(scs_inference,[],[222,133,107,2,23])).
% 11.68/11.79 cnf(230,plain,
% 11.68/11.79 (E(f6(f6(a1,a3),a2),f6(x2301,x2301))),
% 11.68/11.79 inference(scs_inference,[],[222,133,107,37,223,2,23,22])).
% 11.68/11.79 cnf(232,plain,
% 11.68/11.79 (P1(f6(x2321,x2321),x2322)),
% 11.68/11.79 inference(rename_variables,[],[37])).
% 11.68/11.79 cnf(235,plain,
% 11.68/11.79 (P2(x2351,f6(x2352,x2352),x2351)),
% 11.68/11.79 inference(rename_variables,[],[173])).
% 11.68/11.79 cnf(237,plain,
% 11.68/11.79 (P2(x2371,a1,f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[66,210,222,125,133,107,37,173,63,223,2,23,22,9,8,10])).
% 11.68/11.79 cnf(239,plain,
% 11.68/11.79 (P1(f6(x2391,a1),f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[66,210,222,125,133,107,37,173,63,223,221,2,23,22,9,8,10,7])).
% 11.68/11.79 cnf(241,plain,
% 11.68/11.79 (P1(f6(f6(a1,a3),f6(a4,a3)),x2411)),
% 11.68/11.79 inference(scs_inference,[],[66,210,222,125,133,107,37,232,173,63,223,221,2,23,22,9,8,10,7,6])).
% 11.68/11.79 cnf(243,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),a4),f6(x2431,x2431))),
% 11.68/11.79 inference(scs_inference,[],[66,210,222,125,133,107,37,232,173,235,63,223,221,20,2,23,22,9,8,10,7,6,28])).
% 11.68/11.79 cnf(247,plain,
% 11.68/11.79 (E(a7,f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[66,210,222,16,125,133,107,37,232,173,235,63,223,221,20,2,23,22,9,8,10,7,6,28,27])).
% 11.68/11.79 cnf(252,plain,
% 11.68/11.79 (E(f6(x2521,x2521),f6(f6(a1,a3),a2))),
% 11.68/11.79 inference(scs_inference,[],[230,2])).
% 11.68/11.79 cnf(253,plain,
% 11.68/11.79 (P1(f6(a3,a7),f6(a1,a4))),
% 11.68/11.79 inference(scs_inference,[],[230,80,147,2,23])).
% 11.68/11.79 cnf(260,plain,
% 11.68/11.79 (P2(f6(a7,f6(a7,a7)),x2601,f6(x2602,x2602))),
% 11.68/11.79 inference(scs_inference,[],[55,230,137,80,96,147,37,220,218,2,23,22,10,8])).
% 11.68/11.79 cnf(261,plain,
% 11.68/11.79 (P1(f6(a7,a3),f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[55,230,137,80,96,147,37,220,218,153,2,23,22,10,8,7])).
% 11.68/11.79 cnf(262,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),a2),f6(x2621,x2621))),
% 11.68/11.79 inference(scs_inference,[],[55,230,137,80,130,96,147,37,173,220,218,153,20,2,23,22,10,8,7,28])).
% 11.68/11.79 cnf(268,plain,
% 11.68/11.79 (E(x2681,f6(a1,a4))+~E(x2681,a5)),
% 11.68/11.79 inference(scs_inference,[],[55,230,137,16,80,127,130,96,147,37,173,220,218,153,20,2,23,22,10,8,7,28,9,6,3])).
% 11.68/11.79 cnf(281,plain,
% 11.68/11.79 (P1(f6(f6(a1,a3),a2),a7)),
% 11.68/11.79 inference(scs_inference,[],[34,168,117,18,12,218,219,241,223,2,22,9,10,8,7])).
% 11.68/11.79 cnf(283,plain,
% 11.68/11.79 (P1(f6(a1,f6(a4,a3)),a3)),
% 11.68/11.79 inference(scs_inference,[],[34,168,117,18,14,107,12,218,219,241,223,20,2,22,9,10,8,7,28])).
% 11.68/11.79 cnf(292,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),a2),f6(x2921,x2921))),
% 11.68/11.79 inference(scs_inference,[],[118,37,262,2,22])).
% 11.68/11.79 cnf(296,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),a4),a7)),
% 11.68/11.79 inference(scs_inference,[],[118,117,37,262,243,2,22,7])).
% 11.68/11.79 cnf(310,plain,
% 11.68/11.79 (E(f6(x3101,a1),f6(f6(a3,a7),a3))),
% 11.68/11.79 inference(scs_inference,[],[196,2])).
% 11.68/11.79 cnf(311,plain,
% 11.68/11.79 (E(f6(x3111,a1),f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[196,241,239,2,22])).
% 11.68/11.79 cnf(316,plain,
% 11.68/11.79 (E(f6(x3161,x3161),f6(f6(a1,a3),f6(a4,a3)))),
% 11.68/11.79 inference(scs_inference,[],[117,196,247,241,239,221,2,22,7,3])).
% 11.68/11.79 cnf(317,plain,
% 11.68/11.79 (P1(f6(f6(a5,a7),a5),f6(x3171,x3171))),
% 11.68/11.79 inference(scs_inference,[],[117,196,247,173,157,241,239,221,20,2,22,7,3,28])).
% 11.68/11.79 cnf(334,plain,
% 11.68/11.79 (P1(f6(f6(a5,a7),a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[117,316,12,201,317,2,22,7])).
% 11.68/11.79 cnf(337,plain,
% 11.68/11.79 (P1(f6(a4,f6(a4,a3)),a7)),
% 11.68/11.79 inference(scs_inference,[],[117,196,316,310,19,107,12,201,317,20,2,22,7,3,28])).
% 11.68/11.79 cnf(354,plain,
% 11.68/11.79 (E(f6(f6(a1,a3),a2),a7)),
% 11.68/11.79 inference(scs_inference,[],[292,12,281,2,22])).
% 11.68/11.79 cnf(374,plain,
% 11.68/11.79 (E(f6(a7,f6(a7,a7)),f6(a7,x3741))),
% 11.68/11.79 inference(scs_inference,[],[311,144,20,2,27])).
% 11.68/11.79 cnf(375,plain,
% 11.68/11.79 (P2(x3751,x3752,f6(x3751,x3752))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(377,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),a2),a7)),
% 11.68/11.79 inference(scs_inference,[],[311,144,12,197,20,2,27,22])).
% 11.68/11.79 cnf(381,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),f6(a1,a3)),a7)),
% 11.68/11.79 inference(scs_inference,[],[34,311,144,19,12,197,175,182,20,375,2,27,22,7,28])).
% 11.68/11.79 cnf(396,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),a4),f6(x3961,x3961))),
% 11.68/11.79 inference(scs_inference,[],[354,37,243,2,22])).
% 11.68/11.79 cnf(400,plain,
% 11.68/11.79 (P1(f6(a4,f6(a4,a3)),f6(x4001,x4001))),
% 11.68/11.79 inference(scs_inference,[],[34,354,37,243,337,2,22,7])).
% 11.68/11.79 cnf(401,plain,
% 11.68/11.79 (P1(f6(a3,a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[34,354,18,78,37,243,337,20,2,22,7,29])).
% 11.68/11.79 cnf(403,plain,
% 11.68/11.79 (P2(x4031,x4032,f6(x4031,x4032))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(405,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),a5),f6(x4051,x4051))),
% 11.68/11.79 inference(scs_inference,[],[34,354,18,173,78,37,211,243,337,20,403,2,22,7,29,28])).
% 11.68/11.79 cnf(420,plain,
% 11.68/11.79 (E(a7,f6(a7,x4201))),
% 11.68/11.79 inference(scs_inference,[],[377,17,20,2,27])).
% 11.68/11.79 cnf(421,plain,
% 11.68/11.79 (P2(x4211,x4212,f6(x4211,x4212))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(423,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),a4),a7)),
% 11.68/11.79 inference(scs_inference,[],[377,17,12,296,20,2,27,22])).
% 11.68/11.79 cnf(426,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[117,377,17,12,296,405,20,2,27,22,7])).
% 11.68/11.79 cnf(429,plain,
% 11.68/11.79 (P1(f6(f6(a5,a7),f6(a1,a4)),a7)),
% 11.68/11.79 inference(scs_inference,[],[117,377,17,19,12,195,296,405,20,421,2,27,22,7,3,28])).
% 11.68/11.79 cnf(442,plain,
% 11.68/11.79 (P1(f6(f6(a5,a7),f6(a1,a4)),f6(x4421,x4421))),
% 11.68/11.79 inference(scs_inference,[],[34,396,12,334,429,2,22,7])).
% 11.68/11.79 cnf(443,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),f6(a1,a4)),f6(x4431,x4431))),
% 11.68/11.79 inference(scs_inference,[],[34,396,173,12,253,334,429,20,2,22,7,28])).
% 11.68/11.79 cnf(462,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),f6(a1,a4)),a7)),
% 11.68/11.79 inference(scs_inference,[],[117,423,37,317,443,2,22,7])).
% 11.68/11.79 cnf(464,plain,
% 11.68/11.79 (P1(f6(a4,a2),f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[117,423,193,19,37,317,182,443,2,22,7,28])).
% 11.68/11.79 cnf(469,plain,
% 11.68/11.79 (P1(x4691,f6(a1,a4))+~E(a3,x4691)),
% 11.68/11.79 inference(scs_inference,[],[117,423,237,193,19,147,37,317,182,443,2,22,7,28,9,6])).
% 11.68/11.79 cnf(478,plain,
% 11.68/11.79 (P1(f6(a3,a5),f6(x4781,x4781))),
% 11.68/11.79 inference(scs_inference,[],[34,420,12,337,401,2,22,7])).
% 11.68/11.79 cnf(479,plain,
% 11.68/11.79 (P1(f6(f6(a1,a5),f6(a4,a3)),f6(x4791,x4791))),
% 11.68/11.79 inference(scs_inference,[],[34,420,173,12,20,228,337,401,2,22,7,28])).
% 11.68/11.79 cnf(510,plain,
% 11.68/11.79 (E(f6(a4,a2),f6(a7,f6(a7,a7)))),
% 11.68/11.79 inference(scs_inference,[],[374,72,464,2,22])).
% 11.68/11.79 cnf(511,plain,
% 11.68/11.79 (P1(f6(a7,f6(a7,a7)),x5111)),
% 11.68/11.79 inference(rename_variables,[],[72])).
% 11.68/11.79 cnf(515,plain,
% 11.68/11.79 (P2(x5151,f6(x5152,a1),x5151)),
% 11.68/11.79 inference(scs_inference,[],[176,374,145,144,193,72,464,2,22,8,10,9])).
% 11.68/11.79 cnf(517,plain,
% 11.68/11.79 (P1(f6(x5171,a1),x5172)),
% 11.68/11.79 inference(scs_inference,[],[176,374,145,144,193,72,511,261,464,2,22,8,10,9,7,6])).
% 11.68/11.79 cnf(530,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),f6(a1,a3)),a7)),
% 11.68/11.79 inference(scs_inference,[],[510,12,381,2,22])).
% 11.68/11.79 cnf(538,plain,
% 11.68/11.79 (E(a7,f6(a4,a2))),
% 11.68/11.79 inference(scs_inference,[],[34,176,420,510,98,260,12,20,464,381,2,22,8,10,9,7,3])).
% 11.68/11.79 cnf(542,plain,
% 11.68/11.79 (E(a7,f6(f6(a1,a5),f6(a1,a3)))),
% 11.68/11.79 inference(scs_inference,[],[530,2])).
% 11.68/11.79 cnf(546,plain,
% 11.68/11.79 (P2(f6(x5461,x5461),x5462,f6(a7,x5462))),
% 11.68/11.79 inference(scs_inference,[],[34,530,12,20,462,2,22,8])).
% 11.68/11.79 cnf(549,plain,
% 11.68/11.79 (E(f6(x5491,x5491),f6(a4,a2))),
% 11.68/11.79 inference(scs_inference,[],[34,176,117,530,538,194,12,20,462,2,22,8,10,3])).
% 11.68/11.79 cnf(557,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[549,12,426,2,22])).
% 11.68/11.79 cnf(561,plain,
% 11.68/11.79 (E(f6(x5611,x5611),f6(f6(a1,a5),f6(a1,a3)))),
% 11.68/11.79 inference(scs_inference,[],[176,117,549,542,171,12,426,2,22,10,3])).
% 11.68/11.79 cnf(572,plain,
% 11.68/11.79 (P2(f6(a3,a7),a3,f6(x5721,x5721))),
% 11.68/11.79 inference(scs_inference,[],[140,561,429,20,12,2,22,10])).
% 11.68/11.79 cnf(575,plain,
% 11.68/11.79 (P2(f6(a3,a7),x5751,f6(x5752,x5752))+~E(a3,x5751)),
% 11.68/11.79 inference(scs_inference,[],[140,561,429,20,12,2,22,10,8,9])).
% 11.68/11.79 cnf(585,plain,
% 11.68/11.79 (E(f6(a3,a5),a7)),
% 11.68/11.79 inference(scs_inference,[],[557,401,12,2,22])).
% 11.68/11.79 cnf(592,plain,
% 11.68/11.79 (P2(f6(a3,a7),x5921,a7)+~E(a3,x5921)),
% 11.68/11.79 inference(scs_inference,[],[117,557,401,12,572,2,22,10,3,8,9])).
% 11.68/11.79 cnf(625,plain,
% 11.68/11.79 (E(f6(a4,f6(a4,a3)),f6(x6251,x6251))),
% 11.68/11.79 inference(scs_inference,[],[585,37,400,2,22])).
% 11.68/11.79 cnf(648,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),f6(a1,a4)),f6(x6481,x6481))),
% 11.68/11.79 inference(scs_inference,[],[625,37,443,2,22])).
% 11.68/11.79 cnf(664,plain,
% 11.68/11.79 (E(f6(f6(a5,a7),f6(a1,a4)),f6(x6641,x6641))),
% 11.68/11.79 inference(scs_inference,[],[648,37,442,2,22])).
% 11.68/11.79 cnf(678,plain,
% 11.68/11.79 (E(f6(f6(a1,a5),f6(a4,a3)),f6(x6781,x6781))),
% 11.68/11.79 inference(scs_inference,[],[664,37,479,2,22])).
% 11.68/11.79 cnf(699,plain,
% 11.68/11.79 (P2(f6(a3,a7),x6991,f6(f6(a1,a3),a2))+~E(a3,x6991)),
% 11.68/11.79 inference(scs_inference,[],[252,34,678,103,478,37,572,12,2,23,22,10,3,9])).
% 11.68/11.79 cnf(846,plain,
% 11.68/11.79 (E(f6(a1,a3),a4)),
% 11.68/11.79 inference(scs_inference,[],[92,2])).
% 11.68/11.79 cnf(900,plain,
% 11.68/11.79 (P1(f6(a3,f6(a1,a4)),f6(x9001,x9001))),
% 11.68/11.79 inference(scs_inference,[],[147,173,20,28])).
% 11.68/11.79 cnf(915,plain,
% 11.68/11.79 (P1(f6(a1,f6(a4,a3)),x9151)+~E(a3,x9151)),
% 11.68/11.79 inference(scs_inference,[],[283,37,900,22,2,7])).
% 11.68/11.79 cnf(917,plain,
% 11.68/11.79 (P1(x9171,x9172)+~E(a3,x9172)+~E(f6(a1,f6(a4,a3)),x9171)),
% 11.68/11.79 inference(scs_inference,[],[34,283,37,900,22,2,7,3,6])).
% 11.68/11.79 cnf(998,plain,
% 11.68/11.79 (E(a3,f6(a1,a2))),
% 11.68/11.79 inference(scs_inference,[],[13,20,27])).
% 11.68/11.79 cnf(999,plain,
% 11.68/11.79 (P2(x9991,x9992,f6(x9991,x9992))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(1004,plain,
% 11.68/11.79 (P1(f6(a1,a2),a5)),
% 11.68/11.79 inference(scs_inference,[],[13,92,78,80,14,20,27,9,10,7,6])).
% 11.68/11.79 cnf(1005,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),f6(a1,a2)),f6(x10051,x10051))),
% 11.68/11.79 inference(scs_inference,[],[13,92,78,80,14,173,20,999,27,9,10,7,6,28])).
% 11.68/11.79 cnf(1007,plain,
% 11.68/11.79 (P2(x10071,x10072,f6(x10071,x10072))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(1009,plain,
% 11.68/11.79 (P1(a3,f6(a3,a2))),
% 11.68/11.79 inference(scs_inference,[],[13,92,18,78,80,14,173,19,20,999,1007,27,9,10,7,6,28,31])).
% 11.68/11.79 cnf(1014,plain,
% 11.68/11.79 (P1(f6(a1,a2),f6(a1,a4))),
% 11.68/11.79 inference(scs_inference,[],[13,92,18,78,80,14,173,19,20,999,1007,27,9,10,7,6,28,31,469])).
% 11.68/11.79 cnf(1019,plain,
% 11.68/11.79 (E(f6(a1,a2),a3)),
% 11.68/11.79 inference(scs_inference,[],[13,92,18,78,80,14,173,19,20,999,1007,27,9,10,7,6,28,31,469,915,575,592,699,2])).
% 11.68/11.79 cnf(1021,plain,
% 11.68/11.79 (P1(f6(a3,a7),f6(a3,a2))),
% 11.68/11.79 inference(scs_inference,[],[13,92,18,78,80,14,173,19,20,999,1007,27,9,10,7,6,28,31,469,915,575,592,699,2,917,23])).
% 11.68/11.79 cnf(1036,plain,
% 11.68/11.79 (P1(f6(a1,a2),f6(a3,a2))),
% 11.68/11.79 inference(scs_inference,[],[21,1019,998,37,1005,1009,22,3,6])).
% 11.68/11.79 cnf(1037,plain,
% 11.68/11.79 (P1(f6(f6(a1,a2),f6(a1,a4)),f6(x10371,x10371))),
% 11.68/11.79 inference(scs_inference,[],[21,1019,998,173,20,37,1014,1005,1009,22,3,6,28])).
% 11.68/11.79 cnf(1038,plain,
% 11.68/11.79 (P2(x10381,f6(x10382,x10382),x10381)),
% 11.68/11.79 inference(rename_variables,[],[173])).
% 11.68/11.79 cnf(1039,plain,
% 11.68/11.79 (P2(x10391,x10392,f6(x10391,x10392))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(1041,plain,
% 11.68/11.79 (P1(f6(a3,f6(a7,a2)),a3)),
% 11.68/11.79 inference(scs_inference,[],[13,21,1019,998,173,1038,546,20,1039,37,1014,1005,1009,22,3,6,28,31])).
% 11.68/11.79 cnf(1046,plain,
% 11.68/11.79 (E(f6(x10461,x10461),f6(f6(a3,a7),f6(a1,a2)))),
% 11.68/11.79 inference(scs_inference,[],[13,21,1019,998,173,1038,546,20,1039,37,1014,1005,1009,22,3,6,28,31,2])).
% 11.68/11.79 cnf(1061,plain,
% 11.68/11.79 (E(a7,f6(f6(a3,a7),f6(a1,a2)))),
% 11.68/11.79 inference(scs_inference,[],[34,1046,37,1037,22,3])).
% 11.68/11.79 cnf(1063,plain,
% 11.68/11.79 (P1(f6(f6(a1,a2),a5),f6(x10631,x10631))),
% 11.68/11.79 inference(scs_inference,[],[34,1046,173,20,37,1004,1037,22,3,28])).
% 11.68/11.79 cnf(1067,plain,
% 11.68/11.79 (E(f6(x10671,x10671),f6(f6(a1,a2),f6(a1,a4)))),
% 11.68/11.79 inference(scs_inference,[],[34,1046,173,20,37,1004,1037,22,3,28,2])).
% 11.68/11.79 cnf(1083,plain,
% 11.68/11.79 (E(f6(f6(a1,a2),a5),f6(x10831,x10831))),
% 11.68/11.79 inference(scs_inference,[],[1061,37,1063,2,22])).
% 11.68/11.79 cnf(1087,plain,
% 11.68/11.79 (E(a7,f6(f6(a1,a2),f6(a1,a4)))),
% 11.68/11.79 inference(scs_inference,[],[34,1067,1061,37,1063,2,22,3])).
% 11.68/11.79 cnf(1107,plain,
% 11.68/11.79 (E(a7,f6(f6(a1,a2),a5))),
% 11.68/11.79 inference(scs_inference,[],[34,1083,2,3])).
% 11.68/11.79 cnf(1108,plain,
% 11.68/11.79 (P1(f6(f6(a1,a2),f6(a3,a2)),f6(x11081,x11081))),
% 11.68/11.79 inference(scs_inference,[],[34,1083,173,20,1036,2,3,28])).
% 11.68/11.79 cnf(1127,plain,
% 11.68/11.79 (E(f6(f6(a1,a2),f6(a3,a2)),f6(x11271,x11271))),
% 11.68/11.79 inference(scs_inference,[],[1087,37,1108,2,22])).
% 11.68/11.79 cnf(1131,plain,
% 11.68/11.79 (P1(f6(f6(a5,a7),a5),f6(x11311,a1))),
% 11.68/11.79 inference(scs_inference,[],[1087,157,515,20,37,1108,2,22,28])).
% 11.68/11.79 cnf(1149,plain,
% 11.68/11.79 (P1(f6(f6(a3,a7),f6(a3,a2)),f6(x11491,x11491))),
% 11.68/11.79 inference(scs_inference,[],[34,1127,173,20,517,1021,1131,2,22,3,28])).
% 11.68/11.79 cnf(1165,plain,
% 11.68/11.79 (E(f6(f6(a3,a7),f6(a3,a2)),f6(x11651,x11651))),
% 11.68/11.79 inference(scs_inference,[],[1107,37,1149,2,22])).
% 11.68/11.79 cnf(1234,plain,
% 11.68/11.79 (E(a7,f6(f6(a3,a7),f6(a3,a2)))),
% 11.68/11.79 inference(scs_inference,[],[34,1165,2,3])).
% 11.68/11.79 cnf(1270,plain,
% 11.68/11.79 (P2(x12701,x12701,a7)),
% 11.68/11.79 inference(rename_variables,[],[18])).
% 11.68/11.79 cnf(1275,plain,
% 11.68/11.79 (P1(a3,f6(a1,a2))),
% 11.68/11.79 inference(scs_inference,[],[998,1234,18,1270,173,32,2,9,10,8,7])).
% 11.68/11.79 cnf(2144,plain,
% 11.68/11.79 (P2(x21441,f6(x21442,x21442),x21441)),
% 11.68/11.79 inference(rename_variables,[],[173])).
% 11.68/11.79 cnf(2146,plain,
% 11.68/11.79 (P2(x21461,x21461,a7)),
% 11.68/11.79 inference(rename_variables,[],[18])).
% 11.68/11.79 cnf(2152,plain,
% 11.68/11.79 (P1(x21521,x21521)),
% 11.68/11.79 inference(rename_variables,[],[32])).
% 11.68/11.79 cnf(2154,plain,
% 11.68/11.79 (P1(x21541,x21541)),
% 11.68/11.79 inference(rename_variables,[],[32])).
% 11.68/11.79 cnf(2156,plain,
% 11.68/11.79 (P2(x21561,x21562,f6(x21561,x21562))),
% 11.68/11.79 inference(rename_variables,[],[20])).
% 11.68/11.79 cnf(2170,plain,
% 11.68/11.79 ($false),
% 11.68/11.79 inference(scs_inference,[],[14,21,846,1041,15,126,18,2146,173,2144,20,2156,32,2152,2154,1275,78,10,8,23,9,6,7,29,28,31,22,268,162,2]),
% 11.68/11.79 ['proof']).
% 11.68/11.79 % SZS output end Proof
% 11.68/11.79 % Total time :11.160000s
%------------------------------------------------------------------------------