%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG038-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 : n020.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:48 EDT 2024
% Result : Unsatisfiable 0.53s 0.73s
% Output : CNFRefutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : RNG038-2 : TPTP v8.2.0. Released v1.0.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n020.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 : Tue Jun 18 14:36:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.57 start to proof:theBenchmark
% 0.53/0.72 %-------------------------------------------
% 0.53/0.72 % File :CSE---1.7
% 0.53/0.72 % Problem :theBenchmark
% 0.53/0.72 % Transform :cnf
% 0.53/0.72 % Format :tptp:raw
% 0.53/0.72 % Command :java -jar mcs_scs.jar %d %s
% 0.53/0.72
% 0.53/0.72 % Result :Theorem 0.110000s
% 0.53/0.72 % Output :CNFRefutation 0.110000s
% 0.53/0.72 %-------------------------------------------
% 0.53/0.72 %--------------------------------------------------------------------------
% 0.53/0.72 % File : RNG038-2 : TPTP v8.2.0. Released v1.0.0.
% 0.53/0.72 % Domain : Ring Theory
% 0.53/0.72 % Problem : Ring property 1
% 0.53/0.72 % Version : [Wos65] axioms : Reduced > Incomplete.
% 0.53/0.72 % English :
% 0.53/0.72
% 0.53/0.72 % Refs : [Wos65] Wos (1965), Unpublished Note
% 0.53/0.72 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 0.53/0.72 % Source : [SPRFN]
% 0.53/0.72 % Names : Problem 27 [Wos65]
% 0.53/0.72 % : wos27 [WM76]
% 0.53/0.72
% 0.53/0.72 % Status : Unsatisfiable
% 0.53/0.72 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.11 v2.1.0, 0.00 v2.0.0
% 0.53/0.72 % Syntax : Number of clauses : 30 ( 9 unt; 0 nHn; 21 RR)
% 0.53/0.72 % Number of literals : 79 ( 0 equ; 51 neg)
% 0.53/0.72 % Maximal clause size : 5 ( 2 avg)
% 0.53/0.72 % Maximal term depth : 2 ( 1 avg)
% 0.53/0.72 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 0.53/0.72 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 0.53/0.72 % Number of variables : 105 ( 2 sgn)
% 0.53/0.72 % SPC : CNF_UNS_RFO_NEQ_HRN
% 0.53/0.72
% 0.53/0.72 % Comments :
% 0.53/0.72 %--------------------------------------------------------------------------
% 0.53/0.72 %----Don't Include ring theory axioms
% 0.53/0.72 %include('Axioms/RNG001-0.ax').
% 0.53/0.72 %--------------------------------------------------------------------------
% 0.53/0.72 %----Equality axioms for additive operator
% 0.53/0.72 cnf(additive_inverse_substitution,axiom,
% 0.53/0.72 ( ~ equalish(X,Y)
% 0.53/0.72 | equalish(additive_inverse(X),additive_inverse(Y)) ) ).
% 0.53/0.72
% 0.53/0.72 cnf(add_substitution1,axiom,
% 0.53/0.72 ( ~ equalish(X,Y)
% 0.53/0.72 | equalish(add(X,W),add(Y,W)) ) ).
% 0.53/0.72
% 0.53/0.72 %----This axiom omited in this version
% 0.53/0.72 %input_clause(add_substitution2,axiom,
% 0.53/0.72 % [--equalish(X,Y),
% 0.53/0.72 % ++equalish(add(W,X),add(W,Y))]).
% 0.53/0.72
% 0.53/0.72 cnf(sum_substitution1,axiom,
% 0.53/0.72 ( ~ equalish(X,Y)
% 0.53/0.72 | ~ sum(X,W,Z)
% 0.53/0.72 | sum(Y,W,Z) ) ).
% 0.53/0.72
% 0.53/0.72 cnf(sum_substitution2,axiom,
% 0.53/0.72 ( ~ equalish(X,Y)
% 0.53/0.72 | ~ sum(W,X,Z)
% 0.53/0.72 | sum(W,Y,Z) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(sum_substitution3,axiom,
% 0.53/0.73 ( ~ equalish(X,Y)
% 0.53/0.73 | ~ sum(W,Z,X)
% 0.53/0.73 | sum(W,Z,Y) ) ).
% 0.53/0.73
% 0.53/0.73 %----Equality axioms for multiplicative operator
% 0.53/0.73 cnf(multiply_substitution1,axiom,
% 0.53/0.73 ( ~ equalish(X,Y)
% 0.53/0.73 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 0.53/0.73
% 0.53/0.73 %----This axiom omited in this version
% 0.53/0.73 %input_clause(multiply_substitution2,axiom,
% 0.53/0.73 % [--equalish(X,Y),
% 0.53/0.73 % ++equalish(multiply(W,X),multiply(W,Y))]).
% 0.53/0.73
% 0.53/0.73 cnf(product_substitution1,axiom,
% 0.53/0.73 ( ~ equalish(X,Y)
% 0.53/0.73 | ~ product(X,W,Z)
% 0.53/0.73 | product(Y,W,Z) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(product_substitution2,axiom,
% 0.53/0.73 ( ~ equalish(X,Y)
% 0.53/0.73 | ~ product(W,X,Z)
% 0.53/0.73 | product(W,Y,Z) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(product_substitution3,axiom,
% 0.53/0.73 ( ~ equalish(X,Y)
% 0.53/0.73 | ~ product(W,Z,X)
% 0.53/0.73 | product(W,Z,Y) ) ).
% 0.53/0.73
% 0.53/0.73 %----Not used in this version
% 0.53/0.73 %input_clause(additive_identity1,axiom,
% 0.53/0.73 % [++sum(additive_identity,X,X)]).
% 0.53/0.73
% 0.53/0.73 cnf(additive_identity2,axiom,
% 0.53/0.73 sum(X,additive_identity,X) ).
% 0.53/0.73
% 0.53/0.73 cnf(closure_of_multiplication,axiom,
% 0.53/0.73 product(X,Y,multiply(X,Y)) ).
% 0.53/0.73
% 0.53/0.73 cnf(closure_of_addition,axiom,
% 0.53/0.73 sum(X,Y,add(X,Y)) ).
% 0.53/0.73
% 0.53/0.73 %----Not used in this version
% 0.53/0.73 %input_clause(additive_inverse1,axiom,
% 0.53/0.73 % [++sum(additive_inverse(X),X,additive_identity)]).
% 0.53/0.73
% 0.53/0.73 cnf(additive_inverse2,axiom,
% 0.53/0.73 sum(X,additive_inverse(X),additive_identity) ).
% 0.53/0.73
% 0.53/0.73 cnf(associativity_of_addition1,axiom,
% 0.53/0.73 ( ~ sum(X,Y,U)
% 0.53/0.73 | ~ sum(Y,Z,V)
% 0.53/0.73 | ~ sum(U,Z,W)
% 0.53/0.73 | sum(X,V,W) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(associativity_of_addition2,axiom,
% 0.53/0.73 ( ~ sum(X,Y,U)
% 0.53/0.73 | ~ sum(Y,Z,V)
% 0.53/0.73 | ~ sum(X,V,W)
% 0.53/0.73 | sum(U,Z,W) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(commutativity_of_addition,axiom,
% 0.53/0.73 ( ~ sum(X,Y,Z)
% 0.53/0.73 | sum(Y,X,Z) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(associativity_of_multiplication1,axiom,
% 0.53/0.73 ( ~ product(X,Y,U)
% 0.53/0.73 | ~ product(Y,Z,V)
% 0.53/0.73 | ~ product(U,Z,W)
% 0.53/0.73 | product(X,V,W) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(associativity_of_multiplication2,axiom,
% 0.53/0.73 ( ~ product(X,Y,U)
% 0.53/0.73 | ~ product(Y,Z,V)
% 0.53/0.73 | ~ product(X,V,W)
% 0.53/0.73 | product(U,Z,W) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(distributivity1,axiom,
% 0.53/0.73 ( ~ product(X,Y,V1)
% 0.53/0.73 | ~ product(X,Z,V2)
% 0.53/0.73 | ~ sum(Y,Z,V3)
% 0.53/0.73 | ~ product(X,V3,V4)
% 0.53/0.73 | sum(V1,V2,V4) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(distributivity2,axiom,
% 0.53/0.73 ( ~ product(X,Y,V1)
% 0.53/0.73 | ~ product(X,Z,V2)
% 0.53/0.73 | ~ sum(Y,Z,V3)
% 0.53/0.73 | ~ sum(V1,V2,V4)
% 0.53/0.73 | product(X,V3,V4) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(distributivity3,axiom,
% 0.53/0.73 ( ~ product(Y,X,V1)
% 0.53/0.73 | ~ product(Z,X,V2)
% 0.53/0.73 | ~ sum(Y,Z,V3)
% 0.53/0.73 | ~ product(V3,X,V4)
% 0.53/0.73 | sum(V1,V2,V4) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(distributivity4,axiom,
% 0.53/0.73 ( ~ product(Y,X,V1)
% 0.53/0.73 | ~ product(Z,X,V2)
% 0.53/0.73 | ~ sum(Y,Z,V3)
% 0.53/0.73 | ~ sum(V1,V2,V4)
% 0.53/0.73 | product(V3,X,V4) ) ).
% 0.53/0.73
% 0.53/0.73 %-----Equality axioms for operators
% 0.53/0.73 cnf(addition_is_well_defined,axiom,
% 0.53/0.73 ( ~ sum(X,Y,U)
% 0.53/0.73 | ~ sum(X,Y,V)
% 0.53/0.73 | equalish(U,V) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(multiplication_is_well_defined,axiom,
% 0.53/0.73 ( ~ product(X,Y,U)
% 0.53/0.73 | ~ product(X,Y,V)
% 0.53/0.73 | equalish(U,V) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(multiplicative_identity1,axiom,
% 0.53/0.73 product(additive_identity,X,additive_identity) ).
% 0.53/0.73
% 0.53/0.73 cnf(multiplicative_identity2,axiom,
% 0.53/0.73 product(X,additive_identity,additive_identity) ).
% 0.53/0.73
% 0.53/0.73 cnf(some_property,hypothesis,
% 0.53/0.73 ( ~ equalish(X,additive_identity)
% 0.53/0.73 | product(X,h(X,Y),Y) ) ).
% 0.53/0.73
% 0.53/0.73 cnf(a_times_b,hypothesis,
% 0.53/0.73 product(a,b,additive_identity) ).
% 0.53/0.73
% 0.53/0.73 %----Proving either a or b is the additive_identity. Either clause will
% 0.53/0.73 %----do.
% 0.53/0.73 cnf(a_not_additive_identity,negated_conjecture,
% 0.53/0.73 ~ equalish(a,additive_identity) ).
% 0.53/0.73
% 0.53/0.73 cnf(prove_b_is_additive_identity,negated_conjecture,
% 0.53/0.73 ~ equalish(b,additive_identity) ).
% 0.53/0.73
% 0.53/0.73 %--------------------------------------------------------------------------
% 0.53/0.73 %-------------------------------------------
% 0.53/0.73 % Proof found
% 0.53/0.73 % SZS status Theorem for theBenchmark
% 0.53/0.73 % SZS output start Proof
% 0.53/0.73 %ClaNum:30(EqnAxiom:0)
% 0.53/0.73 %VarNum:213(SingletonVarNum:105)
% 0.53/0.73 %MaxLitNum:5
% 0.53/0.73 %MaxfuncDepth:1
% 0.53/0.73 %SharedTerms:6
% 0.53/0.73 %goalClause: 8 9
% 0.53/0.73 %singleGoalClaCount:2
% 0.53/0.73 [1]P1(a1,a2,a3)
% 0.53/0.73 [8]~P2(a1,a3)
% 0.53/0.73 [9]~P2(a2,a3)
% 0.53/0.73 [2]P1(x21,a3,a3)
% 0.53/0.73 [3]P1(a3,x31,a3)
% 0.53/0.73 [4]P3(x41,a3,x41)
% 0.53/0.73 [5]P3(x51,f5(x51),a3)
% 0.53/0.73 [6]P3(x61,x62,f4(x61,x62))
% 0.53/0.73 [7]P1(x71,x72,f6(x71,x72))
% 0.53/0.73 [10]~P2(x101,x102)+P2(f5(x101),f5(x102))
% 0.53/0.73 [13]P1(x131,f7(x131,x132),x132)+~P2(x131,a3)
% 0.53/0.73 [14]~P3(x142,x141,x143)+P3(x141,x142,x143)
% 0.53/0.73 [11]~P2(x111,x113)+P2(f4(x111,x112),f4(x113,x112))
% 0.53/0.73 [12]~P2(x121,x123)+P2(f6(x121,x122),f6(x123,x122))
% 0.53/0.73 [15]~P3(x151,x152,x154)+P3(x151,x152,x153)+~P2(x154,x153)
% 0.53/0.73 [16]~P3(x161,x164,x163)+P3(x161,x162,x163)+~P2(x164,x162)
% 0.53/0.73 [17]~P3(x174,x172,x173)+P3(x171,x172,x173)+~P2(x174,x171)
% 0.53/0.73 [18]~P1(x181,x182,x184)+P1(x181,x182,x183)+~P2(x184,x183)
% 0.53/0.73 [19]~P1(x191,x194,x193)+P1(x191,x192,x193)+~P2(x194,x192)
% 0.53/0.73 [20]~P1(x204,x202,x203)+P1(x201,x202,x203)+~P2(x204,x201)
% 0.53/0.73 [21]~P3(x213,x214,x211)+P2(x211,x212)+~P3(x213,x214,x212)
% 0.53/0.73 [22]~P1(x223,x224,x221)+P2(x221,x222)+~P1(x223,x224,x222)
% 0.53/0.73 [23]~P3(x236,x234,x231)+P3(x231,x232,x233)+~P3(x234,x232,x235)+~P3(x236,x235,x233)
% 0.53/0.73 [24]~P3(x241,x246,x244)+P3(x241,x242,x243)+~P3(x244,x245,x243)+~P3(x246,x245,x242)
% 0.53/0.73 [25]~P1(x256,x254,x251)+P1(x251,x252,x253)+~P1(x254,x252,x255)+~P1(x256,x255,x253)
% 0.53/0.73 [26]~P1(x261,x266,x264)+P1(x261,x262,x263)+~P1(x264,x265,x263)+~P1(x266,x265,x262)
% 0.53/0.73 [27]~P1(x277,x275,x272)+~P1(x277,x274,x271)+P3(x271,x272,x273)+~P3(x274,x275,x276)+~P1(x277,x276,x273)
% 0.53/0.73 [28]~P1(x285,x287,x282)+~P1(x284,x287,x281)+P3(x281,x282,x283)+~P3(x284,x285,x286)+~P1(x286,x287,x283)
% 0.53/0.73 [29]~P1(x297,x292,x295)+~P1(x296,x292,x294)+P1(x291,x292,x293)+~P3(x294,x295,x293)+~P3(x296,x297,x291)
% 0.53/0.73 [30]~P1(x301,x307,x305)+~P1(x301,x306,x304)+P1(x301,x302,x303)+~P3(x304,x305,x303)+~P3(x306,x307,x302)
% 0.53/0.73 %EqnAxiom
% 0.53/0.73
% 0.53/0.73 %-------------------------------------------
% 0.53/0.73 cnf(31,plain,
% 0.53/0.73 (P2(x311,x311)),
% 0.53/0.73 inference(scs_inference,[],[4,21])).
% 0.53/0.73 cnf(33,plain,
% 0.53/0.73 (P2(f6(x331,a3),a3)),
% 0.53/0.73 inference(scs_inference,[],[4,7,2,21,22])).
% 0.53/0.73 cnf(34,plain,
% 0.53/0.73 (P1(x341,a3,a3)),
% 0.53/0.73 inference(rename_variables,[],[2])).
% 0.53/0.73 cnf(35,plain,
% 0.53/0.73 (P1(x351,x352,f6(x351,x352))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(37,plain,
% 0.53/0.73 (P3(f6(x371,a3),a3,a3)),
% 0.53/0.73 inference(scs_inference,[],[4,7,2,21,22,15])).
% 0.53/0.73 cnf(38,plain,
% 0.53/0.73 (P3(x381,a3,x381)),
% 0.53/0.73 inference(rename_variables,[],[4])).
% 0.53/0.73 cnf(40,plain,
% 0.53/0.73 (P3(x401,a3,f4(x401,f6(x402,a3)))),
% 0.53/0.73 inference(scs_inference,[],[4,6,7,2,21,22,15,16])).
% 0.53/0.73 cnf(41,plain,
% 0.53/0.73 (P3(x411,x412,f4(x411,x412))),
% 0.53/0.73 inference(rename_variables,[],[6])).
% 0.53/0.73 cnf(43,plain,
% 0.53/0.73 (P3(a3,a3,f6(x431,a3))),
% 0.53/0.73 inference(scs_inference,[],[4,38,6,7,2,21,22,15,16,17])).
% 0.53/0.73 cnf(44,plain,
% 0.53/0.73 (P3(x441,a3,x441)),
% 0.53/0.73 inference(rename_variables,[],[4])).
% 0.53/0.73 cnf(46,plain,
% 0.53/0.73 (P1(x461,a3,f6(x461,f6(x462,a3)))),
% 0.53/0.73 inference(scs_inference,[],[4,38,6,7,35,2,21,22,15,16,17,19])).
% 0.53/0.73 cnf(47,plain,
% 0.53/0.73 (P1(x471,x472,f6(x471,x472))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(50,plain,
% 0.53/0.73 (P1(x501,x502,f6(x501,x502))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(52,plain,
% 0.53/0.73 (P3(x521,f4(a3,a3),x521)),
% 0.53/0.73 inference(scs_inference,[],[4,38,44,6,41,7,35,47,2,21,22,15,16,17,19,20,24])).
% 0.53/0.73 cnf(53,plain,
% 0.53/0.73 (P3(x531,x532,f4(x531,x532))),
% 0.53/0.73 inference(rename_variables,[],[6])).
% 0.53/0.73 cnf(55,plain,
% 0.53/0.73 (P1(f6(x551,a3),a3,f6(x551,a3))),
% 0.53/0.73 inference(scs_inference,[],[4,38,44,6,41,7,35,47,50,2,34,21,22,15,16,17,19,20,24,25])).
% 0.53/0.73 cnf(56,plain,
% 0.53/0.73 (P1(x561,x562,f6(x561,x562))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(57,plain,
% 0.53/0.73 (P1(x571,x572,f6(x571,x572))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(60,plain,
% 0.53/0.73 (P1(x601,f6(x601,x601),f6(f6(x601,x601),x601))),
% 0.53/0.73 inference(scs_inference,[],[4,38,44,6,41,7,35,47,50,57,56,2,34,21,22,15,16,17,19,20,24,25,26])).
% 0.53/0.73 cnf(62,plain,
% 0.53/0.73 (P1(x621,x622,f6(x621,x622))),
% 0.53/0.73 inference(rename_variables,[],[7])).
% 0.53/0.73 cnf(65,plain,
% 0.53/0.73 (P3(f6(x651,a3),f6(x651,a3),f6(x651,a3))),
% 0.53/0.73 inference(scs_inference,[],[4,38,44,6,41,7,35,47,50,57,62,56,2,34,21,22,15,16,17,19,20,24,25,26,27])).
% 0.53/0.73 cnf(68,plain,
% 0.53/0.74 (P1(x681,x682,f6(x681,x682))),
% 0.53/0.74 inference(rename_variables,[],[7])).
% 0.53/0.74 cnf(69,plain,
% 0.53/0.74 (P3(x691,a3,x691)),
% 0.53/0.74 inference(rename_variables,[],[4])).
% 0.53/0.74 cnf(74,plain,
% 0.53/0.74 (P1(x741,x742,f6(x741,x742))),
% 0.53/0.74 inference(rename_variables,[],[7])).
% 0.53/0.74 cnf(75,plain,
% 0.53/0.74 (P3(x751,a3,x751)),
% 0.53/0.74 inference(rename_variables,[],[4])).
% 0.53/0.74 cnf(78,plain,
% 0.53/0.74 (P3(x781,x782,f4(x781,x782))),
% 0.53/0.74 inference(rename_variables,[],[6])).
% 0.53/0.74 cnf(79,plain,
% 0.53/0.74 (P3(x791,a3,x791)),
% 0.53/0.74 inference(rename_variables,[],[4])).
% 0.53/0.74 cnf(81,plain,
% 0.53/0.74 (P1(x811,x812,f6(x811,x812))),
% 0.53/0.74 inference(rename_variables,[],[7])).
% 0.53/0.74 cnf(89,plain,
% 0.53/0.74 (P1(f6(x891,a3),f7(f6(x891,a3),x892),x892)),
% 0.53/0.74 inference(scs_inference,[],[4,38,44,69,75,79,6,41,53,78,7,35,47,50,57,62,68,74,81,56,2,34,21,22,15,16,17,19,20,24,25,26,27,28,29,30,13])).
% 0.53/0.74 cnf(97,plain,
% 0.53/0.74 (P2(x971,f4(x971,f4(a3,a3)))),
% 0.53/0.74 inference(scs_inference,[],[31,52,6,13,21])).
% 0.53/0.74 cnf(100,plain,
% 0.53/0.74 (P3(a3,f4(a3,a3),f6(x1001,a3))),
% 0.53/0.74 inference(scs_inference,[],[31,33,52,6,13,21,17])).
% 0.53/0.74 cnf(101,plain,
% 0.53/0.74 (P3(x1011,f4(a3,a3),x1011)),
% 0.53/0.74 inference(rename_variables,[],[52])).
% 0.53/0.74 cnf(104,plain,
% 0.53/0.74 (P3(x1041,f4(a3,a3),x1041)),
% 0.53/0.74 inference(rename_variables,[],[52])).
% 0.53/0.74 cnf(109,plain,
% 0.53/0.74 (P1(x1091,a3,a3)),
% 0.53/0.74 inference(rename_variables,[],[2])).
% 0.53/0.74 cnf(114,plain,
% 0.53/0.74 (P1(f6(x1141,a3),x1142,f6(x1141,a3))),
% 0.53/0.74 inference(scs_inference,[],[31,33,52,101,65,40,46,55,3,43,6,2,13,21,17,15,16,22,24,25])).
% 0.53/0.74 cnf(116,plain,
% 0.53/0.74 (P3(x1161,f5(f4(a3,a3)),x1161)),
% 0.53/0.74 inference(scs_inference,[],[31,33,52,101,104,65,40,46,55,3,43,6,2,5,4,13,21,17,15,16,22,24,25,23])).
% 0.53/0.74 cnf(120,plain,
% 0.53/0.74 (P1(a3,f6(a3,a3),x1201)),
% 0.53/0.74 inference(scs_inference,[],[31,33,60,52,101,104,89,65,40,46,55,3,43,6,2,5,4,13,21,17,15,16,22,24,25,23,26])).
% 0.53/0.74 cnf(122,plain,
% 0.53/0.74 (P1(f6(x1221,a3),f7(f6(x1221,a3),x1222),x1222)),
% 0.53/0.74 inference(rename_variables,[],[89])).
% 0.53/0.74 cnf(124,plain,
% 0.53/0.74 (P1(x1241,f6(x1242,a3),f6(x1242,a3))),
% 0.53/0.74 inference(scs_inference,[],[31,33,60,52,101,104,89,65,40,46,55,3,43,6,2,109,5,4,13,21,17,15,16,22,24,25,23,26,30])).
% 0.53/0.74 cnf(126,plain,
% 0.53/0.74 (P3(x1261,x1261,x1261)),
% 0.53/0.74 inference(scs_inference,[],[31,33,60,52,101,104,89,122,65,40,46,55,3,43,6,2,109,5,4,13,21,17,15,16,22,24,25,23,26,30,28])).
% 0.53/0.74 cnf(134,plain,
% 0.53/0.74 (P1(f6(x1341,a3),x1342,f4(f6(x1341,a3),f4(a3,a3)))),
% 0.53/0.74 inference(scs_inference,[],[97,114,18])).
% 0.53/0.74 cnf(135,plain,
% 0.53/0.74 (P2(x1351,f4(x1351,f4(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[97])).
% 0.53/0.74 cnf(137,plain,
% 0.53/0.74 (P1(f4(f6(x1371,a3),f4(a3,a3)),x1372,f6(x1371,a3))),
% 0.53/0.74 inference(scs_inference,[],[97,135,114,18,20])).
% 0.53/0.74 cnf(138,plain,
% 0.53/0.74 (P2(x1381,f4(x1381,f4(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[97])).
% 0.53/0.74 cnf(140,plain,
% 0.53/0.74 (P3(f4(x1401,f4(a3,a3)),x1401,x1401)),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,126,114,18,20,17])).
% 0.53/0.74 cnf(141,plain,
% 0.53/0.74 (P2(x1411,f4(x1411,f4(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[97])).
% 0.53/0.74 cnf(143,plain,
% 0.53/0.74 (P3(x1431,f4(x1431,f4(a3,a3)),x1431)),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,141,126,114,18,20,17,16])).
% 0.53/0.74 cnf(144,plain,
% 0.53/0.74 (P2(x1441,f4(x1441,f4(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[97])).
% 0.53/0.74 cnf(148,plain,
% 0.53/0.74 (P3(x1481,x1481,x1481)),
% 0.53/0.74 inference(rename_variables,[],[126])).
% 0.53/0.74 cnf(150,plain,
% 0.53/0.74 (P3(x1501,x1501,f4(x1501,f4(a3,a3)))),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,141,144,126,148,114,40,18,20,17,16,21,15])).
% 0.53/0.74 cnf(154,plain,
% 0.53/0.74 (P1(x1541,f6(x1542,a3),f6(x1542,a3))),
% 0.53/0.74 inference(rename_variables,[],[124])).
% 0.53/0.74 cnf(155,plain,
% 0.53/0.74 (P1(f6(x1551,a3),x1552,f6(x1551,a3))),
% 0.53/0.74 inference(rename_variables,[],[114])).
% 0.53/0.74 cnf(157,plain,
% 0.53/0.74 (P1(f6(a3,a3),x1571,x1572)),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,141,144,126,148,114,155,124,154,120,40,18,20,17,16,21,15,22,25])).
% 0.53/0.74 cnf(158,plain,
% 0.53/0.74 (P1(x1581,f6(x1582,a3),f6(x1582,a3))),
% 0.53/0.74 inference(rename_variables,[],[124])).
% 0.53/0.74 cnf(159,plain,
% 0.53/0.74 (P1(f6(x1591,a3),x1592,f6(x1591,a3))),
% 0.53/0.74 inference(rename_variables,[],[114])).
% 0.53/0.74 cnf(162,plain,
% 0.53/0.74 (P3(x1621,x1621,x1621)),
% 0.53/0.74 inference(rename_variables,[],[126])).
% 0.53/0.74 cnf(164,plain,
% 0.53/0.74 (P1(f6(x1641,a3),x1642,f6(a3,a3))),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,141,144,126,148,114,155,159,124,154,158,120,100,40,18,20,17,16,21,15,22,25,24,26])).
% 0.53/0.74 cnf(165,plain,
% 0.53/0.74 (P1(f6(x1651,a3),x1652,f6(x1651,a3))),
% 0.53/0.74 inference(rename_variables,[],[114])).
% 0.53/0.74 cnf(166,plain,
% 0.53/0.74 (P1(x1661,f6(x1662,a3),f6(x1662,a3))),
% 0.53/0.74 inference(rename_variables,[],[124])).
% 0.53/0.74 cnf(170,plain,
% 0.53/0.74 (P1(f6(x1701,a3),x1702,f6(x1701,a3))),
% 0.53/0.74 inference(rename_variables,[],[114])).
% 0.53/0.74 cnf(171,plain,
% 0.53/0.74 (P3(x1711,x1711,x1711)),
% 0.53/0.74 inference(rename_variables,[],[126])).
% 0.53/0.74 cnf(173,plain,
% 0.53/0.74 (P1(f6(x1731,a3),x1732,f4(f6(x1731,a3),f6(x1731,a3)))),
% 0.53/0.74 inference(scs_inference,[],[97,135,138,141,144,126,148,162,171,114,155,159,165,170,124,154,158,166,120,100,40,6,18,20,17,16,21,15,22,25,24,26,27,30])).
% 0.53/0.74 cnf(193,plain,
% 0.53/0.74 (P3(x1931,f4(x1931,f4(a3,a3)),x1931)),
% 0.53/0.74 inference(rename_variables,[],[143])).
% 0.53/0.74 cnf(195,plain,
% 0.53/0.74 (P1(a3,x1951,x1952)),
% 0.53/0.74 inference(scs_inference,[],[33,43,157,143,150,21,17,20])).
% 0.53/0.74 cnf(196,plain,
% 0.53/0.74 (P2(f6(x1961,a3),a3)),
% 0.53/0.74 inference(rename_variables,[],[33])).
% 0.53/0.74 cnf(207,plain,
% 0.53/0.74 (P1(x2071,f6(a3,a3),f4(f6(a3,a3),f6(a3,a3)))),
% 0.53/0.74 inference(scs_inference,[],[33,196,97,43,157,140,143,150,164,173,21,17,20,16,15,22,25])).
% 0.53/0.74 cnf(209,plain,
% 0.53/0.74 (P1(f6(a3,a3),x2091,x2092)),
% 0.53/0.74 inference(rename_variables,[],[157])).
% 0.53/0.74 cnf(210,plain,
% 0.53/0.74 (P1(f6(a3,a3),x2101,x2102)),
% 0.53/0.74 inference(rename_variables,[],[157])).
% 0.53/0.74 cnf(216,plain,
% 0.53/0.74 (P3(a3,a3,f6(x2161,a3))),
% 0.53/0.74 inference(rename_variables,[],[43])).
% 0.53/0.74 cnf(218,plain,
% 0.53/0.74 (P3(x2181,x2181,x2182)),
% 0.53/0.74 inference(scs_inference,[],[33,196,97,43,216,157,210,209,140,143,193,150,164,173,37,21,17,20,16,15,22,25,23,24,27])).
% 0.53/0.74 cnf(231,plain,
% 0.53/0.74 (P2(f6(x2311,a3),a3)),
% 0.53/0.74 inference(rename_variables,[],[33])).
% 0.53/0.74 cnf(234,plain,
% 0.53/0.74 (P2(f6(x2341,a3),a3)),
% 0.53/0.74 inference(rename_variables,[],[33])).
% 0.53/0.74 cnf(236,plain,
% 0.53/0.74 (P2(x2361,f5(f4(a3,a3)))),
% 0.53/0.74 inference(scs_inference,[],[33,231,218,207,116,137,19,18,21])).
% 0.53/0.74 cnf(237,plain,
% 0.53/0.74 (P3(x2371,f5(f4(a3,a3)),x2371)),
% 0.53/0.74 inference(rename_variables,[],[116])).
% 0.53/0.74 cnf(238,plain,
% 0.53/0.74 (P3(x2381,x2381,x2382)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(240,plain,
% 0.53/0.74 (P3(a3,f6(x2401,a3),x2402)),
% 0.53/0.74 inference(scs_inference,[],[33,231,234,218,238,207,116,137,19,18,21,17])).
% 0.53/0.74 cnf(241,plain,
% 0.53/0.74 (P3(x2411,x2411,x2412)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(243,plain,
% 0.53/0.74 (P3(f6(x2431,a3),a3,x2432)),
% 0.53/0.74 inference(scs_inference,[],[33,231,234,218,238,241,207,116,137,19,18,21,17,16])).
% 0.53/0.74 cnf(244,plain,
% 0.53/0.74 (P3(x2441,x2441,x2442)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(247,plain,
% 0.53/0.74 (P1(f4(f6(x2471,a3),f4(a3,a3)),x2472,f6(x2471,a3))),
% 0.53/0.74 inference(rename_variables,[],[137])).
% 0.53/0.74 cnf(248,plain,
% 0.53/0.74 (P1(x2481,f6(a3,a3),f4(f6(a3,a3),f6(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[207])).
% 0.53/0.74 cnf(250,plain,
% 0.53/0.74 (P3(f5(f4(a3,a3)),x2501,x2501)),
% 0.53/0.74 inference(scs_inference,[],[33,231,234,218,238,241,244,207,116,237,137,19,18,21,17,16,22,23])).
% 0.53/0.74 cnf(252,plain,
% 0.53/0.74 (P3(x2521,x2521,x2522)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(253,plain,
% 0.53/0.74 (P3(x2531,x2531,x2532)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(256,plain,
% 0.53/0.74 (P1(f4(f6(x2561,a3),f4(a3,a3)),x2562,f6(x2561,a3))),
% 0.53/0.74 inference(rename_variables,[],[137])).
% 0.53/0.74 cnf(257,plain,
% 0.53/0.74 (P1(x2571,f6(a3,a3),f4(f6(a3,a3),f6(a3,a3)))),
% 0.53/0.74 inference(rename_variables,[],[207])).
% 0.53/0.74 cnf(260,plain,
% 0.53/0.74 (P3(x2601,x2602,x2601)),
% 0.53/0.74 inference(scs_inference,[],[33,231,234,218,238,241,244,253,252,207,248,116,237,137,247,134,19,18,21,17,16,22,23,25,24])).
% 0.53/0.74 cnf(263,plain,
% 0.53/0.74 (P3(x2631,x2631,x2632)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(267,plain,
% 0.53/0.74 (P3(x2671,x2671,x2672)),
% 0.53/0.74 inference(rename_variables,[],[218])).
% 0.53/0.74 cnf(270,plain,
% 0.53/0.74 (P1(x2701,f6(a3,a3),x2701)),
% 0.53/0.74 inference(scs_inference,[],[33,231,234,218,238,241,244,253,263,267,252,207,248,257,116,237,137,247,256,134,19,18,21,17,16,22,23,25,24,30,29])).
% 0.53/0.74 cnf(278,plain,
% 0.53/0.74 (P2(f6(x2781,a3),a3)),
% 0.53/0.74 inference(rename_variables,[],[33])).
% 0.53/0.74 cnf(281,plain,
% 0.53/0.74 (P1(x2811,f6(a3,a3),x2811)),
% 0.53/0.74 inference(rename_variables,[],[270])).
% 0.53/0.74 cnf(284,plain,
% 0.53/0.74 (P3(f5(f4(a3,a3)),x2841,x2841)),
% 0.53/0.74 inference(rename_variables,[],[250])).
% 0.53/0.74 cnf(285,plain,
% 0.53/0.74 (P3(x2851,x2852,x2851)),
% 0.53/0.74 inference(rename_variables,[],[260])).
% 0.53/0.74 cnf(290,plain,
% 0.53/0.74 (P3(f6(x2901,a3),x2902,a3)),
% 0.53/0.74 inference(scs_inference,[],[33,278,236,260,285,270,281,250,19,18,21,20,15])).
% 0.53/0.74 cnf(291,plain,
% 0.53/0.74 (P3(x2911,x2912,x2911)),
% 0.53/0.74 inference(rename_variables,[],[260])).
% 0.53/0.74 cnf(294,plain,
% 0.53/0.74 (P3(x2941,x2942,x2941)),
% 0.53/0.74 inference(rename_variables,[],[260])).
% 0.53/0.74 cnf(298,plain,
% 0.53/0.74 (P1(x2981,f6(a3,a3),x2981)),
% 0.53/0.74 inference(rename_variables,[],[270])).
% 0.53/0.74 cnf(301,plain,
% 0.53/0.74 (P1(x3011,f6(a3,a3),x3011)),
% 0.53/0.74 inference(rename_variables,[],[270])).
% 0.53/0.74 cnf(304,plain,
% 0.53/0.74 (P3(f5(f4(a3,a3)),x3041,f6(x3042,a3))),
% 0.53/0.74 inference(scs_inference,[],[33,278,236,260,285,291,294,270,281,298,250,284,195,240,89,157,19,18,21,20,15,17,22,25,24])).
% 0.53/0.74 cnf(305,plain,
% 0.53/0.74 (P3(x3051,x3052,x3051)),
% 0.53/0.74 inference(rename_variables,[],[260])).
% 0.53/0.74 cnf(311,plain,
% 0.53/0.74 (P1(x3111,f6(a3,a3),x3112)),
% 0.53/0.74 inference(scs_inference,[],[33,278,236,260,285,291,294,305,270,281,298,301,250,284,195,240,218,89,173,157,19,18,21,20,15,17,22,25,24,26,30])).
% 0.53/0.74 cnf(316,plain,
% 0.53/0.74 (P2(f6(x3161,a3),a3)),
% 0.53/0.74 inference(rename_variables,[],[33])).
% 0.53/0.74 cnf(321,plain,
% 0.53/0.74 ($false),
% 0.53/0.74 inference(scs_inference,[],[8,33,316,311,304,243,290,19,15,21]),
% 0.53/0.74 ['proof']).
% 0.53/0.74 % SZS output end Proof
% 0.53/0.74 % Total time :0.110000s
%------------------------------------------------------------------------------