%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN010-6 : 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 : 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:53 EDT 2024
% Result : Unsatisfiable 7.81s 7.87s
% Output : CNFRefutation 7.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HEN010-6 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n019.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Sat Jun 22 05:33:39 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.49/0.56 start to proof:theBenchmark
% 7.81/7.87 %-------------------------------------------
% 7.81/7.87 % File :CSE---1.7
% 7.81/7.87 % Problem :theBenchmark
% 7.81/7.87 % Transform :cnf
% 7.81/7.87 % Format :tptp:raw
% 7.81/7.87 % Command :java -jar mcs_scs.jar %d %s
% 7.81/7.87
% 7.81/7.87 % Result :Theorem 7.270000s
% 7.81/7.87 % Output :CNFRefutation 7.270000s
% 7.81/7.87 %-------------------------------------------
% 7.81/7.87 %--------------------------------------------------------------------------
% 7.81/7.87 % File : HEN010-6 : TPTP v8.2.0. Released v1.0.0.
% 7.81/7.87 % Domain : Henkin Models
% 7.81/7.87 % Problem : Define X' as identity/X. Then X' = X'/(identity/X')
% 7.81/7.87 % Version : [MOW76] axioms : Augmented.
% 7.81/7.87 % English :
% 7.81/7.87
% 7.81/7.87 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 7.81/7.87 % Source : [ANL]
% 7.81/7.87 % Names : hp10.ver2.in [ANL]
% 7.81/7.87
% 7.81/7.87 % Status : Unsatisfiable
% 7.81/7.87 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.25 v5.4.0, 0.27 v5.3.0, 0.33 v5.2.0, 0.12 v5.1.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 7.81/7.87 % Syntax : Number of clauses : 16 ( 10 unt; 0 nHn; 6 RR)
% 7.81/7.87 % Number of literals : 23 ( 9 equ; 8 neg)
% 7.81/7.87 % Maximal clause size : 3 ( 1 avg)
% 7.81/7.87 % Maximal term depth : 4 ( 1 avg)
% 7.81/7.87 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 7.81/7.87 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 7.81/7.87 % Number of variables : 26 ( 5 sgn)
% 7.81/7.87 % SPC : CNF_UNS_RFO_SEQ_HRN
% 7.81/7.87
% 7.81/7.87 % Comments :
% 7.81/7.87 %--------------------------------------------------------------------------
% 7.81/7.87 %----Include Henkin model axioms for equality formulation
% 7.81/7.87 include('Axioms/HEN002-0.ax').
% 7.81/7.87 %--------------------------------------------------------------------------
% 7.81/7.87 cnf(everything_divide_id_is_zero,axiom,
% 7.81/7.87 divide(X,identity) = zero ).
% 7.81/7.87
% 7.81/7.87 cnf(zero_divide_anything_is_zero,axiom,
% 7.81/7.87 divide(zero,X) = zero ).
% 7.81/7.87
% 7.81/7.87 cnf(x_divide_x_is_zero,axiom,
% 7.81/7.87 divide(X,X) = zero ).
% 7.81/7.87
% 7.81/7.87 cnf(x_divide_zero_is_x,axiom,
% 7.81/7.87 divide(a,zero) = a ).
% 7.81/7.87
% 7.81/7.87 cnf(property_of_divide1,axiom,
% 7.81/7.87 ( ~ less_equal(divide(X,Y),Z)
% 7.81/7.87 | less_equal(divide(X,Z),Y) ) ).
% 7.81/7.87
% 7.81/7.87 cnf(property_of_divide2,axiom,
% 7.81/7.87 ( ~ less_equal(X,Y)
% 7.81/7.87 | less_equal(divide(Z,Y),divide(Z,X)) ) ).
% 7.81/7.87
% 7.81/7.87 cnf(property_of_divide3,axiom,
% 7.81/7.87 ( ~ less_equal(X,Y)
% 7.81/7.87 | less_equal(divide(X,Z),divide(Y,Z)) ) ).
% 7.81/7.87
% 7.81/7.87 cnf(one_inversion_equals_three,axiom,
% 7.81/7.87 divide(identity,divide(identity,divide(identity,X))) = divide(identity,X) ).
% 7.81/7.87
% 7.81/7.87 cnf(prove_property_of_inversion,negated_conjecture,
% 7.81/7.87 divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))) ).
% 7.81/7.87
% 7.81/7.87 %--------------------------------------------------------------------------
% 7.81/7.87 %-------------------------------------------
% 7.81/7.87 % Proof found
% 7.81/7.87 % SZS status Theorem for theBenchmark
% 7.81/7.87 % SZS output start Proof
% 7.81/7.87 %ClaNum:23(EqnAxiom:7)
% 7.81/7.87 %VarNum:50(SingletonVarNum:26)
% 7.81/7.87 %MaxLitNum:3
% 7.81/7.87 %MaxfuncDepth:3
% 7.81/7.87 %SharedTerms:9
% 7.81/7.87 %goalClause: 17
% 7.81/7.87 %singleGoalClaCount:1
% 7.81/7.87 [8]E(f3(a1,a2),a1)
% 7.81/7.87 [17]~E(f3(f3(a4,a1),f3(a4,f3(a4,a1))),f3(a4,a1))
% 7.81/7.87 [11]P1(x111,a4)
% 7.81/7.87 [12]P1(a2,x121)
% 7.81/7.87 [9]E(f3(x91,a4),a2)
% 7.81/7.87 [10]E(f3(a2,x101),a2)
% 7.81/7.87 [13]E(f3(x131,x131),a2)
% 7.81/7.87 [15]E(f3(a4,f3(a4,f3(a4,x151))),f3(a4,x151))
% 7.81/7.87 [14]P1(f3(x141,x142),x141)
% 7.81/7.87 [16]P1(f3(f3(x161,x162),f3(x163,x162)),f3(f3(x161,x163),x162))
% 7.81/7.87 [18]~P1(x181,x182)+E(f3(x181,x182),a2)
% 7.81/7.87 [19]P1(x191,x192)+~E(f3(x191,x192),a2)
% 7.81/7.87 [21]~P1(x213,x212)+P1(f3(x211,x212),f3(x211,x213))
% 7.81/7.87 [22]~P1(x221,x223)+P1(f3(x221,x222),f3(x223,x222))
% 7.81/7.87 [23]~P1(f3(x231,x233),x232)+P1(f3(x231,x232),x233)
% 7.81/7.87 [20]~P1(x202,x201)+~P1(x201,x202)+E(x201,x202)
% 7.81/7.87 %EqnAxiom
% 7.81/7.87 [1]E(x11,x11)
% 7.81/7.87 [2]E(x22,x21)+~E(x21,x22)
% 7.81/7.88 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 7.81/7.88 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 7.81/7.88 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 7.81/7.88 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 7.81/7.88 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 7.81/7.88
% 7.81/7.88 %-------------------------------------------
% 7.81/7.88 cnf(24,plain,
% 7.81/7.88 (E(a2,f3(x241,x241))),
% 7.81/7.88 inference(scs_inference,[],[13,2])).
% 7.81/7.88 cnf(25,plain,
% 7.81/7.88 (P1(x251,x251)),
% 7.81/7.88 inference(scs_inference,[],[13,2,19])).
% 7.81/7.88 cnf(27,plain,
% 7.81/7.88 (~P1(f3(a4,a1),f3(f3(a4,a1),f3(a4,f3(a4,a1))))),
% 7.81/7.88 inference(scs_inference,[],[17,14,13,2,19,20])).
% 7.81/7.88 cnf(30,plain,
% 7.81/7.88 (E(f3(a4,f3(a4,f3(a4,a4))),a2)),
% 7.81/7.88 inference(scs_inference,[],[17,14,13,15,2,19,20,3])).
% 7.81/7.88 cnf(33,plain,
% 7.81/7.88 (~E(a2,f3(a4,a1))),
% 7.81/7.88 inference(scs_inference,[],[17,12,14,13,15,2,19,20,3,6])).
% 7.81/7.88 cnf(37,plain,
% 7.81/7.88 (P1(a4,f3(a4,f3(a4,a4)))),
% 7.81/7.88 inference(scs_inference,[],[30,19])).
% 7.81/7.88 cnf(39,plain,
% 7.81/7.88 (E(a2,f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[30,19,2])).
% 7.81/7.88 cnf(40,plain,
% 7.81/7.88 (~P1(f3(a4,a1),a2)),
% 7.81/7.88 inference(scs_inference,[],[30,33,12,19,2,20])).
% 7.81/7.88 cnf(43,plain,
% 7.81/7.88 (E(f3(a4,f3(a4,f3(a4,a4))),f3(x431,x431))),
% 7.81/7.88 inference(scs_inference,[],[24,30,33,12,19,2,20,3])).
% 7.81/7.88 cnf(50,plain,
% 7.81/7.88 (E(f3(x501,x501),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[43,2])).
% 7.81/7.88 cnf(51,plain,
% 7.81/7.88 (E(a4,f3(a4,f3(a4,a4)))),
% 7.81/7.88 inference(scs_inference,[],[43,37,11,2,20])).
% 7.81/7.88 cnf(56,plain,
% 7.81/7.88 (P1(f3(f3(x561,a4),f3(x562,a4)),a2)),
% 7.81/7.88 inference(scs_inference,[],[40,43,37,16,9,11,14,2,20,6,7])).
% 7.81/7.88 cnf(59,plain,
% 7.81/7.88 (~E(a2,a4)),
% 7.81/7.88 inference(scs_inference,[],[40,43,37,16,9,11,14,2,20,6,7,4])).
% 7.81/7.88 cnf(60,plain,
% 7.81/7.88 (E(x601,a1)+~E(x601,f3(a1,a2))),
% 7.81/7.88 inference(scs_inference,[],[40,43,37,16,9,8,11,14,2,20,6,7,4,3])).
% 7.81/7.88 cnf(63,plain,
% 7.81/7.88 (E(f3(a4,f3(a4,a4)),a4)),
% 7.81/7.88 inference(scs_inference,[],[51,2])).
% 7.81/7.88 cnf(64,plain,
% 7.81/7.88 (E(f3(f3(x641,a4),f3(x642,a4)),a2)),
% 7.81/7.88 inference(scs_inference,[],[51,56,12,2,20])).
% 7.81/7.88 cnf(67,plain,
% 7.81/7.88 (E(f3(x671,x671),f3(x672,x672))),
% 7.81/7.88 inference(scs_inference,[],[50,51,43,56,12,2,20,3])).
% 7.81/7.88 cnf(68,plain,
% 7.81/7.88 (P1(f3(f3(x681,a4),f3(x682,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[50,39,51,43,56,12,2,20,3,7])).
% 7.81/7.88 cnf(70,plain,
% 7.81/7.88 (P1(f3(x701,a4),f3(x702,a4))),
% 7.81/7.88 inference(scs_inference,[],[40,50,39,51,43,56,12,2,20,3,7,6,19])).
% 7.81/7.88 cnf(72,plain,
% 7.81/7.88 (E(a2,f3(f3(x721,a4),f3(x722,a4)))),
% 7.81/7.88 inference(scs_inference,[],[64,2])).
% 7.81/7.88 cnf(73,plain,
% 7.81/7.88 (~P1(a4,a2)),
% 7.81/7.88 inference(scs_inference,[],[64,59,11,2,20])).
% 7.81/7.88 cnf(76,plain,
% 7.81/7.88 (P1(f3(x761,a4),f3(x762,x762))),
% 7.81/7.88 inference(scs_inference,[],[67,64,59,70,11,2,20,7])).
% 7.81/7.88 cnf(78,plain,
% 7.81/7.88 (E(f3(x781,x781),f3(x782,x782))),
% 7.81/7.88 inference(rename_variables,[],[67])).
% 7.81/7.88 cnf(79,plain,
% 7.81/7.88 (~E(a2,f3(a4,f3(a4,a4)))),
% 7.81/7.88 inference(scs_inference,[],[67,64,63,59,70,11,2,20,7,3])).
% 7.81/7.88 cnf(80,plain,
% 7.81/7.88 (P1(f3(x801,x801),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[67,78,64,63,59,68,70,11,2,20,7,3,6])).
% 7.81/7.88 cnf(83,plain,
% 7.81/7.88 (E(a2,f3(a2,x831))),
% 7.81/7.88 inference(scs_inference,[],[10,2])).
% 7.81/7.88 cnf(84,plain,
% 7.81/7.88 (E(f3(f3(x841,a4),f3(x841,a4)),f3(f3(x841,x841),a4))),
% 7.81/7.88 inference(scs_inference,[],[10,76,16,2,20])).
% 7.81/7.88 cnf(86,plain,
% 7.81/7.88 (P1(f3(x861,a4),f3(x862,x862))),
% 7.81/7.88 inference(rename_variables,[],[76])).
% 7.81/7.88 cnf(88,plain,
% 7.81/7.88 (E(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x881,a4),f3(x882,a4)))),
% 7.81/7.88 inference(scs_inference,[],[30,72,10,76,16,2,20,3])).
% 7.81/7.88 cnf(89,plain,
% 7.81/7.88 (P1(f3(x891,x891),a2)),
% 7.81/7.88 inference(scs_inference,[],[30,72,10,76,80,16,2,20,3,7])).
% 7.81/7.88 cnf(90,plain,
% 7.81/7.88 (P1(f3(x901,x901),f3(x902,x902))),
% 7.81/7.88 inference(scs_inference,[],[30,72,67,10,76,86,80,16,2,20,3,7,6])).
% 7.81/7.88 cnf(93,plain,
% 7.81/7.88 (E(f3(f3(x931,x931),a4),f3(f3(x931,a4),f3(x931,a4)))),
% 7.81/7.88 inference(scs_inference,[],[84,2])).
% 7.81/7.88 cnf(97,plain,
% 7.81/7.88 (P1(f3(x971,x971),f3(f3(x972,x972),a4))),
% 7.81/7.88 inference(scs_inference,[],[84,90,79,12,2,20,7])).
% 7.81/7.88 cnf(99,plain,
% 7.81/7.88 (E(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x991,x991),a4))),
% 7.81/7.88 inference(scs_inference,[],[84,88,90,79,12,2,20,7,3])).
% 7.81/7.88 cnf(102,plain,
% 7.81/7.88 (~E(f3(x1021,x1021),f3(a4,a1))),
% 7.81/7.88 inference(scs_inference,[],[40,84,88,90,89,79,12,2,20,7,3,6])).
% 7.81/7.88 cnf(104,plain,
% 7.81/7.88 (~P1(f3(a4,a2),f3(a4,a4))),
% 7.81/7.88 inference(scs_inference,[],[40,84,88,90,89,79,12,2,20,7,3,6,5,23])).
% 7.81/7.88 cnf(109,plain,
% 7.81/7.88 (E(f3(f3(x1091,x1091),a4),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[99,102,4,2])).
% 7.81/7.88 cnf(110,plain,
% 7.81/7.88 (E(f3(x1101,x1101),f3(f3(x1102,x1102),a4))),
% 7.81/7.88 inference(scs_inference,[],[99,102,97,76,4,2,20])).
% 7.81/7.88 cnf(111,plain,
% 7.81/7.88 (P1(f3(x1111,x1111),f3(f3(x1112,x1112),a4))),
% 7.81/7.88 inference(rename_variables,[],[97])).
% 7.81/7.88 cnf(115,plain,
% 7.81/7.88 (~E(f3(a4,a1),a2)),
% 7.81/7.88 inference(scs_inference,[],[40,99,39,102,97,25,76,4,2,20,3,7])).
% 7.81/7.88 cnf(117,plain,
% 7.81/7.88 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x1171,x1171),a4))),
% 7.81/7.88 inference(scs_inference,[],[40,99,39,50,102,97,111,25,76,4,2,20,3,7,6])).
% 7.81/7.88 cnf(121,plain,
% 7.81/7.88 (E(f3(f3(x1211,x1211),a4),f3(x1212,x1212))),
% 7.81/7.88 inference(scs_inference,[],[110,2])).
% 7.81/7.88 cnf(122,plain,
% 7.81/7.88 (~E(f3(a4,a1),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[30,110,115,2,3])).
% 7.81/7.88 cnf(125,plain,
% 7.81/7.88 (~E(f3(x1251,x1251),f3(a4,a2))),
% 7.81/7.88 inference(scs_inference,[],[30,110,93,104,117,115,90,2,3,7,6])).
% 7.81/7.88 cnf(128,plain,
% 7.81/7.88 (~E(a4,a2)),
% 7.81/7.88 inference(scs_inference,[],[125,5])).
% 7.81/7.88 cnf(130,plain,
% 7.81/7.88 (E(f3(f3(x1301,a4),f3(x1302,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[88,125,5,2])).
% 7.81/7.88 cnf(131,plain,
% 7.81/7.88 (~E(f3(a4,a1),f3(f3(x1311,x1311),a4))),
% 7.81/7.88 inference(scs_inference,[],[109,88,125,122,5,2,3])).
% 7.81/7.88 cnf(132,plain,
% 7.81/7.88 (~E(f3(a4,f3(a4,a4)),a2)),
% 7.81/7.88 inference(scs_inference,[],[73,109,88,125,122,37,5,2,3,7])).
% 7.81/7.88 cnf(133,plain,
% 7.81/7.88 (P1(f3(f3(x1331,x1331),a4),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.88 inference(scs_inference,[],[73,109,110,88,125,122,37,80,5,2,3,7,6])).
% 7.81/7.88 cnf(135,plain,
% 7.81/7.88 (~P1(a4,f3(a4,a4))),
% 7.81/7.88 inference(scs_inference,[],[73,109,110,88,125,122,37,80,5,2,3,7,6,18])).
% 7.81/7.88 cnf(138,plain,
% 7.81/7.89 (~E(f3(a4,f3(a4,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[30,132,8,2,3])).
% 7.81/7.89 cnf(139,plain,
% 7.81/7.89 (P1(f3(f3(x1391,x1391),a4),a2)),
% 7.81/7.89 inference(scs_inference,[],[30,133,132,8,2,3,7])).
% 7.81/7.89 cnf(142,plain,
% 7.81/7.89 (~E(f3(a4,a4),f3(a4,f3(a4,a4)))),
% 7.81/7.89 inference(scs_inference,[],[30,135,133,132,70,8,2,3,7,6,5])).
% 7.81/7.89 cnf(143,plain,
% 7.81/7.89 (~E(a4,f3(a4,a4))),
% 7.81/7.89 inference(scs_inference,[],[142,5])).
% 7.81/7.89 cnf(144,plain,
% 7.81/7.89 (E(a2,f3(x1441,a4))),
% 7.81/7.89 inference(scs_inference,[],[142,9,5,2])).
% 7.81/7.89 cnf(146,plain,
% 7.81/7.89 (P1(f3(f3(x1461,x1461),a4),f3(a2,x1462))),
% 7.81/7.89 inference(scs_inference,[],[30,83,142,128,139,9,5,2,3,7])).
% 7.81/7.89 cnf(148,plain,
% 7.81/7.89 (E(f3(a4,x1481),f3(a4,f3(a4,f3(a4,x1481))))),
% 7.81/7.89 inference(scs_inference,[],[15,2])).
% 7.81/7.89 cnf(149,plain,
% 7.81/7.89 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(x1491,x1491))),
% 7.81/7.89 inference(scs_inference,[],[121,117,15,2,7])).
% 7.81/7.89 cnf(152,plain,
% 7.81/7.89 (E(f3(f3(x1521,x1521),a4),f3(x1522,x1522))),
% 7.81/7.89 inference(rename_variables,[],[121])).
% 7.81/7.89 cnf(153,plain,
% 7.81/7.89 (P1(f3(x1531,x1531),f3(a2,x1532))),
% 7.81/7.89 inference(scs_inference,[],[121,152,146,143,117,15,2,7,3,6])).
% 7.81/7.89 cnf(155,plain,
% 7.81/7.89 (P1(f3(x1551,x1551),f3(x1552,a4))),
% 7.81/7.89 inference(scs_inference,[],[144,89,7])).
% 7.81/7.89 cnf(156,plain,
% 7.81/7.89 (~E(f3(a4,f3(a4,a4)),f3(f3(x1561,a4),f3(x1562,a4)))),
% 7.81/7.89 inference(scs_inference,[],[130,144,138,89,7,3])).
% 7.81/7.89 cnf(157,plain,
% 7.81/7.89 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(a2,x1571))),
% 7.81/7.89 inference(scs_inference,[],[130,144,153,138,89,7,3,6])).
% 7.81/7.89 cnf(162,plain,
% 7.81/7.89 (P1(f3(x1621,a4),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[148,156,76,4,7])).
% 7.81/7.89 cnf(168,plain,
% 7.81/7.89 (E(f3(a2,a4),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[162,157,20])).
% 7.81/7.89 cnf(169,plain,
% 7.81/7.89 (P1(f3(x1691,a4),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(rename_variables,[],[162])).
% 7.81/7.89 cnf(172,plain,
% 7.81/7.89 (P1(f3(x1721,a4),a2)),
% 7.81/7.89 inference(scs_inference,[],[30,162,169,157,20,7])).
% 7.81/7.89 cnf(179,plain,
% 7.81/7.89 (~E(f3(a4,a2),a2)),
% 7.81/7.89 inference(scs_inference,[],[104,21,19])).
% 7.81/7.89 cnf(180,plain,
% 7.81/7.89 (P1(f3(f3(x1801,a4),f3(x1802,a4)),f3(x1803,x1803))),
% 7.81/7.89 inference(scs_inference,[],[24,56,7])).
% 7.81/7.89 cnf(181,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(a4,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[30,24,179,56,7,3])).
% 7.81/7.89 cnf(183,plain,
% 7.81/7.89 (P1(f3(x1831,a4),f3(f3(x1832,a4),f3(x1833,a4)))),
% 7.81/7.89 inference(scs_inference,[],[72,172,7])).
% 7.81/7.89 cnf(184,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(a2,a4))),
% 7.81/7.89 inference(scs_inference,[],[168,72,181,172,7,3])).
% 7.81/7.89 cnf(186,plain,
% 7.81/7.89 (P1(f3(f3(x1861,a4),f3(x1862,a4)),f3(x1863,x1863))),
% 7.81/7.89 inference(rename_variables,[],[180])).
% 7.81/7.89 cnf(187,plain,
% 7.81/7.89 (E(f3(a4,a4),f3(f3(x1871,a4),f3(x1872,a4)))),
% 7.81/7.89 inference(scs_inference,[],[168,72,181,180,186,172,135,7,3,6,20])).
% 7.81/7.89 cnf(190,plain,
% 7.81/7.89 (E(f3(f3(x1901,a4),f3(x1902,a4)),f3(a4,a4))),
% 7.81/7.89 inference(scs_inference,[],[168,72,181,180,186,172,135,7,3,6,20,2])).
% 7.81/7.89 cnf(191,plain,
% 7.81/7.89 (E(f3(f3(x1911,a4),f3(x1912,a4)),f3(f3(x1911,x1912),a4))),
% 7.81/7.89 inference(scs_inference,[],[183,16,20])).
% 7.81/7.89 cnf(193,plain,
% 7.81/7.89 (P1(f3(x1931,a4),f3(f3(x1932,a4),f3(x1933,a4)))),
% 7.81/7.89 inference(rename_variables,[],[183])).
% 7.81/7.89 cnf(195,plain,
% 7.81/7.89 (P1(f3(x1951,x1951),f3(f3(x1952,a4),f3(x1953,a4)))),
% 7.81/7.89 inference(scs_inference,[],[187,183,155,16,20,7])).
% 7.81/7.89 cnf(197,plain,
% 7.81/7.89 (~E(f3(a4,a1),f3(x1971,x1971))),
% 7.81/7.89 inference(scs_inference,[],[187,110,131,183,155,16,20,7,3])).
% 7.81/7.89 cnf(199,plain,
% 7.81/7.89 (P1(f3(f3(x1991,a4),f3(x1992,a4)),f3(f3(x1993,a4),f3(x1994,a4)))),
% 7.81/7.89 inference(scs_inference,[],[187,110,131,183,193,155,16,20,7,3,6])).
% 7.81/7.89 cnf(201,plain,
% 7.81/7.89 (E(f3(f3(x2011,x2012),a4),f3(f3(x2011,a4),f3(x2012,a4)))),
% 7.81/7.89 inference(scs_inference,[],[187,110,131,183,193,155,16,20,7,3,6,2])).
% 7.81/7.89 cnf(202,plain,
% 7.81/7.89 (P1(f3(x2021,a4),f3(a2,x2022))),
% 7.81/7.89 inference(scs_inference,[],[83,172,7])).
% 7.81/7.89 cnf(205,plain,
% 7.81/7.89 (~E(f3(a4,a1),f3(f3(x2051,a4),f3(x2052,a4)))),
% 7.81/7.89 inference(scs_inference,[],[190,83,197,180,172,104,7,6,3])).
% 7.81/7.89 cnf(213,plain,
% 7.81/7.89 (P1(f3(f3(x2131,a4),f3(x2132,a4)),f3(a2,x2133))),
% 7.81/7.89 inference(scs_inference,[],[191,201,199,202,153,183,20,7,6])).
% 7.81/7.89 cnf(217,plain,
% 7.81/7.89 (E(f3(f3(x2171,a4),f3(x2171,a4)),f3(a2,a4))),
% 7.81/7.89 inference(scs_inference,[],[191,201,205,199,202,153,183,20,7,6,3,2])).
% 7.81/7.89 cnf(218,plain,
% 7.81/7.89 (E(f3(f3(x2181,a4),f3(x2182,a4)),f3(a2,a2))),
% 7.81/7.89 inference(scs_inference,[],[195,213,20])).
% 7.81/7.89 cnf(222,plain,
% 7.81/7.89 (P1(f3(f3(x2221,f3(x2221,a4)),f3(a4,f3(x2221,a4))),f3(a2,a4))),
% 7.81/7.89 inference(scs_inference,[],[217,195,213,16,20,7])).
% 7.81/7.89 cnf(224,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(f3(x2241,a4),f3(x2241,a4)))),
% 7.81/7.89 inference(scs_inference,[],[217,184,195,213,16,20,7,3])).
% 7.81/7.89 cnf(227,plain,
% 7.81/7.89 (E(f3(a2,a2),f3(f3(x2271,a4),f3(x2272,a4)))),
% 7.81/7.89 inference(scs_inference,[],[217,184,195,213,149,135,16,20,7,3,6,2])).
% 7.81/7.89 cnf(228,plain,
% 7.81/7.89 (E(f3(f3(a4,f3(a4,a4)),f3(a4,f3(a4,a4))),f3(a2,a4))),
% 7.81/7.89 inference(scs_inference,[],[222,76,20])).
% 7.81/7.89 cnf(232,plain,
% 7.81/7.89 (P1(f3(f3(x2321,a4),f3(x2322,a4)),f3(x2323,a4))),
% 7.81/7.89 inference(scs_inference,[],[144,222,76,56,20,7])).
% 7.81/7.89 cnf(235,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(a2,a2))),
% 7.81/7.89 inference(scs_inference,[],[227,144,222,224,70,76,104,56,20,7,6,3])).
% 7.81/7.89 cnf(238,plain,
% 7.81/7.89 (E(f3(x2381,a4),f3(f3(x2382,a4),f3(x2383,a4)))),
% 7.81/7.89 inference(scs_inference,[],[232,183,20])).
% 7.81/7.89 cnf(241,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(f3(x2411,a4),f3(x2412,a4)))),
% 7.81/7.89 inference(scs_inference,[],[218,235,232,183,20,3])).
% 7.81/7.89 cnf(242,plain,
% 7.81/7.89 (E(f3(f3(x2421,a4),f3(x2422,a4)),f3(x2423,a4))),
% 7.81/7.89 inference(scs_inference,[],[218,235,232,183,20,3,2])).
% 7.81/7.89 cnf(243,plain,
% 7.81/7.89 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x2431,a4),f3(x2432,a4)))),
% 7.81/7.89 inference(scs_inference,[],[238,117,7])).
% 7.81/7.89 cnf(244,plain,
% 7.81/7.89 (E(f3(x2441,a4),f3(f3(x2442,a4),f3(x2443,a4)))),
% 7.81/7.89 inference(rename_variables,[],[238])).
% 7.81/7.89 cnf(245,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(x2451,a4))),
% 7.81/7.89 inference(scs_inference,[],[238,244,241,117,7,3])).
% 7.81/7.89 cnf(247,plain,
% 7.81/7.89 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(x2471,a4))),
% 7.81/7.89 inference(scs_inference,[],[242,243,7])).
% 7.81/7.89 cnf(249,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(f3(a4,f3(a4,a4)),f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[228,242,243,245,7,3])).
% 7.81/7.89 cnf(254,plain,
% 7.81/7.89 (~E(f3(a4,a2),f3(x2541,x2541))),
% 7.81/7.89 inference(scs_inference,[],[67,249,3])).
% 7.81/7.89 cnf(256,plain,
% 7.81/7.89 (~E(f3(a4,f3(a4,a4)),f3(a2,x2561))),
% 7.81/7.89 inference(scs_inference,[],[10,132,3])).
% 7.81/7.89 cnf(267,plain,
% 7.81/7.89 (E(f3(a2,x2671),f3(f3(x2672,a4),x2671))),
% 7.81/7.89 inference(scs_inference,[],[9,2,4])).
% 7.81/7.89 cnf(268,plain,
% 7.81/7.89 (E(f3(f3(x2681,a4),x2682),f3(a2,x2682))),
% 7.81/7.89 inference(scs_inference,[],[267,2])).
% 7.81/7.89 cnf(269,plain,
% 7.81/7.89 (P1(f3(f3(x2691,f3(x2691,a4)),f3(a4,f3(x2691,a4))),a2)),
% 7.81/7.89 inference(scs_inference,[],[9,267,222,2,7])).
% 7.81/7.89 cnf(273,plain,
% 7.81/7.89 (E(f3(f3(x2731,f3(x2731,a4)),f3(a4,f3(x2731,a4))),a2)),
% 7.81/7.89 inference(scs_inference,[],[9,254,267,222,12,2,7,3,20])).
% 7.81/7.89 cnf(277,plain,
% 7.81/7.89 (P1(f3(x2771,f3(x2771,a4)),f3(a4,f3(x2771,a4)))),
% 7.81/7.89 inference(scs_inference,[],[9,40,254,267,222,12,2,7,3,20,6,19])).
% 7.81/7.89 cnf(279,plain,
% 7.81/7.89 (E(f3(x2791,a2),f3(x2791,f3(x2792,a4)))),
% 7.81/7.89 inference(scs_inference,[],[9,2,5])).
% 7.81/7.89 cnf(280,plain,
% 7.81/7.89 (E(a2,f3(f3(x2801,f3(x2801,a4)),f3(a4,f3(x2801,a4))))),
% 7.81/7.89 inference(scs_inference,[],[273,2])).
% 7.81/7.89 cnf(281,plain,
% 7.81/7.89 (P1(f3(a2,f3(x2811,a4)),f3(f3(x2812,a4),f3(x2813,a4)))),
% 7.81/7.89 inference(scs_inference,[],[268,273,199,2,6])).
% 7.81/7.89 cnf(283,plain,
% 7.81/7.89 (E(f3(f3(x2831,a4),x2832),f3(a2,x2832))),
% 7.81/7.89 inference(rename_variables,[],[268])).
% 7.81/7.89 cnf(284,plain,
% 7.81/7.89 (P1(f3(a4,f3(a4,f3(a4,a4))),a2)),
% 7.81/7.89 inference(scs_inference,[],[9,268,273,199,247,2,6,7])).
% 7.81/7.89 cnf(288,plain,
% 7.81/7.89 (E(f3(a2,f3(x2881,a4)),f3(f3(x2882,a4),f3(x2883,a4)))),
% 7.81/7.89 inference(scs_inference,[],[9,268,283,273,256,199,247,213,2,6,7,3,20])).
% 7.81/7.89 cnf(291,plain,
% 7.81/7.89 (E(f3(a1,f3(x2911,a4)),a1)),
% 7.81/7.89 inference(scs_inference,[],[279,2,60])).
% 7.81/7.89 cnf(292,plain,
% 7.81/7.89 (E(f3(f3(x2921,a4),f3(x2922,a4)),f3(a2,f3(x2923,a4)))),
% 7.81/7.89 inference(scs_inference,[],[288,2])).
% 7.81/7.89 cnf(293,plain,
% 7.81/7.89 (P1(f3(f3(x2931,a4),f3(x2932,a4)),f3(a4,f3(a2,a4)))),
% 7.81/7.89 inference(scs_inference,[],[288,277,2,6])).
% 7.81/7.89 cnf(296,plain,
% 7.81/7.89 (P1(f3(a2,f3(x2961,a4)),f3(a2,a2))),
% 7.81/7.89 inference(scs_inference,[],[288,218,277,281,2,6,7])).
% 7.81/7.89 cnf(302,plain,
% 7.81/7.89 (E(a1,f3(a1,f3(x3021,a4)))),
% 7.81/7.89 inference(scs_inference,[],[291,2])).
% 7.81/7.89 cnf(307,plain,
% 7.81/7.89 (P1(f3(x3071,x3071),f3(f3(x3072,f3(x3072,a4)),f3(a4,f3(x3072,a4))))),
% 7.81/7.89 inference(scs_inference,[],[40,280,291,296,284,153,89,2,20,6,7])).
% 7.81/7.89 cnf(312,plain,
% 7.81/7.89 (E(f3(x3121,f3(x3122,a4)),f3(x3121,a2))),
% 7.81/7.89 inference(scs_inference,[],[279,2])).
% 7.81/7.89 cnf(313,plain,
% 7.81/7.89 (P1(f3(x3131,a4),f3(f3(x3132,f3(x3132,a4)),f3(a4,f3(x3132,a4))))),
% 7.81/7.89 inference(scs_inference,[],[280,279,172,2,7])).
% 7.81/7.89 cnf(318,plain,
% 7.81/7.89 (P1(f3(f3(x3181,a4),f3(x3182,a4)),f3(a4,a2))),
% 7.81/7.89 inference(scs_inference,[],[312,293,313,222,20,7])).
% 7.81/7.89 cnf(323,plain,
% 7.81/7.89 (P1(f3(f3(x3231,f3(x3231,a4)),f3(a4,f3(x3231,a4))),f3(x3232,a4))),
% 7.81/7.89 inference(scs_inference,[],[9,269,2,7])).
% 7.81/7.89 cnf(324,plain,
% 7.81/7.89 (~P1(f3(a4,a2),f3(f3(x3241,a4),f3(x3241,a4)))),
% 7.81/7.89 inference(scs_inference,[],[125,318,20])).
% 7.81/7.89 cnf(338,plain,
% 7.81/7.89 (~E(f3(a2,f3(x3381,a4)),f3(a4,a2))),
% 7.81/7.89 inference(scs_inference,[],[324,307,323,281,20,6])).
% 7.81/7.89 cnf(340,plain,
% 7.81/7.89 (P1(f3(f3(x3401,a4),x3402),a2)),
% 7.81/7.89 inference(scs_inference,[],[9,324,307,323,281,14,20,6,7])).
% 7.81/7.89 cnf(344,plain,
% 7.81/7.89 (E(f3(f3(x3441,a4),x3442),a2)),
% 7.81/7.89 inference(scs_inference,[],[340,12,20])).
% 7.81/7.89 cnf(349,plain,
% 7.81/7.89 (P1(f3(x3491,a4),x3492)),
% 7.81/7.89 inference(scs_inference,[],[40,39,340,12,20,6,7,19])).
% 7.81/7.89 cnf(351,plain,
% 7.81/7.89 (E(a2,f3(f3(x3511,a4),x3512))),
% 7.81/7.89 inference(scs_inference,[],[40,39,340,12,20,6,7,19,2])).
% 7.81/7.89 cnf(352,plain,
% 7.81/7.89 (E(a2,f3(f3(f3(x3521,a4),f3(x3522,a4)),f3(a4,f3(a2,a4))))),
% 7.81/7.89 inference(scs_inference,[],[293,18,2])).
% 7.81/7.89 cnf(358,plain,
% 7.81/7.89 (P1(f3(a2,f3(x3581,a4)),f3(a4,f3(a2,a4)))),
% 7.81/7.89 inference(scs_inference,[],[292,352,102,293,349,2,20,6])).
% 7.81/7.89 cnf(362,plain,
% 7.81/7.89 (E(f3(x3621,a4),f3(f3(f3(x3622,a4),f3(x3623,a4)),f3(a4,f3(a2,a4))))),
% 7.81/7.89 inference(scs_inference,[],[9,292,352,102,293,349,281,2,20,6,7,3])).
% 7.81/7.89 cnf(367,plain,
% 7.81/7.89 (P1(f3(a2,a2),f3(a4,f3(a2,a4)))),
% 7.81/7.89 inference(scs_inference,[],[362,312,358,2,6])).
% 7.81/7.89 cnf(368,plain,
% 7.81/7.89 (P1(f3(a2,f3(x3681,a4)),f3(a4,f3(a2,a4)))),
% 7.81/7.89 inference(rename_variables,[],[358])).
% 7.81/7.89 cnf(369,plain,
% 7.81/7.89 (E(f3(x3691,f3(x3692,a4)),f3(x3691,a2))),
% 7.81/7.89 inference(rename_variables,[],[312])).
% 7.81/7.89 cnf(370,plain,
% 7.81/7.89 (P1(f3(a2,f3(x3701,a4)),f3(a4,a2))),
% 7.81/7.89 inference(scs_inference,[],[362,312,369,358,368,2,6,7])).
% 7.81/7.89 cnf(376,plain,
% 7.81/7.89 (~P1(f3(a4,a2),f3(a2,f3(x3761,a4)))),
% 7.81/7.89 inference(scs_inference,[],[338,370,20])).
% 7.81/7.89 cnf(456,plain,
% 7.81/7.89 (E(f3(a2,a2),f3(a4,f3(a2,a4)))+~P1(f3(a4,f3(a2,a4)),f3(a2,a2))),
% 7.81/7.89 inference(scs_inference,[],[351,367,340,7,20])).
% 7.81/7.89 cnf(473,plain,
% 7.81/7.89 (E(f3(a2,a2),f3(a4,f3(a2,a4)))+~E(f3(f3(a4,f3(a2,a4)),f3(a2,a2)),a2)),
% 7.81/7.89 inference(scs_inference,[],[456,19])).
% 7.81/7.89 cnf(476,plain,
% 7.81/7.89 (E(f3(f3(a2,x4761),x4762),a2)),
% 7.81/7.89 inference(scs_inference,[],[10,14,12,7,20])).
% 7.81/7.89 cnf(481,plain,
% 7.81/7.89 (P1(f3(a2,x4811),x4812)),
% 7.81/7.89 inference(scs_inference,[],[10,40,14,12,132,7,20,6,3,19])).
% 7.81/7.89 cnf(486,plain,
% 7.81/7.89 (E(a2,f3(f3(a2,x4861),x4862))),
% 7.81/7.89 inference(scs_inference,[],[476,2])).
% 7.81/7.89 cnf(492,plain,
% 7.81/7.89 (P1(f3(f3(x4921,x4922),f3(a4,x4922)),a2)),
% 7.81/7.89 inference(scs_inference,[],[344,476,102,16,115,481,2,20,3,7])).
% 7.81/7.89 cnf(502,plain,
% 7.81/7.89 (P1(f3(x5021,x5022),f3(a4,x5022))),
% 7.81/7.89 inference(scs_inference,[],[476,12,179,492,20,3,19])).
% 7.81/7.89 cnf(505,plain,
% 7.81/7.89 (P1(f3(x5051,f3(a4,f3(a4,a4))),a2)),
% 7.81/7.89 inference(scs_inference,[],[30,476,12,179,492,20,3,19,2,7])).
% 7.81/7.89 cnf(507,plain,
% 7.81/7.89 (~E(f3(f3(a4,f3(a2,a4)),f3(a2,a2)),a2)),
% 7.81/7.89 inference(scs_inference,[],[312,125,473,3])).
% 7.81/7.89 cnf(512,plain,
% 7.81/7.89 (~P1(f3(a4,a1),f3(a1,a1))),
% 7.81/7.89 inference(scs_inference,[],[102,502,507,18,23,20])).
% 7.81/7.89 cnf(527,plain,
% 7.81/7.89 (E(a2,f3(x5271,f3(a4,f3(a4,a4))))),
% 7.81/7.89 inference(scs_inference,[],[512,302,144,291,340,12,505,23,20,3,7,2])).
% 7.81/7.89 cnf(633,plain,
% 7.81/7.89 (P1(f3(x6331,x6332),f3(x6331,f3(x6333,a4)))),
% 7.81/7.89 inference(scs_inference,[],[344,19,21])).
% 7.81/7.89 cnf(635,plain,
% 7.81/7.89 (P1(f3(x6351,x6352),f3(x6351,f3(x6353,a4)))),
% 7.81/7.89 inference(rename_variables,[],[633])).
% 7.81/7.89 cnf(639,plain,
% 7.81/7.89 (P1(f3(f3(f3(x6391,a4),x6392),x6393),a2)),
% 7.81/7.89 inference(scs_inference,[],[376,344,14,633,635,142,20,6,7])).
% 7.81/7.89 cnf(667,plain,
% 7.81/7.89 (E(f3(f3(x6671,a4),x6672),f3(f3(a2,x6673),x6674))),
% 7.81/7.89 inference(scs_inference,[],[344,486,12,639,20,3])).
% 7.81/7.89 cnf(668,plain,
% 7.81/7.89 (P1(f3(f3(x6681,a4),x6682),x6683)),
% 7.81/7.89 inference(scs_inference,[],[344,486,12,639,20,3,19])).
% 7.81/7.89 cnf(670,plain,
% 7.81/7.89 (E(a2,f3(f3(f3(x6701,a4),x6702),x6703))),
% 7.81/7.89 inference(scs_inference,[],[344,486,12,639,20,3,19,2])).
% 7.81/7.89 cnf(676,plain,
% 7.81/7.89 (P1(f3(f3(f3(x6761,a4),x6762),x6763),f3(a2,x6764))),
% 7.81/7.89 inference(scs_inference,[],[83,667,102,668,639,2,20,7])).
% 7.81/7.89 cnf(711,plain,
% 7.81/7.89 (E(f3(x7111,a2),f3(x7111,f3(f3(x7112,a4),x7113)))),
% 7.81/7.89 inference(scs_inference,[],[344,5,2])).
% 7.81/7.89 cnf(713,plain,
% 7.81/7.89 (P1(f3(x7131,f3(a4,f3(a4,a4))),f3(x7132,a4))),
% 7.81/7.89 inference(scs_inference,[],[144,711,505,2,7])).
% 7.81/7.89 cnf(721,plain,
% 7.81/7.89 (E(f3(f3(x7211,x7212),f3(x7211,a2)),a2)),
% 7.81/7.89 inference(scs_inference,[],[12,21,18])).
% 7.81/7.89 cnf(724,plain,
% 7.81/7.89 (E(a2,f3(f3(x7241,x7242),f3(x7241,a2)))),
% 7.81/7.89 inference(scs_inference,[],[721,19,2])).
% 7.81/7.89 cnf(745,plain,
% 7.81/7.89 (P1(f3(f3(x7451,x7451),x7452),a2)),
% 7.81/7.89 inference(scs_inference,[],[13,14,7])).
% 7.81/7.89 cnf(749,plain,
% 7.81/7.89 (E(f3(f3(x7491,x7491),x7492),a2)),
% 7.81/7.89 inference(scs_inference,[],[13,670,14,12,7,3,2,20])).
% 7.81/7.89 cnf(755,plain,
% 7.81/7.89 (P1(f3(f3(x7551,x7552),x7553),f3(f3(x7551,f3(x7554,a4)),x7553))),
% 7.81/7.89 inference(scs_inference,[],[349,22,21])).
% 7.81/7.89 cnf(756,plain,
% 7.81/7.89 (E(a2,f3(f3(x7561,x7561),x7562))),
% 7.81/7.89 inference(scs_inference,[],[749,2])).
% 7.81/7.89 cnf(761,plain,
% 7.81/7.89 (P1(f3(f3(x7611,f3(x7611,x7612)),f3(x7612,f3(x7611,x7612))),a2)),
% 7.81/7.89 inference(scs_inference,[],[13,749,349,16,713,2,20,7])).
% 7.81/7.89 cnf(763,plain,
% 7.81/7.89 (E(f3(x7631,x7631),a2)),
% 7.81/7.89 inference(rename_variables,[],[13])).
% 7.81/7.89 cnf(764,plain,
% 7.81/7.89 (E(f3(x7641,x7641),f3(f3(x7642,x7643),f3(x7642,a2)))),
% 7.81/7.89 inference(scs_inference,[],[13,763,749,724,349,16,713,2,20,7,3])).
% 7.81/7.89 cnf(772,plain,
% 7.81/7.89 (P1(f3(f3(x7721,x7722),f3(x7721,f3(x7723,a4))),a2)),
% 7.81/7.89 inference(scs_inference,[],[13,764,349,755,676,2,20,7])).
% 7.81/7.89 cnf(774,plain,
% 7.81/7.89 (E(f3(x7741,x7741),a2)),
% 7.81/7.89 inference(rename_variables,[],[13])).
% 7.81/7.89 cnf(775,plain,
% 7.81/7.89 (E(f3(x7751,x7751),f3(f3(x7752,x7752),x7753))),
% 7.81/7.89 inference(scs_inference,[],[13,774,764,756,349,755,676,2,20,7,3])).
% 7.81/7.89 cnf(784,plain,
% 7.81/7.89 (P1(f3(x7841,f3(x7841,x7842)),f3(x7842,f3(x7841,x7842)))),
% 7.81/7.89 inference(scs_inference,[],[13,40,83,775,527,12,745,761,772,2,20,6,7,3,19])).
% 7.81/7.89 cnf(1210,plain,
% 7.81/7.89 ($false),
% 7.81/7.89 inference(scs_inference,[],[27,15,784,6]),
% 7.81/7.89 ['proof']).
% 7.81/7.89 % SZS output end Proof
% 7.81/7.89 % Total time :7.270000s
%------------------------------------------------------------------------------