%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG001-5 : 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 : n014.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 14:00:33 EDT 2024
% Result : Unsatisfiable 1.51s 1.64s
% Output : CNFRefutation 1.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : RNG001-5 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n014.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 : Tue Jun 18 14:16:39 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 1.51/1.63 %-------------------------------------------
% 1.51/1.63 % File :CSE---1.7
% 1.51/1.63 % Problem :theBenchmark
% 1.51/1.63 % Transform :cnf
% 1.51/1.63 % Format :tptp:raw
% 1.51/1.63 % Command :java -jar mcs_scs.jar %d %s
% 1.51/1.63
% 1.51/1.63 % Result :Theorem 1.030000s
% 1.51/1.63 % Output :CNFRefutation 1.030000s
% 1.51/1.63 %-------------------------------------------
% 1.51/1.63 %--------------------------------------------------------------------------
% 1.51/1.63 % File : RNG001-5 : TPTP v8.2.0. Released v1.0.0.
% 1.51/1.63 % Domain : Ring Theory
% 1.51/1.63 % Problem : X.additive_identity = additive_identity for any X
% 1.51/1.63 % Version : [Wos65] axioms : Reduced > Incomplete.
% 1.51/1.63 % English :
% 1.51/1.63
% 1.51/1.63 % Refs : [Wos65] Wos (1965), Unpublished Note
% 1.51/1.63 % : [FL+74] Fleisig et al. (1974), An Implementation of the Model
% 1.51/1.63 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 1.51/1.63 % Source : [SPRFN]
% 1.51/1.63 % Names : Problem 21 [Wos65]
% 1.51/1.63 % : wos21 [WM76]
% 1.51/1.63
% 1.51/1.63 % Status : Unsatisfiable
% 1.51/1.63 % Rating : 0.09 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.29 v6.0.0, 0.22 v5.5.0, 0.50 v5.3.0, 0.55 v5.2.0, 0.31 v5.1.0, 0.44 v5.0.0, 0.40 v4.0.1, 0.43 v3.4.0, 0.40 v3.3.0, 0.00 v2.7.0, 0.25 v2.6.0, 0.43 v2.5.0, 0.29 v2.4.0, 0.29 v2.3.0, 0.57 v2.2.1, 0.67 v2.1.0, 0.57 v2.0.0
% 1.51/1.63 % Syntax : Number of clauses : 30 ( 8 unt; 0 nHn; 21 RR)
% 1.51/1.63 % Number of literals : 81 ( 0 equ; 52 neg)
% 1.51/1.63 % Maximal clause size : 5 ( 2 avg)
% 1.51/1.63 % Maximal term depth : 2 ( 1 avg)
% 1.51/1.63 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 1.51/1.63 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 1.51/1.63 % Number of variables : 109 ( 0 sgn)
% 1.51/1.63 % SPC : CNF_UNS_RFO_NEQ_HRN
% 1.51/1.63
% 1.51/1.63 % Comments : Omits two equality subsitution axioms.
% 1.51/1.63 % : These are the same axioms as in [MOW76].
% 1.51/1.63 % : I guess this is Example 6c in [FL+74].
% 1.51/1.63 %--------------------------------------------------------------------------
% 1.51/1.63 %----Include ring theory axioms
% 1.51/1.63 %include('Axioms/RNG001-0.ax').
% 1.51/1.63 %--------------------------------------------------------------------------
% 1.51/1.63 cnf(reflexivity,axiom,
% 1.51/1.63 equalish(X,X) ).
% 1.51/1.63
% 1.51/1.63 cnf(symmetry,axiom,
% 1.51/1.63 ( ~ equalish(X,Y)
% 1.51/1.63 | equalish(Y,X) ) ).
% 1.51/1.63
% 1.51/1.63 cnf(transitivity,axiom,
% 1.51/1.63 ( ~ equalish(X,Y)
% 1.51/1.63 | ~ equalish(Y,Z)
% 1.51/1.63 | equalish(X,Z) ) ).
% 1.51/1.63
% 1.51/1.63 %----Equality axioms for additive operator
% 1.51/1.63 cnf(additive_inverse_substitution,axiom,
% 1.51/1.63 ( ~ equalish(X,Y)
% 1.51/1.63 | equalish(additive_inverse(X),additive_inverse(Y)) ) ).
% 1.51/1.63
% 1.51/1.63 cnf(add_substitution1,axiom,
% 1.51/1.63 ( ~ equalish(X,Y)
% 1.51/1.63 | equalish(add(X,W),add(Y,W)) ) ).
% 1.51/1.63
% 1.51/1.63 %----This axiom omited in this version
% 1.51/1.63 %input_clause(add_substitution2,axiom,
% 1.51/1.63 % [--equalish(X,Y),
% 1.51/1.63 % ++equalish(add(W,X),add(W,Y))]).
% 1.51/1.64
% 1.51/1.64 cnf(sum_substitution1,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ sum(X,W,Z)
% 1.51/1.64 | sum(Y,W,Z) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(sum_substitution2,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ sum(W,X,Z)
% 1.51/1.64 | sum(W,Y,Z) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(sum_substitution3,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ sum(W,Z,X)
% 1.51/1.64 | sum(W,Z,Y) ) ).
% 1.51/1.64
% 1.51/1.64 %----Equality axioms for multiplicative operator
% 1.51/1.64 cnf(multiply_substitution1,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 1.51/1.64
% 1.51/1.64 %----This axiom omited in this version
% 1.51/1.64 %input_clause(multiply_substitution2,axiom,
% 1.51/1.64 % [--equalish(X,Y),
% 1.51/1.64 % ++equalish(multiply(W,X),multiply(W,Y))]).
% 1.51/1.64
% 1.51/1.64 cnf(product_substitution1,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ product(X,W,Z)
% 1.51/1.64 | product(Y,W,Z) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(product_substitution2,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ product(W,X,Z)
% 1.51/1.64 | product(W,Y,Z) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(product_substitution3,axiom,
% 1.51/1.64 ( ~ equalish(X,Y)
% 1.51/1.64 | ~ product(W,Z,X)
% 1.51/1.64 | product(W,Z,Y) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(additive_identity1,axiom,
% 1.51/1.64 sum(additive_identity,X,X) ).
% 1.51/1.64
% 1.51/1.64 cnf(additive_identity2,axiom,
% 1.51/1.64 sum(X,additive_identity,X) ).
% 1.51/1.64
% 1.51/1.64 cnf(closure_of_multiplication,axiom,
% 1.51/1.64 product(X,Y,multiply(X,Y)) ).
% 1.51/1.64
% 1.51/1.64 cnf(closure_of_addition,axiom,
% 1.51/1.64 sum(X,Y,add(X,Y)) ).
% 1.51/1.64
% 1.51/1.64 cnf(left_inverse,axiom,
% 1.51/1.64 sum(additive_inverse(X),X,additive_identity) ).
% 1.51/1.64
% 1.51/1.64 cnf(right_inverse,axiom,
% 1.51/1.64 sum(X,additive_inverse(X),additive_identity) ).
% 1.51/1.64
% 1.51/1.64 cnf(associativity_of_addition1,axiom,
% 1.51/1.64 ( ~ sum(X,Y,U)
% 1.51/1.64 | ~ sum(Y,Z,V)
% 1.51/1.64 | ~ sum(U,Z,W)
% 1.51/1.64 | sum(X,V,W) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(associativity_of_addition2,axiom,
% 1.51/1.64 ( ~ sum(X,Y,U)
% 1.51/1.64 | ~ sum(Y,Z,V)
% 1.51/1.64 | ~ sum(X,V,W)
% 1.51/1.64 | sum(U,Z,W) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(commutativity_of_addition,axiom,
% 1.51/1.64 ( ~ sum(X,Y,Z)
% 1.51/1.64 | sum(Y,X,Z) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(associativity_of_multiplication1,axiom,
% 1.51/1.64 ( ~ product(X,Y,U)
% 1.51/1.64 | ~ product(Y,Z,V)
% 1.51/1.64 | ~ product(U,Z,W)
% 1.51/1.64 | product(X,V,W) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(associativity_of_multiplication2,axiom,
% 1.51/1.64 ( ~ product(X,Y,U)
% 1.51/1.64 | ~ product(Y,Z,V)
% 1.51/1.64 | ~ product(X,V,W)
% 1.51/1.64 | product(U,Z,W) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(distributivity1,axiom,
% 1.51/1.64 ( ~ product(X,Y,V1)
% 1.51/1.64 | ~ product(X,Z,V2)
% 1.51/1.64 | ~ sum(Y,Z,V3)
% 1.51/1.64 | ~ product(X,V3,V4)
% 1.51/1.64 | sum(V1,V2,V4) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(distributivity2,axiom,
% 1.51/1.64 ( ~ product(X,Y,V1)
% 1.51/1.64 | ~ product(X,Z,V2)
% 1.51/1.64 | ~ sum(Y,Z,V3)
% 1.51/1.64 | ~ sum(V1,V2,V4)
% 1.51/1.64 | product(X,V3,V4) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(distributivity3,axiom,
% 1.51/1.64 ( ~ product(Y,X,V1)
% 1.51/1.64 | ~ product(Z,X,V2)
% 1.51/1.64 | ~ sum(Y,Z,V3)
% 1.51/1.64 | ~ product(V3,X,V4)
% 1.51/1.64 | sum(V1,V2,V4) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(distributivity4,axiom,
% 1.51/1.64 ( ~ product(Y,X,V1)
% 1.51/1.64 | ~ product(Z,X,V2)
% 1.51/1.64 | ~ sum(Y,Z,V3)
% 1.51/1.64 | ~ sum(V1,V2,V4)
% 1.51/1.64 | product(V3,X,V4) ) ).
% 1.51/1.64
% 1.51/1.64 %-----Equality axioms for operators
% 1.51/1.64 cnf(addition_is_well_defined,axiom,
% 1.51/1.64 ( ~ sum(X,Y,U)
% 1.51/1.64 | ~ sum(X,Y,V)
% 1.51/1.64 | equalish(U,V) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(multiplication_is_well_defined,axiom,
% 1.51/1.64 ( ~ product(X,Y,U)
% 1.51/1.64 | ~ product(X,Y,V)
% 1.51/1.64 | equalish(U,V) ) ).
% 1.51/1.64
% 1.51/1.64 cnf(prove_multiplicative_identity_axiom,negated_conjecture,
% 1.51/1.64 ~ product(a,additive_identity,additive_identity) ).
% 1.51/1.64
% 1.51/1.64 %--------------------------------------------------------------------------
% 1.51/1.64 %-------------------------------------------
% 1.51/1.64 % Proof found
% 1.51/1.64 % SZS status Theorem for theBenchmark
% 1.51/1.64 % SZS output start Proof
% 1.51/1.64 %ClaNum:30(EqnAxiom:0)
% 1.51/1.64 %VarNum:222(SingletonVarNum:109)
% 1.51/1.64 %MaxLitNum:5
% 1.51/1.64 %MaxfuncDepth:1
% 1.51/1.64 %SharedTerms:3
% 1.51/1.64 %goalClause: 8
% 1.51/1.64 %singleGoalClaCount:1
% 1.51/1.64 [8]~P3(a3,a1,a1)
% 1.51/1.64 [1]P1(x11,x11)
% 1.51/1.64 [2]P2(x21,a1,x21)
% 1.51/1.64 [3]P2(a1,x31,x31)
% 1.51/1.64 [4]P2(x41,f4(x41),a1)
% 1.51/1.64 [5]P2(f4(x51),x51,a1)
% 1.51/1.64 [6]P2(x61,x62,f2(x61,x62))
% 1.51/1.64 [7]P3(x71,x72,f5(x71,x72))
% 1.51/1.64 [9]~P1(x92,x91)+P1(x91,x92)
% 1.51/1.64 [10]~P1(x101,x102)+P1(f4(x101),f4(x102))
% 1.51/1.64 [14]~P2(x142,x141,x143)+P2(x141,x142,x143)
% 1.51/1.64 [12]~P1(x121,x123)+P1(f2(x121,x122),f2(x123,x122))
% 1.51/1.64 [13]~P1(x131,x133)+P1(f5(x131,x132),f5(x133,x132))
% 1.51/1.64 [11]~P1(x111,x113)+P1(x111,x112)+~P1(x113,x112)
% 1.51/1.64 [15]~P2(x151,x152,x154)+P2(x151,x152,x153)+~P1(x154,x153)
% 1.51/1.64 [16]~P2(x161,x164,x163)+P2(x161,x162,x163)+~P1(x164,x162)
% 1.51/1.64 [17]~P2(x174,x172,x173)+P2(x171,x172,x173)+~P1(x174,x171)
% 1.51/1.64 [18]~P3(x181,x182,x184)+P3(x181,x182,x183)+~P1(x184,x183)
% 1.51/1.64 [19]~P3(x191,x194,x193)+P3(x191,x192,x193)+~P1(x194,x192)
% 1.51/1.64 [20]~P3(x204,x202,x203)+P3(x201,x202,x203)+~P1(x204,x201)
% 1.51/1.64 [21]~P2(x213,x214,x211)+P1(x211,x212)+~P2(x213,x214,x212)
% 1.51/1.64 [22]~P3(x223,x224,x221)+P1(x221,x222)+~P3(x223,x224,x222)
% 1.51/1.64 [23]~P2(x236,x234,x231)+P2(x231,x232,x233)+~P2(x234,x232,x235)+~P2(x236,x235,x233)
% 1.51/1.64 [24]~P2(x241,x246,x244)+P2(x241,x242,x243)+~P2(x244,x245,x243)+~P2(x246,x245,x242)
% 1.51/1.64 [25]~P3(x256,x254,x251)+P3(x251,x252,x253)+~P3(x254,x252,x255)+~P3(x256,x255,x253)
% 1.51/1.64 [26]~P3(x261,x266,x264)+P3(x261,x262,x263)+~P3(x264,x265,x263)+~P3(x266,x265,x262)
% 1.51/1.64 [27]~P3(x277,x275,x272)+~P3(x277,x274,x271)+P2(x271,x272,x273)+~P2(x274,x275,x276)+~P3(x277,x276,x273)
% 1.51/1.64 [28]~P3(x285,x287,x282)+~P3(x284,x287,x281)+P2(x281,x282,x283)+~P2(x284,x285,x286)+~P3(x286,x287,x283)
% 1.51/1.64 [29]~P3(x297,x292,x295)+~P3(x296,x292,x294)+P3(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x297,x291)
% 1.51/1.64 [30]~P3(x301,x307,x305)+~P3(x301,x306,x304)+P3(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x307,x302)
% 1.51/1.64 %EqnAxiom
% 1.51/1.64
% 1.51/1.64 %-------------------------------------------
% 1.51/1.64 cnf(31,plain,
% 1.51/1.64 (P1(x311,f2(x311,a1))),
% 1.51/1.64 inference(scs_inference,[],[2,6,21])).
% 1.51/1.64 cnf(32,plain,
% 1.51/1.64 (P2(x321,x322,f2(x321,x322))),
% 1.51/1.64 inference(rename_variables,[],[6])).
% 1.51/1.64 cnf(34,plain,
% 1.51/1.64 (P2(x341,f2(a1,a1),x341)),
% 1.51/1.64 inference(scs_inference,[],[2,6,32,21,24])).
% 1.51/1.64 cnf(35,plain,
% 1.51/1.64 (P2(x351,x352,f2(x351,x352))),
% 1.51/1.64 inference(rename_variables,[],[6])).
% 1.51/1.64 cnf(38,plain,
% 1.51/1.64 (P2(x381,x382,f2(x381,x382))),
% 1.51/1.64 inference(rename_variables,[],[6])).
% 1.51/1.64 cnf(39,plain,
% 1.51/1.64 (P2(x391,a1,x391)),
% 1.51/1.64 inference(rename_variables,[],[2])).
% 1.51/1.64 cnf(41,plain,
% 1.51/1.64 (P3(x411,x412,f5(x411,x412))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(43,plain,
% 1.51/1.64 (P2(f5(x431,a1),f5(x431,a1),f5(x431,a1))),
% 1.51/1.64 inference(scs_inference,[],[2,39,6,32,35,7,41,21,24,29,27])).
% 1.51/1.64 cnf(46,plain,
% 1.51/1.64 (P3(x461,x462,f5(x461,x462))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(47,plain,
% 1.51/1.64 (P2(x471,a1,x471)),
% 1.51/1.64 inference(rename_variables,[],[2])).
% 1.51/1.64 cnf(49,plain,
% 1.51/1.64 (P2(f5(a1,x491),f5(a1,x491),f5(a1,x491))),
% 1.51/1.64 inference(scs_inference,[],[2,39,47,6,32,35,7,41,46,21,24,29,27,28])).
% 1.51/1.64 cnf(52,plain,
% 1.51/1.64 (P3(x521,x522,f5(x521,x522))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(53,plain,
% 1.51/1.64 (P2(x531,a1,x531)),
% 1.51/1.64 inference(rename_variables,[],[2])).
% 1.51/1.64 cnf(57,plain,
% 1.51/1.64 (P2(x571,a1,x571)),
% 1.51/1.64 inference(rename_variables,[],[2])).
% 1.51/1.64 cnf(58,plain,
% 1.51/1.64 (P3(x581,x582,f5(x581,x582))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(59,plain,
% 1.51/1.64 (P3(x591,x592,f5(x591,x592))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(61,plain,
% 1.51/1.64 (~P3(x611,x612,a1)+P3(x611,x612,f2(a1,a1))),
% 1.51/1.64 inference(scs_inference,[],[2,39,47,53,6,32,35,38,7,41,46,52,21,24,29,27,28,30,18])).
% 1.51/1.64 cnf(63,plain,
% 1.51/1.64 (P3(x631,f2(a1,a1),f5(x631,a1))),
% 1.51/1.64 inference(scs_inference,[],[2,39,47,53,6,32,35,38,7,41,46,52,59,21,24,29,27,28,30,18,19])).
% 1.51/1.64 cnf(64,plain,
% 1.51/1.64 (P3(x641,x642,f5(x641,x642))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(66,plain,
% 1.51/1.64 (P3(f2(a1,a1),x661,f5(a1,x661))),
% 1.51/1.64 inference(scs_inference,[],[2,39,47,53,6,32,35,38,7,41,46,52,59,64,21,24,29,27,28,30,18,19,20])).
% 1.51/1.64 cnf(67,plain,
% 1.51/1.64 (P3(x671,x672,f5(x671,x672))),
% 1.51/1.64 inference(rename_variables,[],[7])).
% 1.51/1.64 cnf(69,plain,
% 1.51/1.64 (P2(f2(a1,a1),a1,a1)),
% 1.51/1.64 inference(scs_inference,[],[2,39,47,53,57,6,32,35,38,7,41,46,52,59,64,21,24,29,27,28,30,18,19,20,17])).
% 1.51/1.64 cnf(72,plain,
% 1.51/1.65 (P1(f5(a1,x721),f2(f5(a1,x721),f5(a1,x721)))),
% 1.51/1.65 inference(scs_inference,[],[2,39,47,53,57,6,32,35,38,7,41,46,52,59,64,67,21,24,29,27,28,30,18,19,20,17,22])).
% 1.51/1.65 cnf(73,plain,
% 1.51/1.65 (P3(x731,x732,f5(x731,x732))),
% 1.51/1.65 inference(rename_variables,[],[7])).
% 1.51/1.65 cnf(75,plain,
% 1.51/1.65 (P3(f5(x751,x751),x751,f5(x751,f5(x751,x751)))),
% 1.51/1.65 inference(scs_inference,[],[2,39,47,53,57,6,32,35,38,7,41,46,52,59,64,67,73,58,21,24,29,27,28,30,18,19,20,17,22,25])).
% 1.51/1.65 cnf(91,plain,
% 1.51/1.65 (P2(x911,f2(f4(x911),a1),a1)),
% 1.51/1.65 inference(scs_inference,[],[4,31,16])).
% 1.51/1.65 cnf(92,plain,
% 1.51/1.65 (P1(x921,f2(x921,a1))),
% 1.51/1.65 inference(rename_variables,[],[31])).
% 1.51/1.65 cnf(94,plain,
% 1.51/1.65 (P2(f2(x941,a1),f4(x941),a1)),
% 1.51/1.65 inference(scs_inference,[],[4,31,92,16,17])).
% 1.51/1.65 cnf(95,plain,
% 1.51/1.65 (P1(x951,f2(x951,a1))),
% 1.51/1.65 inference(rename_variables,[],[31])).
% 1.51/1.65 cnf(97,plain,
% 1.51/1.65 (P2(x971,f4(x971),f2(a1,a1))),
% 1.51/1.65 inference(scs_inference,[],[4,31,92,95,16,17,15])).
% 1.51/1.65 cnf(98,plain,
% 1.51/1.65 (P1(x981,f2(x981,a1))),
% 1.51/1.65 inference(rename_variables,[],[31])).
% 1.51/1.65 cnf(100,plain,
% 1.51/1.65 (P1(a1,f4(a1))),
% 1.51/1.65 inference(scs_inference,[],[4,3,31,92,95,16,17,15,21])).
% 1.51/1.65 cnf(101,plain,
% 1.51/1.65 (P2(a1,x1011,x1011)),
% 1.51/1.65 inference(rename_variables,[],[3])).
% 1.51/1.65 cnf(102,plain,
% 1.51/1.65 (P2(x1021,f4(x1021),a1)),
% 1.51/1.65 inference(rename_variables,[],[4])).
% 1.51/1.65 cnf(107,plain,
% 1.51/1.65 (P2(a1,x1071,f2(x1071,a1))),
% 1.51/1.65 inference(scs_inference,[],[75,4,102,5,3,31,92,95,98,6,16,17,15,21,19,23])).
% 1.51/1.65 cnf(109,plain,
% 1.51/1.65 (P2(x1091,f4(x1091),a1)),
% 1.51/1.65 inference(rename_variables,[],[4])).
% 1.51/1.65 cnf(111,plain,
% 1.51/1.65 (P2(f4(a1),f4(a1),a1)),
% 1.51/1.65 inference(scs_inference,[],[75,4,102,109,5,3,101,31,92,95,98,6,16,17,15,21,19,23,24])).
% 1.51/1.65 cnf(132,plain,
% 1.51/1.65 (P3(f2(f2(a1,a1),a1),x1321,f5(a1,x1321))),
% 1.51/1.65 inference(scs_inference,[],[66,31,20])).
% 1.51/1.65 cnf(133,plain,
% 1.51/1.65 (P1(x1331,f2(x1331,a1))),
% 1.51/1.65 inference(rename_variables,[],[31])).
% 1.51/1.65 cnf(136,plain,
% 1.51/1.65 (P1(x1361,f2(x1361,a1))),
% 1.51/1.65 inference(rename_variables,[],[31])).
% 1.51/1.65 cnf(140,plain,
% 1.51/1.65 (P2(f4(x1401),f2(x1401,a1),a1)),
% 1.51/1.65 inference(scs_inference,[],[66,5,100,31,133,136,20,17,15,16])).
% 1.51/1.65 cnf(143,plain,
% 1.51/1.65 (P1(f5(a1,x1431),f5(f2(a1,a1),x1431))),
% 1.51/1.65 inference(scs_inference,[],[66,5,100,31,133,136,7,20,17,15,16,22])).
% 1.51/1.65 cnf(146,plain,
% 1.51/1.65 (P1(a1,f4(f2(a1,a1)))),
% 1.51/1.65 inference(scs_inference,[],[66,5,34,100,31,133,136,7,20,17,15,16,22,21])).
% 1.51/1.65 cnf(147,plain,
% 1.51/1.65 (P2(x1471,f2(a1,a1),x1471)),
% 1.51/1.65 inference(rename_variables,[],[34])).
% 1.51/1.65 cnf(148,plain,
% 1.51/1.65 (P2(f4(x1481),x1481,a1)),
% 1.51/1.65 inference(rename_variables,[],[5])).
% 1.51/1.65 cnf(150,plain,
% 1.51/1.65 (P3(f2(a1,a1),f4(a1),f5(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[66,5,34,100,31,133,136,7,20,17,15,16,22,21,19])).
% 1.61/1.65 cnf(151,plain,
% 1.61/1.65 (P3(f2(a1,a1),x1511,f5(a1,x1511))),
% 1.61/1.65 inference(rename_variables,[],[66])).
% 1.61/1.65 cnf(158,plain,
% 1.61/1.65 (P2(f4(x1581),x1581,a1)),
% 1.61/1.65 inference(rename_variables,[],[5])).
% 1.61/1.65 cnf(159,plain,
% 1.61/1.65 (P2(a1,x1591,x1591)),
% 1.61/1.65 inference(rename_variables,[],[3])).
% 1.61/1.65 cnf(161,plain,
% 1.61/1.65 (P2(f4(x1611),x1611,f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[66,151,5,148,158,4,3,159,34,147,72,100,31,133,136,7,20,17,15,16,22,21,19,18,23,24])).
% 1.61/1.65 cnf(177,plain,
% 1.61/1.65 (P1(f5(a1,x1771),f5(f2(a1,a1),x1771))),
% 1.61/1.65 inference(rename_variables,[],[143])).
% 1.61/1.65 cnf(178,plain,
% 1.61/1.65 (P2(f5(x1781,a1),f5(x1781,a1),f5(x1781,a1))),
% 1.61/1.65 inference(rename_variables,[],[43])).
% 1.61/1.65 cnf(181,plain,
% 1.61/1.65 (P3(x1811,f2(a1,a1),f5(x1811,a1))),
% 1.61/1.65 inference(rename_variables,[],[63])).
% 1.61/1.65 cnf(184,plain,
% 1.61/1.65 (P1(f5(a1,x1841),f5(f2(a1,a1),x1841))),
% 1.61/1.65 inference(rename_variables,[],[143])).
% 1.61/1.65 cnf(185,plain,
% 1.61/1.65 (P2(f5(x1851,a1),f5(x1851,a1),f5(x1851,a1))),
% 1.61/1.65 inference(rename_variables,[],[43])).
% 1.61/1.65 cnf(187,plain,
% 1.61/1.65 (P2(x1871,f4(x1871),f4(f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[63,43,178,4,143,177,146,17,20,16,15])).
% 1.61/1.65 cnf(189,plain,
% 1.61/1.65 (P1(f5(x1891,a1),f5(x1891,f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[63,181,43,178,4,143,177,146,7,17,20,16,15,22])).
% 1.61/1.65 cnf(190,plain,
% 1.61/1.65 (P3(x1901,x1902,f5(x1901,x1902))),
% 1.61/1.65 inference(rename_variables,[],[7])).
% 1.61/1.65 cnf(192,plain,
% 1.61/1.65 (P1(a1,f2(f4(a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[63,181,43,178,4,143,177,107,146,7,17,20,16,15,22,21])).
% 1.61/1.65 cnf(194,plain,
% 1.61/1.65 (P2(x1941,f4(x1941),a1)),
% 1.61/1.65 inference(rename_variables,[],[4])).
% 1.61/1.65 cnf(201,plain,
% 1.61/1.65 (P3(x2011,f2(a1,a1),f5(x2011,a1))),
% 1.61/1.65 inference(rename_variables,[],[63])).
% 1.61/1.65 cnf(205,plain,
% 1.61/1.65 (P2(x2051,f4(x2051),a1)),
% 1.61/1.65 inference(rename_variables,[],[4])).
% 1.61/1.65 cnf(208,plain,
% 1.61/1.65 (P3(x2081,f5(a1,a1),f5(f5(x2081,a1),f4(a1)))),
% 1.61/1.65 inference(scs_inference,[],[63,181,201,66,150,43,178,4,194,5,161,143,177,184,107,146,7,190,17,20,16,15,22,21,19,18,23,26])).
% 1.61/1.65 cnf(211,plain,
% 1.61/1.65 (P2(f5(x2111,a1),a1,a1)),
% 1.61/1.65 inference(scs_inference,[],[63,181,201,66,150,43,178,185,4,194,205,5,161,143,177,184,107,146,7,190,17,20,16,15,22,21,19,18,23,26,24])).
% 1.61/1.65 cnf(227,plain,
% 1.61/1.65 (P3(x2271,f2(a1,a1),f5(x2271,a1))),
% 1.61/1.65 inference(rename_variables,[],[63])).
% 1.61/1.65 cnf(229,plain,
% 1.61/1.65 (P2(x2291,f4(x2291),f2(f4(a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[63,4,192,20,15])).
% 1.61/1.65 cnf(232,plain,
% 1.61/1.65 (P1(f5(x2321,a1),f5(x2321,f2(a1,a1)))),
% 1.61/1.65 inference(rename_variables,[],[189])).
% 1.61/1.65 cnf(233,plain,
% 1.61/1.65 (P2(f5(a1,x2331),f5(a1,x2331),f5(a1,x2331))),
% 1.61/1.65 inference(rename_variables,[],[49])).
% 1.61/1.65 cnf(237,plain,
% 1.61/1.65 (P2(f5(a1,x2371),f5(a1,x2371),f5(a1,x2371))),
% 1.61/1.65 inference(rename_variables,[],[49])).
% 1.61/1.65 cnf(239,plain,
% 1.61/1.65 (P1(f2(f4(a1),a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[63,49,233,4,3,189,232,91,192,20,15,17,16,21])).
% 1.61/1.65 cnf(243,plain,
% 1.61/1.65 (P3(f2(a1,a1),f2(f4(a1),a1),f5(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[63,66,49,233,4,3,189,232,91,192,20,15,17,16,21,19])).
% 1.61/1.65 cnf(254,plain,
% 1.61/1.65 (P2(f5(a1,x2541),a1,a1)),
% 1.61/1.65 inference(scs_inference,[],[63,227,66,49,233,237,4,3,97,189,232,91,192,72,34,20,15,17,16,21,19,18,23,24])).
% 1.61/1.65 cnf(268,plain,
% 1.61/1.65 (P1(f5(x2681,a1),f5(x2681,f2(a1,a1)))),
% 1.61/1.65 inference(rename_variables,[],[189])).
% 1.61/1.65 cnf(273,plain,
% 1.61/1.65 (P3(f2(x2731,a1),f2(a1,a1),f5(x2731,a1))),
% 1.61/1.65 inference(scs_inference,[],[63,43,111,189,268,100,31,15,16,17,20])).
% 1.61/1.65 cnf(274,plain,
% 1.61/1.65 (P1(x2741,f2(x2741,a1))),
% 1.61/1.65 inference(rename_variables,[],[31])).
% 1.61/1.65 cnf(276,plain,
% 1.61/1.65 (P1(f5(x2761,a1),f2(f5(x2761,a1),f5(x2761,a1)))),
% 1.61/1.65 inference(scs_inference,[],[63,43,111,189,268,100,31,6,15,16,17,20,21])).
% 1.61/1.65 cnf(279,plain,
% 1.61/1.65 (P3(x2791,f2(f2(a1,a1),a1),f5(x2791,a1))),
% 1.61/1.65 inference(scs_inference,[],[63,43,111,189,268,100,31,274,6,15,16,17,20,21,19])).
% 1.61/1.65 cnf(284,plain,
% 1.61/1.65 (P2(f5(x2841,a1),f4(f5(x2841,a1)),f5(x2841,a1))),
% 1.61/1.65 inference(scs_inference,[],[8,63,43,111,239,97,189,268,100,31,274,6,34,15,16,17,20,21,19,18,23])).
% 1.61/1.65 cnf(302,plain,
% 1.61/1.65 (P1(f5(x3021,a1),f2(f5(x3021,a1),f5(x3021,a1)))),
% 1.61/1.65 inference(rename_variables,[],[276])).
% 1.61/1.65 cnf(303,plain,
% 1.61/1.65 (P2(f5(a1,x3031),f5(a1,x3031),f5(a1,x3031))),
% 1.61/1.65 inference(rename_variables,[],[49])).
% 1.61/1.65 cnf(306,plain,
% 1.61/1.65 (P1(f5(x3061,a1),f2(f5(x3061,a1),f5(x3061,a1)))),
% 1.61/1.65 inference(rename_variables,[],[276])).
% 1.61/1.65 cnf(307,plain,
% 1.61/1.65 (P2(f5(a1,x3071),f5(a1,x3071),f5(a1,x3071))),
% 1.61/1.65 inference(rename_variables,[],[49])).
% 1.61/1.65 cnf(312,plain,
% 1.61/1.65 (P3(x3121,f2(a1,a1),f2(f5(x3121,a1),f5(x3121,a1)))),
% 1.61/1.65 inference(scs_inference,[],[63,49,303,307,276,302,306,31,16,17,15,18])).
% 1.61/1.65 cnf(336,plain,
% 1.61/1.65 (P2(f4(a1),x3361,x3361)),
% 1.61/1.65 inference(scs_inference,[],[100,3,17])).
% 1.61/1.65 cnf(339,plain,
% 1.61/1.65 (P2(a1,x3391,x3391)),
% 1.61/1.65 inference(rename_variables,[],[3])).
% 1.61/1.65 cnf(343,plain,
% 1.61/1.65 (P1(f4(a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[111,100,146,3,339,4,239,17,16,15,21])).
% 1.61/1.65 cnf(347,plain,
% 1.61/1.65 (P3(x3471,f2(a1,a1),f2(f5(x3471,a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[63,111,100,146,3,339,4,239,31,17,16,15,21,18])).
% 1.61/1.65 cnf(366,plain,
% 1.61/1.65 (P1(f5(x3661,a1),f5(f2(x3661,a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[273,63,22])).
% 1.61/1.65 cnf(370,plain,
% 1.61/1.65 (P1(x3701,f2(x3701,a1))),
% 1.61/1.65 inference(rename_variables,[],[31])).
% 1.61/1.65 cnf(372,plain,
% 1.61/1.65 (P2(f4(a1),f4(a1),f2(f4(a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[273,63,43,111,192,31,22,16,15])).
% 1.61/1.65 cnf(374,plain,
% 1.61/1.65 (P2(f2(f4(a1),a1),x3741,x3741)),
% 1.61/1.65 inference(scs_inference,[],[273,63,43,111,192,3,31,22,16,15,17])).
% 1.61/1.65 cnf(376,plain,
% 1.61/1.65 (P3(f2(f2(x3761,a1),a1),f2(a1,a1),f5(x3761,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,63,43,111,192,3,31,370,22,16,15,17,20])).
% 1.61/1.65 cnf(377,plain,
% 1.61/1.65 (P1(x3771,f2(x3771,a1))),
% 1.61/1.65 inference(rename_variables,[],[31])).
% 1.61/1.65 cnf(379,plain,
% 1.61/1.65 (P1(f4(a1),f4(f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[273,63,43,111,192,3,187,31,370,22,16,15,17,20,21])).
% 1.61/1.65 cnf(383,plain,
% 1.61/1.65 (P3(f2(x3831,a1),f2(f2(a1,a1),a1),f5(x3831,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,63,43,111,192,3,187,31,370,377,22,16,15,17,20,21,19])).
% 1.61/1.65 cnf(391,plain,
% 1.61/1.65 (P2(f5(x3911,a1),f2(a1,a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[8,273,150,63,43,111,7,192,3,187,343,97,31,370,377,22,16,15,17,20,21,19,18,26,24])).
% 1.61/1.65 cnf(404,plain,
% 1.61/1.65 (P1(f5(x4041,a1),f5(f2(x4041,a1),f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[273,7,22])).
% 1.61/1.65 cnf(414,plain,
% 1.61/1.65 (P1(f2(a1,a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[273,43,111,7,146,3,34,379,366,22,16,17,15,21])).
% 1.61/1.65 cnf(418,plain,
% 1.61/1.65 (P3(f2(x4181,a1),a1,f5(x4181,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,43,111,7,146,3,34,379,366,22,16,17,15,21,19])).
% 1.61/1.65 cnf(437,plain,
% 1.61/1.65 (P1(f5(x4371,a1),f5(f2(x4371,a1),f2(a1,a1)))),
% 1.61/1.65 inference(rename_variables,[],[404])).
% 1.61/1.65 cnf(443,plain,
% 1.61/1.65 (P2(x4431,f4(x4431),a1)),
% 1.61/1.65 inference(rename_variables,[],[4])).
% 1.61/1.65 cnf(445,plain,
% 1.61/1.65 (P1(f5(x4451,a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[43,146,284,4,443,404,437,16,15,17,21])).
% 1.61/1.65 cnf(457,plain,
% 1.61/1.65 (P2(f4(a1),a1,f2(a1,f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[273,63,383,376,208,43,111,146,284,4,443,6,31,404,437,140,16,15,17,21,19,18,26,24])).
% 1.61/1.65 cnf(475,plain,
% 1.61/1.65 (P2(f5(x4751,a1),f5(x4751,a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[63,43,445,20,15])).
% 1.61/1.65 cnf(481,plain,
% 1.61/1.65 (P2(f5(x4811,a1),f5(f2(x4811,a1),a1),f5(x4811,a1))),
% 1.61/1.65 inference(scs_inference,[],[63,43,31,445,366,20,15,17,16])).
% 1.61/1.65 cnf(484,plain,
% 1.61/1.65 (P1(f5(x4841,a1),f2(f4(a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[63,43,284,229,31,445,366,20,15,17,16,21])).
% 1.61/1.65 cnf(487,plain,
% 1.61/1.65 (P3(f2(x4871,a1),f4(a1),f5(x4871,a1))),
% 1.61/1.65 inference(scs_inference,[],[63,418,43,284,100,229,31,445,366,20,15,17,16,21,19])).
% 1.61/1.65 cnf(497,plain,
% 1.61/1.65 (~P3(a3,f5(x4971,a1),f5(x4971,a1))),
% 1.61/1.65 inference(scs_inference,[],[8,63,418,43,5,284,100,3,94,229,31,414,445,366,20,15,17,16,21,19,18,24,23,30])).
% 1.61/1.65 cnf(499,plain,
% 1.61/1.65 (P3(f5(x4991,a1),x4992,f5(x4991,a1))+~P3(a1,x4992,a1)),
% 1.61/1.65 inference(scs_inference,[],[8,63,418,43,5,284,100,3,94,229,31,414,445,366,20,15,17,16,21,19,18,24,23,30,25])).
% 1.61/1.65 cnf(511,plain,
% 1.61/1.65 (P1(f5(x5111,a1),f2(f4(a1),a1))),
% 1.61/1.65 inference(rename_variables,[],[484])).
% 1.61/1.65 cnf(514,plain,
% 1.61/1.65 (P1(f5(x5141,a1),f2(f4(a1),a1))),
% 1.61/1.65 inference(rename_variables,[],[484])).
% 1.61/1.65 cnf(519,plain,
% 1.61/1.65 (P1(f5(x5191,a1),f4(f2(a1,a1)))),
% 1.61/1.65 inference(scs_inference,[],[43,284,187,484,511,404,15,16,17,21])).
% 1.61/1.65 cnf(524,plain,
% 1.61/1.65 (P3(f2(x5241,a1),f2(a1,a1),f2(f4(a1),a1))),
% 1.61/1.65 inference(scs_inference,[],[273,418,43,284,192,187,484,511,514,404,15,16,17,21,19,18])).
% 1.61/1.65 cnf(532,plain,
% 1.61/1.65 (P3(a1,f2(a1,a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[273,418,243,43,284,192,374,187,372,484,511,514,475,404,15,16,17,21,19,18,25,24,29])).
% 1.61/1.65 cnf(535,plain,
% 1.61/1.65 (P3(a1,f2(a1,a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,418,243,43,284,192,374,187,372,484,511,514,475,404,15,16,17,21,19,18,25,24,29,61])).
% 1.61/1.65 cnf(537,plain,
% 1.61/1.65 (P3(f5(x5371,a1),f2(a1,a1),f5(x5371,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,418,243,43,284,192,374,187,372,484,511,514,475,404,15,16,17,21,19,18,25,24,29,61,499])).
% 1.61/1.65 cnf(550,plain,
% 1.61/1.65 (P1(f5(x5501,a1),f4(f2(a1,a1)))),
% 1.61/1.65 inference(rename_variables,[],[519])).
% 1.61/1.65 cnf(558,plain,
% 1.61/1.65 (P1(f5(x5581,a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[43,284,519,550,276,97,16,17,15,21])).
% 1.61/1.65 cnf(563,plain,
% 1.61/1.65 (P3(a1,f2(a1,a1),f4(a1))),
% 1.61/1.65 inference(scs_inference,[],[418,532,43,284,100,146,519,550,276,97,16,17,15,21,19,18])).
% 1.61/1.65 cnf(566,plain,
% 1.61/1.65 (P3(x5661,f2(a1,a1),f5(x5661,a1))),
% 1.61/1.65 inference(rename_variables,[],[63])).
% 1.61/1.65 cnf(576,plain,
% 1.61/1.65 (~P3(f4(a1),f5(x5761,a1),f4(a1))+P3(f5(x5761,a1),a1,a1)),
% 1.61/1.65 inference(scs_inference,[],[418,63,566,487,535,532,43,111,284,2,100,146,519,550,457,475,276,97,16,17,15,21,19,18,26,24,20,25,30])).
% 1.61/1.65 cnf(588,plain,
% 1.61/1.65 (P2(f2(a1,a1),f5(x5881,a1),f5(x5881,a1))),
% 1.61/1.65 inference(scs_inference,[],[279,43,100,558,20,17])).
% 1.61/1.65 cnf(589,plain,
% 1.61/1.65 (P1(f5(x5891,a1),f2(a1,a1))),
% 1.61/1.65 inference(rename_variables,[],[558])).
% 1.61/1.65 cnf(599,plain,
% 1.61/1.65 (P3(f2(x5991,a1),f5(f2(a1,a1),a1),f5(x5991,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,100,192,445,558,589,20,17,15,19,18,26])).
% 1.61/1.65 cnf(605,plain,
% 1.61/1.65 (P2(f4(a1),f2(x6051,a1),x6051)),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,5,3,100,192,107,445,558,589,20,17,15,19,18,26,23,24])).
% 1.61/1.65 cnf(609,plain,
% 1.61/1.65 (P3(f2(a1,a1),f2(a1,a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,5,3,100,192,107,445,558,589,20,17,15,19,18,26,23,24,29])).
% 1.61/1.65 cnf(611,plain,
% 1.61/1.65 (P3(f2(f2(a1,a1),a1),a1,a1)),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,5,3,100,192,107,475,445,558,589,20,17,15,19,18,26,23,24,29,30])).
% 1.61/1.65 cnf(614,plain,
% 1.61/1.65 (P3(f2(f2(a1,a1),a1),a1,f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,5,3,100,192,107,475,445,558,589,20,17,15,19,18,26,23,24,29,30,61])).
% 1.61/1.65 cnf(616,plain,
% 1.61/1.65 (P1(f2(x6161,a1),x6161)),
% 1.61/1.65 inference(scs_inference,[],[273,66,279,63,537,532,43,5,3,336,100,192,107,475,445,558,589,20,17,15,19,18,26,23,24,29,30,61,21])).
% 1.61/1.65 cnf(628,plain,
% 1.61/1.65 (P2(a1,f2(x6281,a1),x6281)),
% 1.61/1.65 inference(scs_inference,[],[43,3,616,366,17,15])).
% 1.61/1.65 cnf(631,plain,
% 1.61/1.65 (P2(f4(f2(x6311,a1)),x6311,a1)),
% 1.61/1.65 inference(scs_inference,[],[43,5,3,616,366,17,15,16])).
% 1.61/1.65 cnf(642,plain,
% 1.61/1.65 (P3(f4(a1),f2(a1,a1),f4(a1))),
% 1.61/1.65 inference(scs_inference,[],[418,66,63,532,609,563,43,5,3,146,616,558,366,17,15,16,19,18,26,25])).
% 1.61/1.65 cnf(656,plain,
% 1.61/1.65 (P1(f4(f2(a1,a1)),a1)),
% 1.61/1.65 inference(scs_inference,[],[2,631,21])).
% 1.61/1.65 cnf(660,plain,
% 1.61/1.65 (P3(f2(x6601,a1),f2(a1,a1),a1)),
% 1.61/1.65 inference(scs_inference,[],[524,2,239,631,21,18])).
% 1.61/1.65 cnf(665,plain,
% 1.61/1.65 (P3(f2(x6651,a1),f2(a1,a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[524,111,3,2,605,239,631,21,18,24,61])).
% 1.61/1.65 cnf(677,plain,
% 1.61/1.65 (P1(f4(f4(a1)),a1)),
% 1.61/1.65 inference(scs_inference,[],[336,4,21])).
% 1.61/1.65 cnf(692,plain,
% 1.61/1.65 (P1(a1,f5(a1,x6921))),
% 1.61/1.65 inference(scs_inference,[],[100,254,2,16,21])).
% 1.61/1.65 cnf(730,plain,
% 1.61/1.65 (P1(f4(f4(a1)),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[532,100,5,336,97,692,20,16,21])).
% 1.61/1.65 cnf(737,plain,
% 1.61/1.65 (P3(f2(a1,a1),a1,a1)),
% 1.61/1.65 inference(scs_inference,[],[273,532,660,100,5,336,189,97,692,20,16,21,18,26])).
% 1.61/1.65 cnf(759,plain,
% 1.61/1.65 (P2(a1,x7591,x7591)),
% 1.61/1.65 inference(rename_variables,[],[3])).
% 1.61/1.65 cnf(767,plain,
% 1.61/1.65 (P1(f4(a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[537,599,737,445,3,759,189,97,730,61,15,20,19,21])).
% 1.61/1.65 cnf(787,plain,
% 1.61/1.65 (P1(x7871,f2(x7871,a1))),
% 1.61/1.65 inference(rename_variables,[],[31])).
% 1.61/1.65 cnf(789,plain,
% 1.61/1.65 (P2(f4(a1),f4(a1),f2(a1,a1))),
% 1.61/1.65 inference(scs_inference,[],[111,31,787,17,15])).
% 1.61/1.65 cnf(796,plain,
% 1.61/1.65 (P1(a1,f5(x7961,a1))),
% 1.61/1.65 inference(scs_inference,[],[532,111,146,31,787,211,2,17,15,20,16,21])).
% 1.61/1.66 cnf(806,plain,
% 1.61/1.66 (P2(f5(x8061,a1),x8062,f2(x8062,a1))),
% 1.61/1.66 inference(scs_inference,[],[8,532,279,132,111,146,31,787,211,2,3,628,677,497,17,15,20,16,21,18,26,24])).
% 1.61/1.66 cnf(828,plain,
% 1.61/1.66 (P1(f2(a1,a1),f5(x8281,a1))),
% 1.61/1.66 inference(scs_inference,[],[537,111,558,391,2,34,656,796,17,15,20,21])).
% 1.61/1.66 cnf(850,plain,
% 1.61/1.66 (~P3(f2(a1,a1),f5(a3,a1),f2(a1,a1))),
% 1.61/1.66 inference(scs_inference,[],[8,487,537,279,642,665,111,100,558,391,211,336,2,3,4,611,34,656,806,789,796,17,15,20,21,16,18,26,24,23,30,576,25])).
% 1.61/1.66 cnf(868,plain,
% 1.61/1.66 (P1(a1,f2(f4(a1),f4(a1)))),
% 1.61/1.66 inference(scs_inference,[],[418,537,63,111,31,616,192,391,211,2,6,828,730,22,17,15,20,16,19,21])).
% 1.61/1.66 cnf(881,plain,
% 1.61/1.66 (~P3(a1,f5(a3,a1),a1)),
% 1.61/1.66 inference(scs_inference,[],[418,537,63,614,75,850,111,31,616,192,558,391,211,2,6,588,828,730,22,17,15,20,16,19,21,18,26,24,25])).
% 1.61/1.66 cnf(936,plain,
% 1.61/1.66 (P1(f5(x9361,a1),a1)),
% 1.61/1.66 inference(rename_variables,[],[445])).
% 1.61/1.66 cnf(943,plain,
% 1.61/1.66 (P3(f5(x9431,a1),f5(x9432,a1),f5(x9431,a1))),
% 1.61/1.66 inference(scs_inference,[],[537,481,445,936,211,868,828,17,15,16,19])).
% 1.61/1.66 cnf(968,plain,
% 1.61/1.66 (P1(a1,f2(f5(a1,a1),f5(a1,a1)))),
% 1.61/1.66 inference(scs_inference,[],[532,312,22])).
% 1.61/1.66 cnf(974,plain,
% 1.61/1.66 (P2(f2(f4(a1),a1),x9741,x9741)),
% 1.61/1.66 inference(rename_variables,[],[374])).
% 1.61/1.66 cnf(977,plain,
% 1.61/1.66 (P2(f2(f4(a1),a1),x9771,x9771)),
% 1.61/1.66 inference(rename_variables,[],[374])).
% 1.61/1.66 cnf(982,plain,
% 1.61/1.66 (P1(f2(a1,a1),f2(f4(a1),a1))),
% 1.61/1.66 inference(scs_inference,[],[532,537,312,146,616,374,974,977,628,276,34,767,22,17,15,16,20,21])).
% 1.61/1.66 cnf(986,plain,
% 1.61/1.66 (P3(a1,a1,a1)),
% 1.61/1.66 inference(scs_inference,[],[532,537,312,146,616,374,974,977,628,276,34,767,22,17,15,16,20,21,19])).
% 1.61/1.66 cnf(1031,plain,
% 1.61/1.66 ($false),
% 1.61/1.66 inference(scs_inference,[],[418,532,537,881,986,943,347,111,192,69,628,366,519,107,692,982,968,22,17,15,20,21,16,19,18,26,24,25]),
% 1.61/1.66 ['proof']).
% 1.61/1.66 % SZS output end Proof
% 1.61/1.66 % Total time :1.030000s
%------------------------------------------------------------------------------