%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP037-3 : 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 06:38:35 EDT 2024
% Result : Unsatisfiable 44.62s 44.67s
% Output : CNFRefutation 44.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP037-3 : 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.33 % Computer : n019.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 : Thu Jun 20 13:34:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.47/0.57 start to proof:theBenchmark
% 44.62/44.66 %-------------------------------------------
% 44.62/44.66 % File :CSE---1.7
% 44.62/44.66 % Problem :theBenchmark
% 44.62/44.66 % Transform :cnf
% 44.62/44.66 % Format :tptp:raw
% 44.62/44.66 % Command :java -jar mcs_scs.jar %d %s
% 44.62/44.66
% 44.62/44.66 % Result :Theorem 44.050000s
% 44.62/44.66 % Output :CNFRefutation 44.050000s
% 44.62/44.66 %-------------------------------------------
% 44.62/44.67 %--------------------------------------------------------------------------
% 44.62/44.67 % File : GRP037-3 : TPTP v8.2.0. Released v1.0.0.
% 44.62/44.67 % Domain : Group Theory (Subgroups)
% 44.62/44.67 % Problem : In subgroups, the inverse of an element is unique
% 44.62/44.67 % Version : [Wos65] axioms.
% 44.62/44.67 % English :
% 44.62/44.67
% 44.62/44.67 % Refs : [Wos65] Wos (1965), Unpublished Note
% 44.62/44.67 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 44.62/44.67 % Source : [SPRFN]
% 44.62/44.67 % Names : Problem 17 [Wos65]
% 44.62/44.67 % : wos17 [WM76]
% 44.62/44.67
% 44.62/44.67 % Status : Unsatisfiable
% 44.62/44.67 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.0.0
% 44.62/44.67 % Syntax : Number of clauses : 19 ( 8 unt; 0 nHn; 14 RR)
% 44.62/44.67 % Number of literals : 39 ( 4 equ; 21 neg)
% 44.62/44.67 % Maximal clause size : 4 ( 2 avg)
% 44.62/44.67 % Maximal term depth : 2 ( 1 avg)
% 44.62/44.67 % Number of predicates : 3 ( 2 usr; 0 prp; 1-3 aty)
% 44.62/44.67 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% 44.62/44.67 % Number of variables : 38 ( 0 sgn)
% 44.62/44.67 % SPC : CNF_UNS_RFO_SEQ_HRN
% 44.62/44.67
% 44.62/44.67 % Comments :
% 44.62/44.67 %--------------------------------------------------------------------------
% 44.62/44.67 %----Include group theory axioms
% 44.62/44.67 include('Axioms/GRP003-0.ax').
% 44.62/44.67 %----Include sub-group theory axioms
% 44.62/44.67 include('Axioms/GRP003-2.ax').
% 44.62/44.67 %--------------------------------------------------------------------------
% 44.62/44.67 cnf(another_left_identity,hypothesis,
% 44.62/44.67 ( ~ subgroup_member(A)
% 44.62/44.67 | product(another_identity,A,A) ) ).
% 44.62/44.67
% 44.62/44.67 cnf(another_right_identity,hypothesis,
% 44.62/44.67 ( ~ subgroup_member(A)
% 44.62/44.67 | product(A,another_identity,A) ) ).
% 44.62/44.67
% 44.62/44.67 cnf(another_right_inverse,hypothesis,
% 44.62/44.67 ( ~ subgroup_member(A)
% 44.62/44.67 | product(A,another_inverse(A),another_identity) ) ).
% 44.62/44.67
% 44.62/44.67 cnf(another_left_inverse,hypothesis,
% 44.62/44.67 ( ~ subgroup_member(A)
% 44.62/44.67 | product(another_inverse(A),A,another_identity) ) ).
% 44.62/44.67
% 44.62/44.67 cnf(another_inverse_in_subgroup,hypothesis,
% 44.62/44.67 ( ~ subgroup_member(A)
% 44.62/44.67 | subgroup_member(another_inverse(A)) ) ).
% 44.62/44.67
% 44.62/44.67 cnf(product_right_cancellation,hypothesis,
% 44.62/44.67 ( ~ product(A,B,C)
% 44.62/44.67 | ~ product(A,D,C)
% 44.62/44.67 | D = B ) ).
% 44.62/44.67
% 44.62/44.67 cnf(product_left_cancellation,hypothesis,
% 44.62/44.67 ( ~ product(A,B,C)
% 44.62/44.67 | ~ product(D,B,C)
% 44.62/44.67 | D = A ) ).
% 44.62/44.67
% 44.62/44.67 cnf(a_is_in_subgroup,hypothesis,
% 44.62/44.67 subgroup_member(a) ).
% 44.62/44.67
% 44.62/44.67 cnf(another_identity_in_subgroup,hypothesis,
% 44.62/44.67 subgroup_member(another_identity) ).
% 44.62/44.67
% 44.62/44.67 cnf(prove_two_inverses_are_equal,negated_conjecture,
% 44.62/44.67 inverse(a) != another_inverse(a) ).
% 44.62/44.67
% 44.62/44.67 %--------------------------------------------------------------------------
% 44.62/44.67 %-------------------------------------------
% 44.62/44.67 % Proof found
% 44.62/44.67 % SZS status Theorem for theBenchmark
% 44.62/44.67 % SZS output start Proof
% 44.62/44.67 %ClaNum:30(EqnAxiom:11)
% 44.62/44.67 %VarNum:80(SingletonVarNum:38)
% 44.62/44.67 %MaxLitNum:4
% 44.62/44.67 %MaxfuncDepth:1
% 44.62/44.67 %SharedTerms:8
% 44.62/44.67 %goalClause: 19
% 44.62/44.67 %singleGoalClaCount:1
% 44.62/44.67 [12]P1(a1)
% 44.62/44.67 [13]P1(a2)
% 44.62/44.67 [19]~E(f5(a2),f4(a2))
% 44.62/44.67 [14]P2(x141,a3,x141)
% 44.62/44.67 [15]P2(a3,x151,x151)
% 44.62/44.67 [16]P2(x161,f5(x161),a3)
% 44.62/44.67 [17]P2(f5(x171),x171,a3)
% 44.62/44.67 [18]P2(x181,x182,f6(x181,x182))
% 44.62/44.67 [21]~P1(x211)+P2(x211,a1,x211)
% 44.62/44.67 [22]~P1(x221)+P2(a1,x221,x221)
% 44.62/44.67 [20]~P1(x201)+P1(f4(x201))
% 44.62/44.67 [23]~P1(x231)+P2(x231,f4(x231),a1)
% 44.62/44.67 [24]~P1(x241)+P2(f4(x241),x241,a1)
% 44.62/44.67 [26]~P2(x263,x264,x261)+E(x261,x262)+~P2(x263,x264,x262)
% 44.62/44.67 [27]~P2(x273,x271,x274)+E(x271,x272)+~P2(x273,x272,x274)
% 44.62/44.67 [28]~P2(x281,x283,x284)+E(x281,x282)+~P2(x282,x283,x284)
% 44.62/44.67 [25]P1(x251)+~P1(x252)+~P1(x253)+~P2(x253,f5(x252),x251)
% 44.62/44.67 [29]~P2(x296,x294,x291)+P2(x291,x292,x293)+~P2(x294,x292,x295)+~P2(x296,x295,x293)
% 44.62/44.67 [30]~P2(x301,x306,x304)+P2(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x305,x302)
% 44.62/44.67 %EqnAxiom
% 44.62/44.67 [1]E(x11,x11)
% 44.62/44.67 [2]E(x22,x21)+~E(x21,x22)
% 44.62/44.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 44.62/44.67 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 44.62/44.67 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 44.62/44.67 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 44.62/44.67 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 44.62/44.67 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 44.62/44.67 [9]P2(x92,x93,x94)+~E(x91,x92)+~P2(x91,x93,x94)
% 44.62/44.67 [10]P2(x103,x102,x104)+~E(x101,x102)+~P2(x103,x101,x104)
% 44.62/44.67 [11]P2(x113,x114,x112)+~E(x111,x112)+~P2(x113,x114,x111)
% 44.62/44.67
% 44.62/44.67 %-------------------------------------------
% 44.66/44.68 cnf(31,plain,
% 44.66/44.68 (E(x311,f6(x311,a3))),
% 44.66/44.68 inference(scs_inference,[],[14,18,26])).
% 44.66/44.68 cnf(32,plain,
% 44.66/44.68 (P2(x321,x322,f6(x321,x322))),
% 44.66/44.68 inference(rename_variables,[],[18])).
% 44.66/44.68 cnf(34,plain,
% 44.66/44.68 (E(f6(a3,x341),x341)),
% 44.66/44.68 inference(scs_inference,[],[14,15,18,32,26,27])).
% 44.66/44.68 cnf(35,plain,
% 44.66/44.68 (P2(x351,x352,f6(x351,x352))),
% 44.66/44.68 inference(rename_variables,[],[18])).
% 44.66/44.68 cnf(36,plain,
% 44.66/44.68 (P2(a3,x361,x361)),
% 44.66/44.68 inference(rename_variables,[],[15])).
% 44.66/44.68 cnf(38,plain,
% 44.66/44.68 (E(f6(x381,a3),x381)),
% 44.66/44.68 inference(scs_inference,[],[14,15,18,32,35,26,27,28])).
% 44.66/44.68 cnf(39,plain,
% 44.66/44.68 (P2(x391,x392,f6(x391,x392))),
% 44.66/44.68 inference(rename_variables,[],[18])).
% 44.66/44.68 cnf(40,plain,
% 44.66/44.68 (P2(x401,a3,x401)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(44,plain,
% 44.66/44.68 (P2(x441,a3,x441)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(46,plain,
% 44.66/44.68 (P2(a3,x461,x461)),
% 44.66/44.68 inference(rename_variables,[],[15])).
% 44.66/44.68 cnf(49,plain,
% 44.66/44.68 (P1(f6(a1,f5(a1)))),
% 44.66/44.68 inference(scs_inference,[],[19,14,40,15,36,46,18,32,35,39,12,26,27,28,3,9,10,11,25])).
% 44.66/44.68 cnf(50,plain,
% 44.66/44.68 (P2(x501,x502,f6(x501,x502))),
% 44.66/44.68 inference(rename_variables,[],[18])).
% 44.66/44.68 cnf(52,plain,
% 44.66/44.68 (P2(x521,f6(a3,a3),x521)),
% 44.66/44.68 inference(scs_inference,[],[19,14,40,44,15,36,46,18,32,35,39,50,12,26,27,28,3,9,10,11,25,30])).
% 44.66/44.68 cnf(57,plain,
% 44.66/44.68 (E(x571,f6(a3,x571))),
% 44.66/44.68 inference(scs_inference,[],[34,2])).
% 44.66/44.68 cnf(58,plain,
% 44.66/44.68 (E(f5(a3),a3)),
% 44.66/44.68 inference(scs_inference,[],[34,14,17,2,26])).
% 44.66/44.68 cnf(59,plain,
% 44.66/44.68 (P2(f5(x591),x591,a3)),
% 44.66/44.68 inference(rename_variables,[],[17])).
% 44.66/44.68 cnf(60,plain,
% 44.66/44.68 (P2(x601,a3,x601)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(62,plain,
% 44.66/44.68 (E(a3,f5(a3))),
% 44.66/44.68 inference(scs_inference,[],[34,14,60,17,59,2,26,28])).
% 44.66/44.68 cnf(63,plain,
% 44.66/44.68 (P2(f5(x631),x631,a3)),
% 44.66/44.68 inference(rename_variables,[],[17])).
% 44.66/44.68 cnf(64,plain,
% 44.66/44.68 (P2(x641,a3,x641)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(66,plain,
% 44.66/44.68 (E(f6(a3,x661),f6(x661,a3))),
% 44.66/44.68 inference(scs_inference,[],[31,34,14,60,17,59,2,26,28,3])).
% 44.66/44.68 cnf(67,plain,
% 44.66/44.68 (E(x671,f6(x671,a3))),
% 44.66/44.68 inference(rename_variables,[],[31])).
% 44.66/44.68 cnf(68,plain,
% 44.66/44.68 (P2(x681,f6(f5(x681),a3),a3)),
% 44.66/44.68 inference(scs_inference,[],[31,67,34,14,60,16,17,59,2,26,28,3,10])).
% 44.66/44.68 cnf(69,plain,
% 44.66/44.68 (E(x691,f6(x691,a3))),
% 44.66/44.68 inference(rename_variables,[],[31])).
% 44.66/44.68 cnf(70,plain,
% 44.66/44.68 (E(f5(f5(x701)),x701)),
% 44.66/44.68 inference(scs_inference,[],[31,67,34,14,60,16,17,59,63,2,26,28,3,10,27])).
% 44.66/44.68 cnf(71,plain,
% 44.66/44.68 (P2(x711,f5(x711),a3)),
% 44.66/44.68 inference(rename_variables,[],[16])).
% 44.66/44.68 cnf(73,plain,
% 44.66/44.68 (P2(x731,f5(x731),f6(a3,a3))),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,34,14,60,16,71,17,59,63,2,26,28,3,10,27,11])).
% 44.66/44.68 cnf(74,plain,
% 44.66/44.68 (E(x741,f6(x741,a3))),
% 44.66/44.68 inference(rename_variables,[],[31])).
% 44.66/44.68 cnf(75,plain,
% 44.66/44.68 (P2(f6(x751,a3),a3,x751)),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,74,34,14,60,64,16,71,17,59,63,2,26,28,3,10,27,11,9])).
% 44.66/44.68 cnf(76,plain,
% 44.66/44.68 (P2(x761,a3,x761)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(77,plain,
% 44.66/44.68 (P2(f5(a3),f5(a3),a3)),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,74,34,14,60,64,76,16,71,17,59,63,2,26,28,3,10,27,11,9,29])).
% 44.66/44.68 cnf(78,plain,
% 44.66/44.68 (P2(f5(x781),x781,a3)),
% 44.66/44.68 inference(rename_variables,[],[17])).
% 44.66/44.68 cnf(79,plain,
% 44.66/44.68 (P2(x791,a3,x791)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(80,plain,
% 44.66/44.68 (P2(x801,f5(x801),a3)),
% 44.66/44.68 inference(rename_variables,[],[16])).
% 44.66/44.68 cnf(82,plain,
% 44.66/44.68 (P2(f5(f6(x821,a3)),x821,a3)),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,74,34,14,60,64,76,79,16,71,17,59,63,78,2,26,28,3,10,27,11,9,29,30])).
% 44.66/44.68 cnf(86,plain,
% 44.66/44.68 (P1(a3)),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,74,34,14,60,64,76,79,16,71,80,17,59,63,78,49,2,26,28,3,10,27,11,9,29,30,25])).
% 44.66/44.68 cnf(89,plain,
% 44.66/44.68 (~P1(f6(a3,x891))+P1(x891)),
% 44.66/44.68 inference(scs_inference,[],[31,67,69,74,34,14,60,64,76,79,16,71,80,17,59,63,78,49,2,26,28,3,10,27,11,9,29,30,25,8])).
% 44.66/44.68 cnf(90,plain,
% 44.66/44.68 (E(x901,f5(f5(x901)))),
% 44.66/44.68 inference(scs_inference,[],[70,2])).
% 44.66/44.68 cnf(91,plain,
% 44.66/44.68 (E(f5(f6(a3,a3)),a3)),
% 44.66/44.68 inference(scs_inference,[],[70,17,52,2,28])).
% 44.66/44.68 cnf(95,plain,
% 44.66/44.68 (E(a3,f5(f6(a3,a3)))),
% 44.66/44.68 inference(scs_inference,[],[70,14,17,73,52,2,28,27])).
% 44.66/44.68 cnf(97,plain,
% 44.66/44.68 (P2(x971,a3,x971)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(101,plain,
% 44.66/44.68 (P2(a3,x1011,x1011)),
% 44.66/44.68 inference(rename_variables,[],[15])).
% 44.66/44.68 cnf(105,plain,
% 44.66/44.68 (P1(f6(a3,a2))),
% 44.66/44.68 inference(scs_inference,[],[19,70,38,57,14,17,15,73,52,68,13,2,28,27,26,3,8])).
% 44.66/44.68 cnf(107,plain,
% 44.66/44.68 (P2(f5(f5(x1071)),a3,x1071)),
% 44.66/44.68 inference(scs_inference,[],[19,70,38,57,14,97,17,15,73,52,68,13,2,28,27,26,3,8,11])).
% 44.66/44.68 cnf(108,plain,
% 44.66/44.68 (P2(x1081,a3,x1081)),
% 44.66/44.68 inference(rename_variables,[],[14])).
% 44.66/44.68 cnf(109,plain,
% 44.66/44.68 (P2(a3,x1091,f5(f5(x1091)))),
% 44.66/44.68 inference(scs_inference,[],[19,70,38,57,14,97,17,15,101,73,52,68,13,2,28,27,26,3,8,11,10])).
% 44.66/44.69 cnf(112,plain,
% 44.66/44.69 (P2(x1121,a3,x1121)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(113,plain,
% 44.66/44.69 (P2(f5(f6(a3,a3)),f5(a3),a3)),
% 44.66/44.69 inference(scs_inference,[],[19,70,38,57,14,97,108,112,17,16,15,101,73,52,82,68,13,2,28,27,26,3,8,11,10,9,29])).
% 44.66/44.69 cnf(121,plain,
% 44.66/44.69 (E(f6(x1211,a3),f6(a3,x1211))),
% 44.66/44.69 inference(scs_inference,[],[66,2])).
% 44.66/44.69 cnf(122,plain,
% 44.66/44.69 (E(a3,f6(f5(a3),a3))),
% 44.66/44.69 inference(scs_inference,[],[66,14,68,2,27])).
% 44.66/44.69 cnf(124,plain,
% 44.66/44.69 (P2(x1241,a3,x1241)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(126,plain,
% 44.66/44.69 (P1(f5(a3))),
% 44.66/44.69 inference(scs_inference,[],[62,66,14,68,86,2,27,8])).
% 44.66/44.69 cnf(128,plain,
% 44.66/44.69 (P2(f5(x1281),x1281,f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[90,62,66,91,14,17,68,86,2,27,8,3,11])).
% 44.66/44.69 cnf(129,plain,
% 44.66/44.69 (E(x1291,f5(f5(x1291)))),
% 44.66/44.69 inference(rename_variables,[],[90])).
% 44.66/44.69 cnf(131,plain,
% 44.66/44.69 (E(x1311,f5(f5(x1311)))),
% 44.66/44.69 inference(rename_variables,[],[90])).
% 44.66/44.69 cnf(132,plain,
% 44.66/44.69 (P2(f5(f5(x1321)),x1322,f6(x1321,x1322))),
% 44.66/44.69 inference(scs_inference,[],[90,129,131,62,66,91,14,124,17,18,68,86,2,27,8,3,11,10,9])).
% 44.66/44.69 cnf(133,plain,
% 44.66/44.69 (P2(x1331,x1332,f6(x1331,x1332))),
% 44.66/44.69 inference(rename_variables,[],[18])).
% 44.66/44.69 cnf(135,plain,
% 44.66/44.69 (P2(x1351,a3,x1351)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(138,plain,
% 44.66/44.69 (P1(f5(f6(a3,a2)))),
% 44.66/44.69 inference(scs_inference,[],[90,129,131,62,66,91,14,124,17,16,18,15,107,105,68,86,2,27,8,3,11,10,9,29,25])).
% 44.66/44.69 cnf(141,plain,
% 44.66/44.69 (E(f5(a3),f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[90,129,131,62,66,91,14,124,135,17,16,18,15,107,105,68,86,2,27,8,3,11,10,9,29,25,26])).
% 44.66/44.69 cnf(142,plain,
% 44.66/44.69 (P2(x1421,a3,x1421)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(144,plain,
% 44.66/44.69 (E(x1441,f6(x1441,f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[90,129,131,62,66,91,14,124,135,17,16,18,133,15,107,105,52,68,86,2,27,8,3,11,10,9,29,25,26,28])).
% 44.66/44.69 cnf(146,plain,
% 44.66/44.69 (P2(x1461,x1462,f6(x1461,x1462))),
% 44.66/44.69 inference(rename_variables,[],[18])).
% 44.66/44.69 cnf(148,plain,
% 44.66/44.69 (P2(x1481,x1482,f6(x1481,f6(x1482,a3)))),
% 44.66/44.69 inference(scs_inference,[],[90,129,131,62,66,91,14,124,135,142,17,16,18,133,146,15,107,75,105,52,68,86,2,27,8,3,11,10,9,29,25,26,28,30])).
% 44.66/44.69 cnf(152,plain,
% 44.66/44.69 (E(f6(x1521,f6(a3,a3)),x1521)),
% 44.66/44.69 inference(scs_inference,[],[144,2])).
% 44.66/44.69 cnf(153,plain,
% 44.66/44.69 (E(f5(f5(x1531)),f6(x1531,a3))),
% 44.66/44.69 inference(scs_inference,[],[144,14,132,2,26])).
% 44.66/44.69 cnf(154,plain,
% 44.66/44.69 (P2(f5(f5(x1541)),x1542,f6(x1541,x1542))),
% 44.66/44.69 inference(rename_variables,[],[132])).
% 44.66/44.69 cnf(155,plain,
% 44.66/44.69 (P2(x1551,a3,x1551)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(157,plain,
% 44.66/44.69 (E(f6(x1571,a3),f5(f5(x1571)))),
% 44.66/44.69 inference(scs_inference,[],[144,14,155,132,154,2,26,28])).
% 44.66/44.69 cnf(158,plain,
% 44.66/44.69 (P2(f5(f5(x1581)),x1582,f6(x1581,x1582))),
% 44.66/44.69 inference(rename_variables,[],[132])).
% 44.66/44.69 cnf(159,plain,
% 44.66/44.69 (P2(x1591,a3,x1591)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(164,plain,
% 44.66/44.69 (E(x1641,f6(x1641,f6(a3,a3)))),
% 44.66/44.69 inference(rename_variables,[],[144])).
% 44.66/44.69 cnf(165,plain,
% 44.66/44.69 (P2(f6(x1651,f6(a3,a3)),a3,x1651)),
% 44.66/44.69 inference(scs_inference,[],[144,164,95,58,14,155,159,132,154,86,2,26,28,3,8,10,9])).
% 44.66/44.69 cnf(166,plain,
% 44.66/44.69 (P2(x1661,a3,x1661)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(167,plain,
% 44.66/44.69 (P2(f5(x1671),x1671,f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[144,164,95,58,14,155,159,17,132,154,86,2,26,28,3,8,10,9,11])).
% 44.66/44.69 cnf(169,plain,
% 44.66/44.69 (P1(f6(a3,a3))),
% 44.66/44.69 inference(scs_inference,[],[144,164,95,58,14,155,159,17,132,154,138,73,86,2,26,28,3,8,10,9,11,25])).
% 44.66/44.69 cnf(173,plain,
% 44.66/44.69 (P2(f5(f5(x1731)),x1732,f6(x1731,x1732))),
% 44.66/44.69 inference(rename_variables,[],[132])).
% 44.66/44.69 cnf(177,plain,
% 44.66/44.69 (E(f6(a3,a3),f5(a3))),
% 44.66/44.69 inference(scs_inference,[],[144,164,95,58,14,155,159,166,17,16,132,154,158,173,138,73,86,2,26,28,3,8,10,9,11,25,29,27])).
% 44.66/44.69 cnf(185,plain,
% 44.66/44.69 (E(f5(a3),f6(a3,a3))),
% 44.66/44.69 inference(scs_inference,[],[177,2])).
% 44.66/44.69 cnf(186,plain,
% 44.66/44.69 (E(f6(a3,f6(a3,a3)),f5(a3))),
% 44.66/44.69 inference(scs_inference,[],[177,14,167,2,28])).
% 44.66/44.69 cnf(187,plain,
% 44.66/44.69 (P2(f5(x1871),x1871,f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(rename_variables,[],[167])).
% 44.66/44.69 cnf(188,plain,
% 44.66/44.69 (P2(x1881,a3,x1881)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(190,plain,
% 44.66/44.69 (E(f6(a3,f6(x1901,a3)),x1901)),
% 44.66/44.69 inference(scs_inference,[],[177,14,15,148,167,2,28,27])).
% 44.66/44.69 cnf(192,plain,
% 44.66/44.69 (P2(a3,x1921,x1921)),
% 44.66/44.69 inference(rename_variables,[],[15])).
% 44.66/44.69 cnf(194,plain,
% 44.66/44.69 (E(f5(a3),f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[177,14,188,15,148,167,187,2,28,27,26])).
% 44.66/44.69 cnf(195,plain,
% 44.66/44.69 (P2(f5(x1951),x1951,f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(rename_variables,[],[167])).
% 44.66/44.69 cnf(196,plain,
% 44.66/44.69 (P2(x1961,a3,x1961)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(206,plain,
% 44.66/44.69 (P1(f6(f5(a3),a3))),
% 44.66/44.69 inference(scs_inference,[],[19,152,153,157,122,177,14,188,196,16,17,15,169,148,167,187,2,28,27,26,3,10,8,9,11,25])).
% 44.66/44.69 cnf(208,plain,
% 44.66/44.69 (P2(f6(a3,a3),a3,f5(a3))),
% 44.66/44.69 inference(scs_inference,[],[19,152,153,157,122,177,14,188,196,16,17,15,192,169,148,167,187,113,2,28,27,26,3,10,8,9,11,25,30])).
% 44.66/44.69 cnf(209,plain,
% 44.66/44.69 (P2(x2091,f5(x2091),a3)),
% 44.66/44.69 inference(rename_variables,[],[16])).
% 44.66/44.69 cnf(212,plain,
% 44.66/44.69 (P2(f5(a3),f5(a3),f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[19,152,153,157,122,177,14,188,196,16,209,17,15,192,169,148,167,187,195,113,2,28,27,26,3,10,8,9,11,25,30,29])).
% 44.66/44.69 cnf(217,plain,
% 44.66/44.69 (E(x2171,f6(a3,f6(x2171,a3)))),
% 44.66/44.69 inference(scs_inference,[],[190,2])).
% 44.66/44.69 cnf(219,plain,
% 44.66/44.69 (P2(f5(x2191),x2191,f5(f5(a3)))),
% 44.66/44.69 inference(rename_variables,[],[128])).
% 44.66/44.69 cnf(220,plain,
% 44.66/44.69 (P2(x2201,a3,x2201)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(223,plain,
% 44.66/44.69 (P1(f6(a3,f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[190,121,185,14,77,206,128,2,28,10,8])).
% 44.66/44.69 cnf(226,plain,
% 44.66/44.69 (P2(x2261,a3,x2261)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(228,plain,
% 44.66/44.69 (P2(x2281,a3,x2281)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(229,plain,
% 44.66/44.69 (P1(f6(a3,f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[190,121,185,14,220,226,77,206,128,212,126,86,2,28,10,8,11,9,25])).
% 44.66/44.69 cnf(231,plain,
% 44.66/44.69 (P2(f5(a3),f5(a3),f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[190,121,185,14,220,226,228,16,77,206,128,219,212,126,86,2,28,10,8,11,9,25,29])).
% 44.66/44.69 cnf(239,plain,
% 44.66/44.69 (P2(a3,x2391,x2391)),
% 44.66/44.69 inference(rename_variables,[],[15])).
% 44.66/44.69 cnf(245,plain,
% 44.66/44.69 (P2(x2451,a3,x2451)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(250,plain,
% 44.66/44.69 (E(f5(a3),f6(f6(a3,a3),f6(a3,a3)))),
% 44.66/44.69 inference(scs_inference,[],[186,217,152,66,177,14,245,16,15,239,229,165,3,10,8,9,11,29,2])).
% 44.66/44.69 cnf(252,plain,
% 44.66/44.69 (P2(a3,x2521,x2521)),
% 44.66/44.69 inference(rename_variables,[],[15])).
% 44.66/44.69 cnf(255,plain,
% 44.66/44.69 (E(x2551,f5(f5(x2551)))),
% 44.66/44.69 inference(rename_variables,[],[90])).
% 44.66/44.69 cnf(256,plain,
% 44.66/44.69 (P2(x2561,f5(x2561),f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[194,250,90,255,16,15,252,126,10,8,9,11])).
% 44.66/44.69 cnf(265,plain,
% 44.66/44.69 (P2(x2651,a3,x2651)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(272,plain,
% 44.66/44.69 (E(f6(f6(x2721,a3),f5(a3)),x2721)),
% 44.66/44.69 inference(scs_inference,[],[141,31,14,265,17,16,18,15,75,10,9,11,29,26])).
% 44.66/44.69 cnf(380,plain,
% 44.66/44.69 (P2(a3,x3801,f6(f6(x3801,a3),a3))),
% 44.66/44.69 inference(scs_inference,[],[66,185,231,148,10,11])).
% 44.66/44.69 cnf(390,plain,
% 44.66/44.69 (E(f6(f6(x3901,a3),a3),x3901)),
% 44.66/44.69 inference(scs_inference,[],[15,380,27])).
% 44.66/44.69 cnf(391,plain,
% 44.66/44.69 (P2(a3,x3911,x3911)),
% 44.66/44.69 inference(rename_variables,[],[15])).
% 44.66/44.69 cnf(393,plain,
% 44.66/44.69 (P2(a3,x3931,f6(f6(x3931,a3),f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[272,15,391,380,27,10])).
% 44.66/44.69 cnf(403,plain,
% 44.66/44.69 (P2(x4031,x4032,f6(x4031,x4032))),
% 44.66/44.69 inference(rename_variables,[],[18])).
% 44.66/44.69 cnf(404,plain,
% 44.66/44.69 (P2(x4041,a3,f6(a3,x4041))),
% 44.66/44.69 inference(scs_inference,[],[121,152,185,390,18,403,2,3,10,11])).
% 44.66/44.69 cnf(408,plain,
% 44.66/44.69 (P2(x4081,f6(f6(a3,a3),f5(a3)),x4081)),
% 44.66/44.69 inference(scs_inference,[],[121,152,185,390,14,16,18,403,393,2,3,10,11,9,30])).
% 44.66/44.69 cnf(454,plain,
% 44.66/44.69 (P2(x4541,f5(f6(x4541,a3)),a3)),
% 44.66/44.69 inference(scs_inference,[],[38,144,16,15,208,10,11,9])).
% 44.66/44.69 cnf(486,plain,
% 44.66/44.69 (E(f6(a3,x4861),x4861)),
% 44.66/44.69 inference(rename_variables,[],[34])).
% 44.66/44.69 cnf(490,plain,
% 44.66/44.69 (P2(x4901,a3,x4901)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(492,plain,
% 44.66/44.69 (P2(x4921,f5(x4921),a3)),
% 44.66/44.69 inference(rename_variables,[],[16])).
% 44.66/44.69 cnf(498,plain,
% 44.66/44.69 (E(f6(f6(a3,x4981),f5(a3)),x4981)),
% 44.66/44.69 inference(scs_inference,[],[14,490,34,486,185,17,16,492,18,3,10,11,9,29,2,26])).
% 44.66/44.69 cnf(508,plain,
% 44.66/44.69 (P2(x5081,f6(x5082,a3),f6(x5081,f6(a3,x5082)))),
% 44.66/44.69 inference(scs_inference,[],[66,157,498,16,18,15,2,3,11,9,10])).
% 44.66/44.69 cnf(522,plain,
% 44.66/44.69 (P2(f5(a3),a1,f5(a3))),
% 44.66/44.69 inference(scs_inference,[],[223,21,89])).
% 44.66/44.69 cnf(629,plain,
% 44.66/44.69 (P2(a3,x6291,x6291)),
% 44.66/44.69 inference(rename_variables,[],[15])).
% 44.66/44.69 cnf(634,plain,
% 44.66/44.69 (P2(a3,f5(a3),a1)),
% 44.66/44.69 inference(scs_inference,[],[62,16,15,629,522,454,109,404,508,27,10,9,11,30])).
% 44.66/44.69 cnf(1916,plain,
% 44.66/44.69 (~P2(f5(a2),a3,f4(a2))),
% 44.66/44.69 inference(scs_inference,[],[19,14,2,26])).
% 44.66/44.69 cnf(1918,plain,
% 44.66/44.69 (P2(x19181,a3,x19181)),
% 44.66/44.69 inference(rename_variables,[],[14])).
% 44.66/44.69 cnf(1920,plain,
% 44.66/44.69 (~E(f4(a2),f5(a2))),
% 44.66/44.69 inference(scs_inference,[],[1916,19,14,1918,26,9])).
% 44.66/44.69 cnf(2174,plain,
% 44.66/44.69 (~P2(a2,f4(a2),f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[19,256,408,1920,26,27])).
% 44.66/44.69 cnf(2445,plain,
% 44.66/44.69 (~E(a1,f5(f5(a3)))),
% 44.66/44.69 inference(scs_inference,[],[13,2174,23,11])).
% 44.66/44.69 cnf(2446,plain,
% 44.66/44.69 ($false),
% 44.66/44.69 inference(scs_inference,[],[256,2445,634,26]),
% 44.66/44.69 ['proof']).
% 44.66/44.69 % SZS output end Proof
% 44.66/44.69 % Total time :44.050000s
%------------------------------------------------------------------------------