%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG001-2 : 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 : n021.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 6.04s 6.15s
% Output : CNFRefutation 6.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : RNG001-2 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 13:48:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 6.04/6.14 %-------------------------------------------
% 6.04/6.14 % File :CSE---1.7
% 6.04/6.14 % Problem :theBenchmark
% 6.04/6.14 % Transform :cnf
% 6.04/6.14 % Format :tptp:raw
% 6.04/6.14 % Command :java -jar mcs_scs.jar %d %s
% 6.04/6.14
% 6.04/6.14 % Result :Theorem 5.540000s
% 6.04/6.14 % Output :CNFRefutation 5.540000s
% 6.04/6.14 %-------------------------------------------
% 6.04/6.15 %--------------------------------------------------------------------------
% 6.04/6.15 % File : RNG001-2 : TPTP v8.2.0. Released v1.0.0.
% 6.04/6.15 % Domain : Ring Theory
% 6.04/6.15 % Problem : X.additive_identity = additive_identity for any X
% 6.04/6.15 % Version : [LS74] axioms : Incomplete.
% 6.04/6.15 % English :
% 6.04/6.15
% 6.04/6.15 % Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% 6.04/6.15 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 6.04/6.15 % Source : [SPRFN]
% 6.04/6.15 % Names : ls37 [LS74]
% 6.04/6.15 % : ls37 [WM76]
% 6.04/6.15
% 6.04/6.15 % Status : Unsatisfiable
% 6.04/6.15 % Rating : 0.09 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.2.0, 0.17 v6.1.0, 0.50 v6.0.0, 0.44 v5.5.0, 0.62 v5.4.0, 0.72 v5.3.0, 0.75 v5.2.0, 0.54 v5.1.0, 0.62 v5.0.0, 0.53 v4.1.0, 0.60 v4.0.1, 0.57 v3.4.0, 0.40 v3.3.0, 0.00 v3.2.0, 0.33 v2.7.0, 0.38 v2.6.0, 0.43 v2.4.0, 0.57 v2.3.0, 0.86 v2.2.1, 1.00 v2.1.0, 0.86 v2.0.0
% 6.04/6.15 % Syntax : Number of clauses : 18 ( 7 unt; 0 nHn; 12 RR)
% 6.04/6.15 % Number of literals : 51 ( 0 equ; 34 neg)
% 6.04/6.15 % Maximal clause size : 5 ( 2 avg)
% 6.04/6.15 % Maximal term depth : 2 ( 1 avg)
% 6.04/6.15 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 6.04/6.15 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 6.04/6.15 % Number of variables : 71 ( 0 sgn)
% 6.04/6.15 % SPC : CNF_UNS_RFO_NEQ_HRN
% 6.04/6.15
% 6.04/6.15 % Comments :
% 6.04/6.15 %--------------------------------------------------------------------------
% 6.04/6.15 %----Don't Include ring theory axioms
% 6.04/6.15 %include('Axioms/RNG001-0.ax').
% 6.04/6.15 %--------------------------------------------------------------------------
% 6.04/6.15 cnf(sum_substitution3,axiom,
% 6.04/6.15 ( ~ equalish(A,B)
% 6.04/6.15 | ~ sum(C,D,A)
% 6.04/6.15 | sum(C,D,B) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(additive_identity1,axiom,
% 6.04/6.15 sum(additive_identity,X,X) ).
% 6.04/6.15
% 6.04/6.15 cnf(additive_identity2,axiom,
% 6.04/6.15 sum(X,additive_identity,X) ).
% 6.04/6.15
% 6.04/6.15 cnf(closure_of_multiplication,axiom,
% 6.04/6.15 product(X,Y,multiply(X,Y)) ).
% 6.04/6.15
% 6.04/6.15 cnf(closure_of_addition,axiom,
% 6.04/6.15 sum(X,Y,add(X,Y)) ).
% 6.04/6.15
% 6.04/6.15 cnf(additive_inverse1,axiom,
% 6.04/6.15 sum(additive_inverse(X),X,additive_identity) ).
% 6.04/6.15
% 6.04/6.15 cnf(additive_inverse2,axiom,
% 6.04/6.15 sum(X,additive_inverse(X),additive_identity) ).
% 6.04/6.15
% 6.04/6.15 cnf(associativity_of_addition1,axiom,
% 6.04/6.15 ( ~ sum(X,Y,U)
% 6.04/6.15 | ~ sum(Y,Z,V)
% 6.04/6.15 | ~ sum(U,Z,W)
% 6.04/6.15 | sum(X,V,W) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(associativity_of_addition2,axiom,
% 6.04/6.15 ( ~ sum(X,Y,U)
% 6.04/6.15 | ~ sum(Y,Z,V)
% 6.04/6.15 | ~ sum(X,V,W)
% 6.04/6.15 | sum(U,Z,W) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(commutativity_of_addition,axiom,
% 6.04/6.15 ( ~ sum(X,Y,Z)
% 6.04/6.15 | sum(Y,X,Z) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(associativity_of_multiplication1,axiom,
% 6.04/6.15 ( ~ product(X,Y,U)
% 6.04/6.15 | ~ product(Y,Z,V)
% 6.04/6.15 | ~ product(U,Z,W)
% 6.04/6.15 | product(X,V,W) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(associativity_of_multiplication2,axiom,
% 6.04/6.15 ( ~ product(X,Y,U)
% 6.04/6.15 | ~ product(Y,Z,V)
% 6.04/6.15 | ~ product(X,V,W)
% 6.04/6.15 | product(U,Z,W) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(distributivity1,axiom,
% 6.04/6.15 ( ~ product(X,Y,V1)
% 6.04/6.15 | ~ product(X,Z,V2)
% 6.04/6.15 | ~ sum(Y,Z,V3)
% 6.04/6.15 | ~ product(X,V3,V4)
% 6.04/6.15 | sum(V1,V2,V4) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(distributivity2,axiom,
% 6.04/6.15 ( ~ product(X,Y,V1)
% 6.04/6.15 | ~ product(X,Z,V2)
% 6.04/6.15 | ~ sum(Y,Z,V3)
% 6.04/6.15 | ~ sum(V1,V2,V4)
% 6.04/6.15 | product(X,V3,V4) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(distributivity3,axiom,
% 6.04/6.15 ( ~ product(Y,X,V1)
% 6.04/6.15 | ~ product(Z,X,V2)
% 6.04/6.15 | ~ sum(Y,Z,V3)
% 6.04/6.15 | ~ product(V3,X,V4)
% 6.04/6.15 | sum(V1,V2,V4) ) ).
% 6.04/6.15
% 6.04/6.15 cnf(distributivity4,axiom,
% 6.04/6.15 ( ~ product(Y,X,V1)
% 6.04/6.15 | ~ product(Z,X,V2)
% 6.04/6.15 | ~ sum(Y,Z,V3)
% 6.04/6.15 | ~ sum(V1,V2,V4)
% 6.04/6.15 | product(V3,X,V4) ) ).
% 6.04/6.15
% 6.04/6.15 %----Equality axioms for operators
% 6.04/6.15 cnf(addition_is_well_defined,axiom,
% 6.04/6.15 ( ~ sum(X,Y,U)
% 6.04/6.15 | ~ sum(X,Y,V)
% 6.04/6.15 | equalish(U,V) ) ).
% 6.04/6.15
% 6.04/6.15 %input_clause(multiplication_is_well_defined,axiom,
% 6.04/6.15 % [--product(X,Y,U),
% 6.04/6.15 % --product(X,Y,V),
% 6.04/6.15 % ++equalish(U,V)]).
% 6.04/6.15
% 6.04/6.15 cnf(theorem,negated_conjecture,
% 6.04/6.15 ~ product(a,additive_identity,additive_identity) ).
% 6.04/6.15
% 6.04/6.15 %--------------------------------------------------------------------------
% 6.04/6.15 %-------------------------------------------
% 6.04/6.15 % Proof found
% 6.04/6.15 % SZS status Theorem for theBenchmark
% 6.04/6.15 % SZS output start Proof
% 6.04/6.15 %ClaNum:18(EqnAxiom:0)
% 6.04/6.15 %VarNum:146(SingletonVarNum:71)
% 6.04/6.15 %MaxLitNum:5
% 6.04/6.15 %MaxfuncDepth:1
% 6.04/6.15 %SharedTerms:3
% 6.04/6.15 %goalClause: 7
% 6.04/6.15 %singleGoalClaCount:1
% 6.04/6.15 [7]~P2(a3,a1,a1)
% 6.04/6.15 [1]P1(x11,a1,x11)
% 6.04/6.15 [2]P1(a1,x21,x21)
% 6.04/6.15 [3]P1(x31,f4(x31),a1)
% 6.04/6.15 [4]P1(f4(x41),x41,a1)
% 6.04/6.15 [5]P1(x51,x52,f2(x51,x52))
% 6.04/6.15 [6]P2(x61,x62,f5(x61,x62))
% 6.04/6.15 [8]~P1(x82,x81,x83)+P1(x81,x82,x83)
% 6.04/6.15 [9]~P1(x91,x92,x94)+P1(x91,x92,x93)+~P3(x94,x93)
% 6.04/6.15 [10]~P1(x103,x104,x101)+P3(x101,x102)+~P1(x103,x104,x102)
% 6.04/6.15 [11]~P1(x116,x114,x111)+P1(x111,x112,x113)+~P1(x114,x112,x115)+~P1(x116,x115,x113)
% 6.04/6.15 [12]~P1(x121,x126,x124)+P1(x121,x122,x123)+~P1(x124,x125,x123)+~P1(x126,x125,x122)
% 6.04/6.15 [13]~P2(x136,x134,x131)+P2(x131,x132,x133)+~P2(x134,x132,x135)+~P2(x136,x135,x133)
% 6.04/6.16 [14]~P2(x141,x146,x144)+P2(x141,x142,x143)+~P2(x144,x145,x143)+~P2(x146,x145,x142)
% 6.04/6.16 [15]~P2(x157,x155,x152)+~P2(x157,x154,x151)+P1(x151,x152,x153)+~P1(x154,x155,x156)+~P2(x157,x156,x153)
% 6.04/6.16 [16]~P2(x165,x167,x162)+~P2(x164,x167,x161)+P1(x161,x162,x163)+~P1(x164,x165,x166)+~P2(x166,x167,x163)
% 6.04/6.16 [17]~P2(x177,x172,x175)+~P2(x176,x172,x174)+P2(x171,x172,x173)+~P1(x174,x175,x173)+~P1(x176,x177,x171)
% 6.04/6.16 [18]~P2(x181,x187,x185)+~P2(x181,x186,x184)+P2(x181,x182,x183)+~P1(x184,x185,x183)+~P1(x186,x187,x182)
% 6.04/6.16 %EqnAxiom
% 6.04/6.16
% 6.04/6.16 %-------------------------------------------
% 6.04/6.16 cnf(21,plain,
% 6.04/6.16 (P1(x211,f2(a1,a1),x211)),
% 6.04/6.16 inference(scs_inference,[],[1,5,10,12])).
% 6.04/6.16 cnf(22,plain,
% 6.04/6.16 (P1(x221,x222,f2(x221,x222))),
% 6.04/6.16 inference(rename_variables,[],[5])).
% 6.04/6.16 cnf(25,plain,
% 6.04/6.16 (P1(x251,x252,f2(x251,x252))),
% 6.04/6.16 inference(rename_variables,[],[5])).
% 6.04/6.16 cnf(26,plain,
% 6.04/6.16 (P1(x261,a1,x261)),
% 6.04/6.16 inference(rename_variables,[],[1])).
% 6.04/6.16 cnf(28,plain,
% 6.04/6.16 (P2(x281,x282,f5(x281,x282))),
% 6.04/6.16 inference(rename_variables,[],[6])).
% 6.04/6.16 cnf(32,plain,
% 6.04/6.16 (P1(x321,a1,x321)),
% 6.04/6.16 inference(rename_variables,[],[1])).
% 6.04/6.16 cnf(34,plain,
% 6.04/6.16 (P2(x341,x342,f5(x341,x342))),
% 6.04/6.16 inference(rename_variables,[],[6])).
% 6.04/6.16 cnf(36,plain,
% 6.04/6.16 (P1(f5(x361,a1),f5(x361,a1),f5(x361,a1))),
% 6.04/6.16 inference(scs_inference,[],[6,28,34,1,26,32,5,22,25,10,12,17,18,15])).
% 6.04/6.16 cnf(39,plain,
% 6.04/6.16 (P2(x391,x392,f5(x391,x392))),
% 6.04/6.16 inference(rename_variables,[],[6])).
% 6.04/6.16 cnf(40,plain,
% 6.04/6.16 (P1(x401,a1,x401)),
% 6.04/6.16 inference(rename_variables,[],[1])).
% 6.04/6.16 cnf(42,plain,
% 6.04/6.16 (P1(f5(a1,x421),f5(a1,x421),f5(a1,x421))),
% 6.04/6.16 inference(scs_inference,[],[6,28,34,39,1,26,32,40,5,22,25,10,12,17,18,15,16])).
% 6.04/6.16 cnf(44,plain,
% 6.04/6.16 (P2(x441,x442,f5(x441,x442))),
% 6.04/6.16 inference(rename_variables,[],[6])).
% 6.04/6.16 cnf(45,plain,
% 6.04/6.16 (P2(x451,x452,f5(x451,x452))),
% 6.04/6.16 inference(rename_variables,[],[6])).
% 6.04/6.16 cnf(48,plain,
% 6.04/6.16 (P2(f5(x481,x482),x483,f5(x481,x482))+~P2(x482,x483,x482)),
% 6.04/6.16 inference(scs_inference,[],[6,28,34,39,45,1,26,32,40,5,22,25,10,12,17,18,15,16,13])).
% 6.04/6.16 cnf(50,plain,
% 6.04/6.16 (P2(x501,f5(x501,x501),f5(f5(x501,x501),x501))),
% 6.04/6.16 inference(scs_inference,[],[6,28,34,39,45,44,1,26,32,40,5,22,25,10,12,17,18,15,16,13,14])).
% 6.04/6.16 cnf(55,plain,
% 6.04/6.16 (P3(f4(a1),a1)),
% 6.04/6.16 inference(scs_inference,[],[2,3,10])).
% 6.04/6.16 cnf(56,plain,
% 6.04/6.16 (P1(x561,f4(x561),a1)),
% 6.04/6.16 inference(rename_variables,[],[3])).
% 6.04/6.16 cnf(61,plain,
% 6.04/6.16 (P1(x611,f4(x611),a1)),
% 6.04/6.16 inference(rename_variables,[],[3])).
% 6.04/6.16 cnf(63,plain,
% 6.04/6.16 (P1(f5(x631,a1),a1,a1)),
% 6.04/6.16 inference(scs_inference,[],[36,2,3,56,61,1,10,11,12])).
% 6.04/6.16 cnf(73,plain,
% 6.04/6.16 (P3(a1,f4(f2(a1,a1)))),
% 6.04/6.16 inference(scs_inference,[],[4,21,10])).
% 6.04/6.16 cnf(75,plain,
% 6.04/6.16 (P1(f4(x751),x751,a1)),
% 6.04/6.16 inference(rename_variables,[],[4])).
% 6.04/6.16 cnf(77,plain,
% 6.04/6.16 (P1(a1,f5(x771,a1),a1)),
% 6.04/6.16 inference(scs_inference,[],[36,4,75,21,10,11])).
% 6.04/6.16 cnf(78,plain,
% 6.04/6.16 (P1(f4(x781),x781,a1)),
% 6.04/6.16 inference(rename_variables,[],[4])).
% 6.04/6.16 cnf(79,plain,
% 6.04/6.16 (P1(f4(x791),x791,a1)),
% 6.04/6.16 inference(rename_variables,[],[4])).
% 6.04/6.16 cnf(81,plain,
% 6.04/6.16 (P1(f4(f4(x811)),a1,x811)),
% 6.04/6.16 inference(scs_inference,[],[36,4,75,79,78,2,21,10,11,12])).
% 6.04/6.16 cnf(94,plain,
% 6.04/6.16 (P1(x941,f4(x941),f4(f2(a1,a1)))),
% 6.04/6.16 inference(scs_inference,[],[3,73,9])).
% 6.04/6.16 cnf(96,plain,
% 6.04/6.16 (P3(a1,f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[3,2,73,9,10])).
% 6.04/6.16 cnf(97,plain,
% 6.04/6.16 (P1(a1,x971,x971)),
% 6.04/6.16 inference(rename_variables,[],[2])).
% 6.04/6.16 cnf(98,plain,
% 6.04/6.16 (P1(x981,f4(x981),a1)),
% 6.04/6.16 inference(rename_variables,[],[3])).
% 6.04/6.16 cnf(100,plain,
% 6.04/6.16 (P1(a1,f4(f4(x1001)),x1001)),
% 6.04/6.16 inference(scs_inference,[],[3,98,4,2,81,73,9,10,11])).
% 6.04/6.16 cnf(101,plain,
% 6.04/6.16 (P1(x1011,f4(x1011),a1)),
% 6.04/6.16 inference(rename_variables,[],[3])).
% 6.04/6.16 cnf(102,plain,
% 6.04/6.16 (P1(f4(x1021),x1021,a1)),
% 6.04/6.16 inference(rename_variables,[],[4])).
% 6.04/6.16 cnf(104,plain,
% 6.04/6.16 (P1(f4(a1),f4(a1),a1)),
% 6.04/6.16 inference(scs_inference,[],[3,98,101,4,102,2,97,81,73,9,10,11,12])).
% 6.04/6.16 cnf(109,plain,
% 6.04/6.16 (~P2(a3,f4(a1),f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[7,3,98,101,4,102,2,97,81,73,9,10,11,12,18])).
% 6.04/6.16 cnf(114,plain,
% 6.04/6.16 (P1(f4(x1141),x1141,f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[4,96,9])).
% 6.04/6.16 cnf(116,plain,
% 6.04/6.16 (P3(f4(a1),f4(f2(a1,a1)))),
% 6.04/6.16 inference(scs_inference,[],[4,2,94,96,9,10])).
% 6.04/6.16 cnf(118,plain,
% 6.04/6.16 (P1(a1,x1181,x1181)),
% 6.04/6.16 inference(rename_variables,[],[2])).
% 6.04/6.16 cnf(120,plain,
% 6.04/6.16 (P1(f4(a1),x1201,x1201)),
% 6.04/6.16 inference(scs_inference,[],[4,2,118,94,96,9,10,12])).
% 6.04/6.16 cnf(133,plain,
% 6.04/6.16 (P1(x1331,f4(x1331),f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[3,96,9])).
% 6.04/6.16 cnf(137,plain,
% 6.04/6.16 (P1(a1,x1371,x1371)),
% 6.04/6.16 inference(rename_variables,[],[2])).
% 6.04/6.16 cnf(139,plain,
% 6.04/6.16 (P1(x1391,f4(a1),x1391)),
% 6.04/6.16 inference(scs_inference,[],[3,2,137,21,114,96,9,10,12])).
% 6.04/6.16 cnf(147,plain,
% 6.04/6.16 (P1(a1,f5(x1471,a1),f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[77,96,9])).
% 6.04/6.16 cnf(149,plain,
% 6.04/6.16 (P3(a1,f5(x1491,a1))),
% 6.04/6.16 inference(scs_inference,[],[77,2,96,9,10])).
% 6.04/6.16 cnf(150,plain,
% 6.04/6.16 (P1(a1,x1501,x1501)),
% 6.04/6.16 inference(rename_variables,[],[2])).
% 6.04/6.16 cnf(152,plain,
% 6.04/6.16 (P1(f4(a1),f5(x1521,a1),f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[36,77,2,96,9,10,11])).
% 6.04/6.16 cnf(154,plain,
% 6.04/6.16 (P1(f5(x1541,a1),f5(x1542,a1),a1)),
% 6.04/6.16 inference(scs_inference,[],[36,77,63,2,150,96,9,10,11,12])).
% 6.04/6.16 cnf(163,plain,
% 6.04/6.16 (P3(a1,f4(f4(a1)))),
% 6.04/6.16 inference(scs_inference,[],[63,4,139,149,9,10])).
% 6.04/6.16 cnf(179,plain,
% 6.04/6.16 (P3(f5(a1,x1791),f2(f5(a1,x1791),f5(a1,x1791)))),
% 6.04/6.16 inference(scs_inference,[],[42,63,163,5,9,10])).
% 6.04/6.16 cnf(197,plain,
% 6.04/6.16 (P1(f5(x1971,a1),f4(a1),f4(a1))),
% 6.04/6.16 inference(scs_inference,[],[63,147,21,4,73,9,10,12])).
% 6.04/6.16 cnf(203,plain,
% 6.04/6.16 (P1(f4(a1),f5(x2031,a1),a1)),
% 6.04/6.16 inference(scs_inference,[],[152,55,9])).
% 6.04/6.16 cnf(219,plain,
% 6.04/6.16 (P3(f4(f4(x2191)),x2191)),
% 6.04/6.16 inference(scs_inference,[],[152,1,116,81,9,10])).
% 6.04/6.16 cnf(242,plain,
% 6.04/6.16 (P1(f4(f4(x2421)),f2(a1,a1),x2421)),
% 6.04/6.16 inference(scs_inference,[],[21,219,9])).
% 6.04/6.16 cnf(245,plain,
% 6.04/6.16 (P1(f5(x2451,a1),x2452,f4(f4(x2452)))),
% 6.04/6.16 inference(scs_inference,[],[63,21,2,100,219,9,12])).
% 6.04/6.16 cnf(275,plain,
% 6.04/6.16 (P1(f4(a1),f4(a1),f5(x2751,a1))),
% 6.04/6.16 inference(scs_inference,[],[104,149,9])).
% 6.04/6.16 cnf(283,plain,
% 6.04/6.16 (P1(f4(a1),f4(a1),f4(f4(a1)))),
% 6.04/6.16 inference(scs_inference,[],[104,163,9])).
% 6.04/6.16 cnf(285,plain,
% 6.04/6.16 (P1(f4(x2851),x2851,f2(a1,a1))),
% 6.04/6.16 inference(scs_inference,[],[104,3,2,242,163,9,12])).
% 6.04/6.16 cnf(307,plain,
% 6.04/6.16 (P1(f4(a1),f4(f4(x3071)),x3071)),
% 6.04/6.16 inference(scs_inference,[],[120,219,9])).
% 6.04/6.16 cnf(316,plain,
% 6.04/6.17 (P3(f4(f2(a1,a1)),f2(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[21,285,10])).
% 6.04/6.17 cnf(325,plain,
% 6.04/6.17 (P1(x3251,f4(x3251),f2(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[94,316,9])).
% 6.04/6.17 cnf(337,plain,
% 6.04/6.17 (P1(x3371,f4(x3371),f2(a1,a1))),
% 6.04/6.17 inference(rename_variables,[],[325])).
% 6.04/6.17 cnf(341,plain,
% 6.04/6.17 (P1(f5(a1,x3411),f2(a1,a1),f2(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[42,147,133,325,337,10,9,12])).
% 6.04/6.17 cnf(345,plain,
% 6.04/6.17 (P1(f4(a1),x3451,f4(f4(x3451)))),
% 6.04/6.17 inference(scs_inference,[],[104,2,307,12])).
% 6.04/6.17 cnf(369,plain,
% 6.04/6.17 (P3(f4(a1),f5(x3691,a1))),
% 6.04/6.17 inference(scs_inference,[],[152,120,10])).
% 6.04/6.17 cnf(384,plain,
% 6.04/6.17 (P1(f5(a1,x3841),f5(a1,x3841),f5(a1,x3841))),
% 6.04/6.17 inference(rename_variables,[],[42])).
% 6.04/6.17 cnf(386,plain,
% 6.04/6.17 (P1(f4(a1),a1,f5(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[42,384,275,203,139,10,9,12])).
% 6.04/6.17 cnf(391,plain,
% 6.04/6.17 (~P2(a3,f5(a1,a1),f5(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[109,42,384,275,203,139,10,9,12,18])).
% 6.04/6.17 cnf(409,plain,
% 6.04/6.17 (P1(f5(x4091,a1),f5(x4092,a1),f4(a1))),
% 6.04/6.17 inference(scs_inference,[],[152,197,120,12])).
% 6.04/6.17 cnf(430,plain,
% 6.04/6.17 (P1(f5(a1,a1),f5(a1,a1),f2(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[42,386,285,10,9])).
% 6.04/6.17 cnf(445,plain,
% 6.04/6.17 (P1(f4(x4451),x4451,f5(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[133,386,81,12])).
% 6.04/6.17 cnf(449,plain,
% 6.04/6.17 (P3(f4(f2(a1,a1)),f5(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[21,445,10])).
% 6.04/6.17 cnf(538,plain,
% 6.04/6.17 (P3(x5381,f2(x5381,a1))),
% 6.04/6.17 inference(scs_inference,[],[1,5,10])).
% 6.04/6.17 cnf(542,plain,
% 6.04/6.17 (P1(x5421,a1,x5421)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(547,plain,
% 6.04/6.17 (P1(x5471,a1,x5471)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(549,plain,
% 6.04/6.17 (P1(x5491,f5(x5492,a1),x5491)),
% 6.04/6.17 inference(scs_inference,[],[1,542,547,42,147,139,5,449,245,10,9,12,11])).
% 6.04/6.17 cnf(583,plain,
% 6.04/6.17 (P1(x5831,a1,x5831)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(586,plain,
% 6.04/6.17 (P1(x5861,a1,x5861)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(591,plain,
% 6.04/6.17 (P1(f4(f4(x5911)),f4(a1),x5911)),
% 6.04/6.17 inference(scs_inference,[],[1,583,586,3,430,81,5,369,345,10,9,12,11])).
% 6.04/6.17 cnf(636,plain,
% 6.04/6.17 (P1(x6361,a1,x6361)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(640,plain,
% 6.04/6.17 (P1(x6401,a1,x6401)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(642,plain,
% 6.04/6.17 (P1(f4(f4(x6421)),f5(x6422,a1),x6421)),
% 6.04/6.17 inference(scs_inference,[],[1,636,640,147,197,345,163,591,9,12,11])).
% 6.04/6.17 cnf(653,plain,
% 6.04/6.17 (P1(x6531,a1,x6531)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(659,plain,
% 6.04/6.17 (P1(x6591,a1,x6591)),
% 6.04/6.17 inference(rename_variables,[],[1])).
% 6.04/6.17 cnf(661,plain,
% 6.04/6.17 (~P2(a3,a1,f4(f4(a1)))),
% 6.04/6.17 inference(scs_inference,[],[1,653,659,7,6,147,133,275,591,73,642,9,12,11,18])).
% 6.04/6.17 cnf(673,plain,
% 6.04/6.17 (~P2(a1,x6731,a1)+P2(f4(a1),x6731,f4(a1))),
% 6.04/6.17 inference(scs_inference,[],[1,96,9,17])).
% 6.04/6.17 cnf(1143,plain,
% 6.04/6.17 (P1(a1,x11431,x11431)),
% 6.04/6.17 inference(rename_variables,[],[2])).
% 6.04/6.17 cnf(1146,plain,
% 6.04/6.17 (P1(a1,x11461,x11461)),
% 6.04/6.17 inference(rename_variables,[],[2])).
% 6.04/6.17 cnf(1147,plain,
% 6.04/6.17 (P1(x11471,f2(a1,a1),x11471)),
% 6.04/6.17 inference(rename_variables,[],[21])).
% 6.04/6.17 cnf(1151,plain,
% 6.04/6.17 (P1(a1,x11511,x11511)),
% 6.04/6.17 inference(rename_variables,[],[2])).
% 6.04/6.17 cnf(1153,plain,
% 6.04/6.17 (P2(a1,f5(a1,a1),f5(a1,a1))),
% 6.04/6.17 inference(scs_inference,[],[2,1143,1146,1151,50,6,341,139,21,1147,242,114,549,179,10,9,12,11,18])).
% 6.04/6.17 cnf(1159,plain,
% 6.04/6.17 (~P2(a1,a1,a3)),
% 6.04/6.17 inference(scs_inference,[],[2,1143,1146,1151,50,6,391,341,139,21,1147,242,114,549,179,10,9,12,11,18,13])).
% 6.04/6.17 cnf(1176,plain,
% 6.04/6.17 (P1(a1,x11761,x11761)),
% 6.04/6.17 inference(rename_variables,[],[2])).
% 6.04/6.17 cnf(1179,plain,
% 6.04/6.17 (P2(a1,a1,a1)),
% 6.04/6.17 inference(scs_inference,[],[2,1153,154,139,5,285,538,10,9,12,18])).
% 6.04/6.17 cnf(1188,plain,
% 6.04/6.17 (P2(f4(a1),a1,f4(a1))),
% 6.04/6.17 inference(scs_inference,[],[2,1176,1159,1153,154,139,100,5,285,538,10,9,12,18,17,48,673])).
% 6.04/6.17 cnf(1396,plain,
% 6.04/6.17 (~P2(a3,a1,f4(a1))),
% 6.04/6.17 inference(scs_inference,[],[2,661,283,18])).
% 6.04/6.17 cnf(1404,plain,
% 6.04/6.17 ($false),
% 6.04/6.17 inference(scs_inference,[],[2,6,1179,1188,1396,409,13,18]),
% 6.04/6.17 ['proof']).
% 6.04/6.17 % SZS output end Proof
% 6.04/6.17 % Total time :5.540000s
%------------------------------------------------------------------------------