%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP031-1 : 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 : n026.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:33 EDT 2024
% Result : Unsatisfiable 13.96s 14.03s
% Output : CNFRefutation 14.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP031-1 : 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 : n026.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 11:46:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.49/0.55 start to proof:theBenchmark
% 13.96/14.03 %-------------------------------------------
% 13.96/14.03 % File :CSE---1.7
% 13.96/14.03 % Problem :theBenchmark
% 13.96/14.03 % Transform :cnf
% 13.96/14.03 % Format :tptp:raw
% 13.96/14.03 % Command :java -jar mcs_scs.jar %d %s
% 13.96/14.03
% 13.96/14.03 % Result :Theorem 13.440000s
% 13.96/14.03 % Output :CNFRefutation 13.440000s
% 13.96/14.03 %-------------------------------------------
% 13.96/14.03 %--------------------------------------------------------------------------
% 13.96/14.03 % File : GRP031-1 : TPTP v8.2.0. Released v1.0.0.
% 13.96/14.03 % Domain : Group Theory (Semigroups)
% 13.96/14.03 % Problem : In semigroups, left inverse and id => right inverse exists
% 13.96/14.03 % Version : [MOW76] axioms.
% 13.96/14.03 % English : If there are left inverses and left identity, then every
% 13.96/14.03 % element has a right inverse.
% 13.96/14.03
% 13.96/14.03 % Refs : [Wos65] Wos (1965), Unpublished Note
% 13.96/14.03 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 13.96/14.03 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 13.96/14.03 % Source : [SPRFN]
% 13.96/14.03 % Names : Problem 5 [Wos65]
% 13.96/14.03 % : wos5 [WM76]
% 13.96/14.03 % : G4 [MOW76]
% 13.96/14.03 % : invers2.ver1.t [ANL]
% 13.96/14.03
% 13.96/14.03 % Status : Unsatisfiable
% 13.96/14.03 % Rating : 0.06 v8.2.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.00 v2.0.0
% 13.96/14.03 % Syntax : Number of clauses : 7 ( 4 unt; 0 nHn; 4 RR)
% 13.96/14.03 % Number of literals : 15 ( 1 equ; 9 neg)
% 13.96/14.03 % Maximal clause size : 4 ( 2 avg)
% 13.96/14.03 % Maximal term depth : 2 ( 1 avg)
% 13.96/14.03 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 13.96/14.03 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 13.96/14.03 % Number of variables : 21 ( 1 sgn)
% 13.96/14.03 % SPC : CNF_UNS_RFO_SEQ_HRN
% 13.96/14.03
% 13.96/14.03 % Comments : This can also be viewed as a group theory problem, showing
% 13.96/14.03 % that the right inverse axiom is dependant on the rest of the
% 13.96/14.03 % axiom set; i.e., if there is a left inverse then there
% 13.96/14.03 % is a right inverse.
% 13.96/14.03 %--------------------------------------------------------------------------
% 13.96/14.03 %----Include semi-group axioms
% 13.96/14.03 include('Axioms/GRP002-0.ax').
% 13.96/14.03 %--------------------------------------------------------------------------
% 13.96/14.03 cnf(left_identity,hypothesis,
% 13.96/14.03 product(identity,A,A) ).
% 13.96/14.03
% 13.96/14.03 cnf(left_inverse,hypothesis,
% 13.96/14.03 product(inverse(A),A,identity) ).
% 13.96/14.03
% 13.96/14.03 cnf(prove_a_has_an_inverse,negated_conjecture,
% 13.96/14.03 ~ product(a,A,identity) ).
% 13.96/14.03
% 13.96/14.03 %--------------------------------------------------------------------------
% 13.96/14.03 %-------------------------------------------
% 13.96/14.03 % Proof found
% 13.96/14.03 % SZS status Theorem for theBenchmark
% 13.96/14.03 % SZS output start Proof
% 13.96/14.03 %ClaNum:16(EqnAxiom:9)
% 13.96/14.03 %VarNum:41(SingletonVarNum:21)
% 13.96/14.03 %MaxLitNum:4
% 13.96/14.03 %MaxfuncDepth:1
% 13.96/14.03 %SharedTerms:2
% 13.96/14.03 %goalClause: 13
% 13.96/14.04 %singleGoalClaCount:1
% 13.96/14.04 [10]P1(a1,x101,x101)
% 13.96/14.04 [13]~P1(a2,x131,a1)
% 13.96/14.04 [11]P1(f3(x111),x111,a1)
% 13.96/14.04 [12]P1(x121,x122,f4(x121,x122))
% 13.96/14.04 [14]~P1(x143,x144,x141)+E(x141,x142)+~P1(x143,x144,x142)
% 13.96/14.04 [15]~P1(x156,x154,x151)+P1(x151,x152,x153)+~P1(x154,x152,x155)+~P1(x156,x155,x153)
% 13.96/14.04 [16]~P1(x161,x166,x164)+P1(x161,x162,x163)+~P1(x164,x165,x163)+~P1(x166,x165,x162)
% 13.96/14.04 %EqnAxiom
% 13.96/14.04 [1]E(x11,x11)
% 13.96/14.04 [2]E(x22,x21)+~E(x21,x22)
% 13.96/14.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 13.96/14.04 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 13.96/14.04 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 13.96/14.04 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 13.96/14.04 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 13.96/14.04 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 13.96/14.04 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 13.96/14.04
% 13.96/14.04 %-------------------------------------------
% 14.03/14.04 cnf(17,plain,
% 14.03/14.04 (~E(a1,a2)),
% 14.03/14.04 inference(scs_inference,[],[13,10,7])).
% 14.03/14.04 cnf(18,plain,
% 14.03/14.04 (P1(a1,x181,x181)),
% 14.03/14.04 inference(rename_variables,[],[10])).
% 14.03/14.04 cnf(19,plain,
% 14.03/14.04 (~P1(a2,x191,a1)),
% 14.03/14.04 inference(rename_variables,[],[13])).
% 14.03/14.04 cnf(20,plain,
% 14.03/14.04 (E(x201,f4(a1,x201))),
% 14.03/14.04 inference(scs_inference,[],[13,10,18,12,7,14])).
% 14.03/14.04 cnf(21,plain,
% 14.03/14.04 (P1(x211,x212,f4(x211,x212))),
% 14.03/14.04 inference(rename_variables,[],[12])).
% 14.03/14.04 cnf(23,plain,
% 14.03/14.04 (P1(a1,f4(a1,x231),x231)),
% 14.03/14.04 inference(scs_inference,[],[13,10,18,12,7,14,8])).
% 14.03/14.04 cnf(25,plain,
% 14.03/14.04 (P1(x251,x252,f4(x251,x252))),
% 14.03/14.04 inference(rename_variables,[],[12])).
% 14.03/14.04 cnf(26,plain,
% 14.03/14.04 (P1(f4(f3(x261),a1),x261,a1)),
% 14.03/14.04 inference(scs_inference,[],[13,19,10,18,12,21,25,11,7,14,8,9,15])).
% 14.03/14.04 cnf(27,plain,
% 14.03/14.04 (P1(f3(x271),x271,a1)),
% 14.03/14.04 inference(rename_variables,[],[11])).
% 14.03/14.04 cnf(28,plain,
% 14.03/14.04 (P1(x281,x282,f4(x281,x282))),
% 14.03/14.04 inference(rename_variables,[],[12])).
% 14.03/14.04 cnf(30,plain,
% 14.03/14.04 (P1(a1,a1,f4(f3(x301),x301))),
% 14.03/14.04 inference(scs_inference,[],[13,19,10,18,12,21,25,28,11,27,7,14,8,9,15,16])).
% 14.03/14.04 cnf(36,plain,
% 14.03/14.04 (E(f4(a1,x361),x361)),
% 14.03/14.04 inference(scs_inference,[],[20,2])).
% 14.03/14.04 cnf(38,plain,
% 14.03/14.04 (E(f4(f3(x381),x381),a1)),
% 14.03/14.04 inference(scs_inference,[],[30,17,20,10,2,3,14])).
% 14.03/14.04 cnf(39,plain,
% 14.03/14.04 (P1(a1,x391,x391)),
% 14.03/14.04 inference(rename_variables,[],[10])).
% 14.03/14.04 cnf(41,plain,
% 14.03/14.04 (~E(f4(f3(x411),a1),a2)),
% 14.03/14.04 inference(scs_inference,[],[13,26,30,17,20,10,2,3,14,7])).
% 14.03/14.04 cnf(42,plain,
% 14.03/14.04 (P1(f4(f3(x421),a1),x421,a1)),
% 14.03/14.04 inference(rename_variables,[],[26])).
% 14.03/14.04 cnf(44,plain,
% 14.03/14.04 (P1(f4(f3(x441),a1),x441,a1)),
% 14.03/14.04 inference(rename_variables,[],[26])).
% 14.03/14.04 cnf(45,plain,
% 14.03/14.04 (E(x451,f4(a1,x451))),
% 14.03/14.04 inference(rename_variables,[],[20])).
% 14.03/14.04 cnf(48,plain,
% 14.03/14.04 (P1(f4(f3(x481),x481),f4(a1,x482),x482)),
% 14.03/14.04 inference(scs_inference,[],[13,26,42,44,30,17,20,45,23,10,39,2,3,14,7,8,9,15])).
% 14.03/14.04 cnf(51,plain,
% 14.03/14.04 (P1(a1,f4(f3(a1),a1),a1)),
% 14.03/14.04 inference(scs_inference,[],[13,26,42,44,30,17,20,45,23,10,39,2,3,14,7,8,9,15,16])).
% 14.03/14.04 cnf(55,plain,
% 14.03/14.04 (E(a1,f4(f3(x551),x551))),
% 14.03/14.04 inference(scs_inference,[],[38,2])).
% 14.03/14.04 cnf(56,plain,
% 14.03/14.04 (E(f4(a1,f4(a1,x561)),x561)),
% 14.03/14.04 inference(scs_inference,[],[38,12,23,2,14])).
% 14.03/14.04 cnf(57,plain,
% 14.03/14.04 (P1(x571,x572,f4(x571,x572))),
% 14.03/14.04 inference(rename_variables,[],[12])).
% 14.03/14.04 cnf(60,plain,
% 14.03/14.04 (E(f4(a1,x601),x601)),
% 14.03/14.04 inference(rename_variables,[],[36])).
% 14.03/14.04 cnf(62,plain,
% 14.03/14.04 (P1(f4(f3(x621),x621),f4(a1,x622),x622)),
% 14.03/14.04 inference(rename_variables,[],[48])).
% 14.03/14.04 cnf(63,plain,
% 14.03/14.04 (~E(f4(f3(x631),x631),a2)),
% 14.03/14.04 inference(scs_inference,[],[13,48,62,41,36,60,38,12,23,2,14,3,8,7])).
% 14.03/14.04 cnf(64,plain,
% 14.03/14.04 (P1(f4(f3(x641),x641),f4(a1,x642),x642)),
% 14.03/14.04 inference(rename_variables,[],[48])).
% 14.03/14.04 cnf(65,plain,
% 14.03/14.04 (~P1(a2,x651,a1)),
% 14.03/14.04 inference(rename_variables,[],[13])).
% 14.03/14.04 cnf(68,plain,
% 14.03/14.04 (~P1(f4(a1,a2),x681,a1)),
% 14.03/14.04 inference(scs_inference,[],[13,65,48,62,64,51,41,26,36,60,38,12,23,20,2,14,3,8,7,9,15])).
% 14.03/14.04 cnf(70,plain,
% 14.03/14.04 (P1(f4(f3(x701),x701),f4(a1,x702),x702)),
% 14.03/14.04 inference(rename_variables,[],[48])).
% 14.03/14.04 cnf(72,plain,
% 14.03/14.04 (P1(a1,x721,f4(a1,f4(a1,x721)))),
% 14.03/14.04 inference(scs_inference,[],[13,65,48,62,64,70,51,41,26,36,60,38,12,57,23,20,2,14,3,8,7,9,15,16])).
% 14.03/14.04 cnf(76,plain,
% 14.03/14.04 (E(x761,f4(a1,f4(a1,x761)))),
% 14.03/14.04 inference(scs_inference,[],[56,2])).
% 14.03/14.04 cnf(79,plain,
% 14.03/14.04 (~E(f3(x791),a2)),
% 14.03/14.04 inference(scs_inference,[],[13,63,56,36,11,2,3,7])).
% 14.03/14.04 cnf(80,plain,
% 14.03/14.05 (P1(f3(x801),x801,a1)),
% 14.03/14.05 inference(rename_variables,[],[11])).
% 14.03/14.05 cnf(81,plain,
% 14.03/14.05 (P1(f4(f3(x811),x811),x812,f4(a1,x812))),
% 14.03/14.05 inference(scs_inference,[],[13,63,48,56,36,11,2,3,7,8])).
% 14.03/14.05 cnf(84,plain,
% 14.03/14.05 (P1(f4(a1,f4(a1,a1)),a1,f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[13,72,63,48,56,55,36,11,80,23,2,3,7,8,9,15])).
% 14.03/14.05 cnf(89,plain,
% 14.03/14.05 (~E(f3(a2),a1)),
% 14.03/14.05 inference(scs_inference,[],[13,72,63,48,56,55,36,11,80,23,2,3,7,8,9,15,5])).
% 14.03/14.05 cnf(90,plain,
% 14.03/14.05 (~E(f3(a2),f4(f3(x901),x901))),
% 14.03/14.05 inference(scs_inference,[],[89,38,3])).
% 14.03/14.05 cnf(91,plain,
% 14.03/14.05 (P1(f4(a1,f4(a1,x911)),x912,f4(x911,x912))),
% 14.03/14.05 inference(scs_inference,[],[76,89,38,12,3,7])).
% 14.03/14.05 cnf(97,plain,
% 14.03/14.05 (P1(f4(a1,a1),f4(f3(a1),a1),f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[84,51,76,89,38,10,12,11,3,7,8,9,15])).
% 14.03/14.05 cnf(100,plain,
% 14.03/14.05 (E(f4(a1,x1001),x1001)),
% 14.03/14.05 inference(rename_variables,[],[36])).
% 14.03/14.05 cnf(101,plain,
% 14.03/14.05 (P1(f4(a1,x1011),x1012,f4(x1011,x1012))),
% 14.03/14.05 inference(scs_inference,[],[91,79,36,100,3,7])).
% 14.03/14.05 cnf(102,plain,
% 14.03/14.05 (E(f4(a1,x1021),x1021)),
% 14.03/14.05 inference(rename_variables,[],[36])).
% 14.03/14.05 cnf(105,plain,
% 14.03/14.05 (P1(f4(a1,a1),f4(f3(a1),a1),a1)),
% 14.03/14.05 inference(scs_inference,[],[97,91,79,55,36,100,102,10,3,7,8,9])).
% 14.03/14.05 cnf(107,plain,
% 14.03/14.05 (P1(f4(a1,a1),f4(a1,x1071),f4(f4(a1,a1),x1071))),
% 14.03/14.05 inference(scs_inference,[],[97,91,79,48,55,36,100,102,10,12,3,7,8,9,15])).
% 14.03/14.05 cnf(108,plain,
% 14.03/14.05 (P1(x1081,x1082,f4(x1081,x1082))),
% 14.03/14.05 inference(rename_variables,[],[12])).
% 14.03/14.05 cnf(109,plain,
% 14.03/14.05 (P1(f4(f3(x1091),x1091),f4(a1,x1092),x1092)),
% 14.03/14.05 inference(rename_variables,[],[48])).
% 14.03/14.05 cnf(111,plain,
% 14.03/14.05 (P1(f4(a1,a1),x1111,f4(f4(a1,a1),f4(a1,x1111)))),
% 14.03/14.05 inference(scs_inference,[],[97,91,79,48,109,55,36,100,102,10,12,108,3,7,8,9,15,16])).
% 14.03/14.05 cnf(115,plain,
% 14.03/14.05 (E(f4(f4(a1,a1),f4(a1,x1151)),f4(a1,x1151))),
% 14.03/14.05 inference(scs_inference,[],[111,101,14])).
% 14.03/14.05 cnf(116,plain,
% 14.03/14.05 (P1(f4(a1,x1161),x1162,f4(x1161,x1162))),
% 14.03/14.05 inference(rename_variables,[],[101])).
% 14.03/14.05 cnf(119,plain,
% 14.03/14.05 (E(f4(a1,f4(a1,x1191)),x1191)),
% 14.03/14.05 inference(rename_variables,[],[56])).
% 14.03/14.05 cnf(120,plain,
% 14.03/14.05 (P1(f4(a1,a1),a1,a1)),
% 14.03/14.05 inference(scs_inference,[],[111,101,17,105,56,38,14,3,8])).
% 14.03/14.05 cnf(122,plain,
% 14.03/14.05 (P1(x1221,x1222,f4(f4(a1,x1221),x1222))),
% 14.03/14.05 inference(scs_inference,[],[111,101,116,17,105,56,119,38,14,3,8,7])).
% 14.03/14.05 cnf(124,plain,
% 14.03/14.05 (P1(f4(a1,f4(a1,a1)),f4(a1,x1241),x1241)),
% 14.03/14.05 inference(scs_inference,[],[111,101,116,91,17,105,56,119,38,14,3,8,7,9])).
% 14.03/14.05 cnf(126,plain,
% 14.03/14.05 (E(f4(a1,x1261),f4(f4(a1,a1),f4(a1,x1261)))),
% 14.03/14.05 inference(scs_inference,[],[111,101,116,91,17,105,56,119,38,14,3,8,7,9,2])).
% 14.03/14.05 cnf(129,plain,
% 14.03/14.05 (E(f4(f4(a1,a1),f4(a1,x1291)),x1291)),
% 14.03/14.05 inference(scs_inference,[],[122,23,14])).
% 14.03/14.05 cnf(130,plain,
% 14.03/14.05 (P1(x1301,x1302,f4(f4(a1,x1301),x1302))),
% 14.03/14.05 inference(rename_variables,[],[122])).
% 14.03/14.05 cnf(135,plain,
% 14.03/14.05 (P1(f4(f4(a1,a1),f4(a1,x1351)),x1352,f4(x1351,x1352))),
% 14.03/14.05 inference(scs_inference,[],[122,101,79,126,120,55,56,23,14,3,8,7])).
% 14.03/14.05 cnf(138,plain,
% 14.03/14.05 (P1(x1381,x1382,f4(f4(a1,x1381),x1382))),
% 14.03/14.05 inference(rename_variables,[],[122])).
% 14.03/14.05 cnf(139,plain,
% 14.03/14.05 (P1(a1,f4(f4(a1,a1),a1),a1)),
% 14.03/14.05 inference(scs_inference,[],[13,30,122,130,138,101,79,26,126,120,55,56,23,14,3,8,7,9,16])).
% 14.03/14.05 cnf(144,plain,
% 14.03/14.05 (E(x1441,f4(f4(a1,a1),f4(a1,x1441)))),
% 14.03/14.05 inference(scs_inference,[],[13,30,122,130,138,101,79,26,126,120,55,56,23,14,3,8,7,9,16,2])).
% 14.03/14.05 cnf(145,plain,
% 14.03/14.05 (E(f4(f3(x1451),x1451),f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[30,12,14])).
% 14.03/14.05 cnf(150,plain,
% 14.03/14.05 (~E(f4(a1,f4(a1,a1)),a2)),
% 14.03/14.05 inference(scs_inference,[],[13,30,144,124,120,12,14,8,7])).
% 14.03/14.05 cnf(153,plain,
% 14.03/14.05 (P1(f4(a1,a1),f4(a1,f4(a1,x1531)),x1531)),
% 14.03/14.05 inference(scs_inference,[],[13,30,107,129,144,124,120,12,14,8,7,9])).
% 14.03/14.05 cnf(155,plain,
% 14.03/14.05 (P1(f4(x1551,a1),f4(f4(a1,a1),a1),f4(x1551,a1))),
% 14.03/14.05 inference(scs_inference,[],[13,30,135,107,139,129,144,124,120,12,14,8,7,9,15])).
% 14.03/14.05 cnf(159,plain,
% 14.03/14.05 (P1(a1,f4(f4(a1,a1),f4(a1,x1591)),x1591)),
% 14.03/14.05 inference(scs_inference,[],[13,30,135,107,139,122,48,129,144,124,120,12,14,8,7,9,15,16])).
% 14.03/14.05 cnf(163,plain,
% 14.03/14.05 (E(f4(a1,a1),f4(f3(x1631),x1631))),
% 14.03/14.05 inference(scs_inference,[],[13,30,135,107,139,122,48,129,144,124,120,12,14,8,7,9,15,16,2])).
% 14.03/14.05 cnf(164,plain,
% 14.03/14.05 (~E(f3(a2),f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[13,30,135,107,139,122,48,129,144,124,90,120,12,14,8,7,9,15,16,2,3])).
% 14.03/14.05 cnf(169,plain,
% 14.03/14.05 (~E(f4(a1,a1),a2)),
% 14.03/14.05 inference(scs_inference,[],[13,150,97,145,153,36,3,8,7])).
% 14.03/14.05 cnf(182,plain,
% 14.03/14.05 (~E(f4(a1,a1),f4(f4(a1,a1),f4(a1,a2)))),
% 14.03/14.05 inference(scs_inference,[],[169,129,3])).
% 14.03/14.05 cnf(183,plain,
% 14.03/14.05 (E(f4(f4(a1,a1),f4(a1,x1831)),x1831)),
% 14.03/14.05 inference(rename_variables,[],[129])).
% 14.03/14.05 cnf(186,plain,
% 14.03/14.05 (P1(f4(a1,a1),x1861,x1861)),
% 14.03/14.05 inference(scs_inference,[],[169,111,163,129,183,10,3,8,9])).
% 14.03/14.05 cnf(188,plain,
% 14.03/14.05 (E(f4(a1,a1),f4(f4(a1,a1),a1))),
% 14.03/14.05 inference(scs_inference,[],[155,186,14])).
% 14.03/14.05 cnf(189,plain,
% 14.03/14.05 (P1(f4(a1,a1),x1891,x1891)),
% 14.03/14.05 inference(rename_variables,[],[186])).
% 14.03/14.05 cnf(195,plain,
% 14.03/14.05 (P1(f4(a1,a1),x1951,x1951)),
% 14.03/14.05 inference(rename_variables,[],[186])).
% 14.03/14.05 cnf(196,plain,
% 14.03/14.05 (P1(f4(a1,a1),f4(a1,a1),f4(f3(x1961),x1961))),
% 14.03/14.05 inference(scs_inference,[],[155,163,126,186,189,195,182,14,3,8,9])).
% 14.03/14.05 cnf(198,plain,
% 14.03/14.05 (E(f4(f4(a1,a1),a1),f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[188,2])).
% 14.03/14.05 cnf(201,plain,
% 14.03/14.05 (P1(f4(a1,x2011),f4(f4(a1,a1),f4(a1,x2012)),f4(x2011,x2012))),
% 14.03/14.05 inference(scs_inference,[],[169,101,144,56,188,2,3,8])).
% 14.03/14.05 cnf(213,plain,
% 14.03/14.05 (P1(f4(f4(a1,a1),f4(a1,a2)),f4(a1,a2),f4(a2,a2))),
% 14.03/14.05 inference(scs_inference,[],[68,115,126,10,198,164,201,3,8,9,16,7])).
% 14.03/14.05 cnf(221,plain,
% 14.03/14.05 (P1(a2,f4(a1,a2),f4(a2,a2))),
% 14.03/14.05 inference(scs_inference,[],[101,213,91,129,14,7])).
% 14.03/14.05 cnf(238,plain,
% 14.03/14.05 (P1(x2381,x2382,f4(a1,f4(x2381,x2382)))),
% 14.03/14.05 inference(scs_inference,[],[48,101,144,81,11,9,15])).
% 14.03/14.05 cnf(261,plain,
% 14.03/14.05 (P1(f4(a1,f4(a1,a2)),f4(a1,a2),f4(a2,a2))),
% 14.03/14.05 inference(scs_inference,[],[221,76,7])).
% 14.03/14.05 cnf(262,plain,
% 14.03/14.05 (E(x2621,f4(a1,f4(a1,x2621)))),
% 14.03/14.05 inference(rename_variables,[],[76])).
% 14.03/14.05 cnf(264,plain,
% 14.03/14.05 (P1(f4(a1,x2641),x2642,f4(x2641,x2642))),
% 14.03/14.05 inference(rename_variables,[],[101])).
% 14.03/14.05 cnf(267,plain,
% 14.03/14.05 (~P1(a2,x2671,f4(a1,f4(a1,a1)))),
% 14.03/14.05 inference(scs_inference,[],[101,264,221,68,76,262,186,153,7,8,9,15])).
% 14.03/14.05 cnf(273,plain,
% 14.03/14.05 (~P1(f4(a1,a2),x2731,f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[48,267,38,81,196,9,15])).
% 14.03/14.05 cnf(277,plain,
% 14.03/14.05 (~E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a2))),
% 14.03/14.05 inference(scs_inference,[],[273,135,7])).
% 14.03/14.05 cnf(279,plain,
% 14.03/14.05 (~P1(f4(a1,a2),x2791,f4(a1,a1))),
% 14.03/14.05 inference(rename_variables,[],[273])).
% 14.03/14.05 cnf(280,plain,
% 14.03/14.05 (P1(x2801,f4(f3(x2802),x2802),f4(x2801,a1))),
% 14.03/14.05 inference(scs_inference,[],[273,135,55,12,7,8])).
% 14.03/14.05 cnf(282,plain,
% 14.03/14.05 (~E(f4(a2,x2821),f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[101,273,279,135,55,12,7,8,9])).
% 14.03/14.05 cnf(384,plain,
% 14.03/14.05 (P1(f4(f4(a1,a1),a1),f4(a1,x3841),x3841)),
% 14.03/14.05 inference(scs_inference,[],[10,101,122,144,12,124,14,8,15])).
% 14.03/14.05 cnf(385,plain,
% 14.03/14.05 (P1(f4(a1,x3851),x3852,f4(x3851,x3852))),
% 14.03/14.05 inference(rename_variables,[],[101])).
% 14.03/14.05 cnf(386,plain,
% 14.03/14.05 (P1(a1,x3861,x3861)),
% 14.03/14.05 inference(rename_variables,[],[10])).
% 14.03/14.05 cnf(388,plain,
% 14.03/14.05 (P1(a1,f4(f4(a1,a2),f4(a1,a2)),f4(a2,a2))),
% 14.03/14.05 inference(scs_inference,[],[10,386,261,101,385,122,144,12,124,14,8,15,16])).
% 14.03/14.05 cnf(418,plain,
% 14.03/14.05 (P1(f3(x4181),x4181,a1)),
% 14.03/14.05 inference(rename_variables,[],[11])).
% 14.03/14.05 cnf(419,plain,
% 14.03/14.05 (~P1(f4(f4(a1,a1),f4(a1,a2)),x4191,a1)),
% 14.03/14.05 inference(scs_inference,[],[11,13,159,10,144,145,282,3,8,15])).
% 14.03/14.05 cnf(421,plain,
% 14.03/14.05 (P1(a1,f4(f4(a1,a1),f4(a1,x4211)),x4211)),
% 14.03/14.05 inference(rename_variables,[],[159])).
% 14.03/14.05 cnf(423,plain,
% 14.03/14.05 (P1(f3(a1),x4231,x4231)),
% 14.03/14.05 inference(scs_inference,[],[11,418,13,159,421,10,144,145,282,3,8,15,16])).
% 14.03/14.05 cnf(430,plain,
% 14.03/14.05 (E(x4301,f4(a1,x4301))),
% 14.03/14.05 inference(rename_variables,[],[20])).
% 14.03/14.05 cnf(431,plain,
% 14.03/14.05 (P1(f3(x4311),f4(a1,x4311),a1)),
% 14.03/14.05 inference(scs_inference,[],[11,388,20,430,7,8])).
% 14.03/14.05 cnf(432,plain,
% 14.03/14.05 (P1(f3(x4321),x4321,a1)),
% 14.03/14.05 inference(rename_variables,[],[11])).
% 14.03/14.05 cnf(433,plain,
% 14.03/14.05 (P1(f3(x4331),x4331,f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[11,432,388,20,430,7,8,9])).
% 14.03/14.05 cnf(444,plain,
% 14.03/14.05 (~P1(f4(f4(a1,a1),f4(a1,a2)),x4441,f4(a1,a1))),
% 14.03/14.05 inference(scs_inference,[],[11,13,159,23,76,431,8,9,15])).
% 14.03/14.05 cnf(456,plain,
% 14.03/14.05 (~P1(f4(f4(a1,a1),f4(a1,a2)),x4561,f4(a1,a1))),
% 14.03/14.05 inference(rename_variables,[],[444])).
% 14.03/14.05 cnf(460,plain,
% 14.03/14.05 (~P1(f4(a1,a2),x4601,f4(a1,f4(a1,a1)))),
% 14.03/14.05 inference(scs_inference,[],[101,444,456,55,12,124,433,431,7,8,9,15])).
% 14.03/14.05 cnf(470,plain,
% 14.03/14.05 (~P1(f4(a1,a2),x4701,f4(f4(a1,a1),f4(a1,a1)))),
% 14.03/14.05 inference(scs_inference,[],[101,122,159,460,419,9,15])).
% 14.03/14.05 cnf(481,plain,
% 14.03/14.05 (P1(f3(x4811),f4(x4811,x4812),f4(a1,f4(a1,x4812)))),
% 14.03/14.05 inference(scs_inference,[],[11,101,238,470,12,9,16])).
% 14.03/14.05 cnf(535,plain,
% 14.03/14.05 (P1(f4(f3(a1),f4(a1,a1)),f4(a1,x5351),x5351)),
% 14.03/14.05 inference(scs_inference,[],[12,101,423,76,8,15])).
% 14.03/14.05 cnf(539,plain,
% 14.03/14.05 (~E(f4(f3(a1),f4(a1,a1)),a2)),
% 14.03/14.05 inference(scs_inference,[],[12,13,101,423,76,8,15,7])).
% 14.03/14.05 cnf(1667,plain,
% 14.03/14.05 (P1(f4(a1,x16671),x16672,f4(x16671,f4(a1,x16672)))),
% 14.03/14.05 inference(scs_inference,[],[36,101,8])).
% 14.03/14.05 cnf(1675,plain,
% 14.03/14.05 (P1(f3(x16751),f4(x16751,x16752),f4(a1,x16752))),
% 14.03/14.05 inference(scs_inference,[],[36,122,481,1667,7,8,9])).
% 14.03/14.05 cnf(1684,plain,
% 14.03/14.05 (P1(f3(x16841),f4(x16841,x16842),f4(a1,x16842))),
% 14.03/14.05 inference(rename_variables,[],[1675])).
% 14.03/14.05 cnf(1688,plain,
% 14.03/14.05 (P1(f3(x16881),f4(x16881,x16882),x16882)),
% 14.03/14.05 inference(scs_inference,[],[36,384,277,1675,1684,14,8,9])).
% 14.03/14.05 cnf(1696,plain,
% 14.03/14.05 (P1(f3(x16961),f4(x16961,x16962),x16962)),
% 14.03/14.05 inference(rename_variables,[],[1688])).
% 14.03/14.05 cnf(1700,plain,
% 14.03/14.05 (P1(f3(x17001),f4(x17001,f4(a1,x17002)),x17002)),
% 14.03/14.05 inference(scs_inference,[],[36,535,539,1688,1696,14,8,9])).
% 14.03/14.05 cnf(1740,plain,
% 14.03/14.05 ($false),
% 14.03/14.05 inference(scs_inference,[],[41,280,1700,14]),
% 14.03/14.05 ['proof']).
% 14.03/14.05 % SZS output end Proof
% 14.03/14.05 % Total time :13.440000s
%------------------------------------------------------------------------------