%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP030-1 : 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 : n023.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 3.96s 4.09s
% Output : CNFRefutation 4.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP030-1 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 20 11:07:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.18/0.56 start to proof:theBenchmark
% 3.96/4.09 %-------------------------------------------
% 3.96/4.09 % File :CSE---1.7
% 3.96/4.09 % Problem :theBenchmark
% 3.96/4.09 % Transform :cnf
% 3.96/4.09 % Format :tptp:raw
% 3.96/4.09 % Command :java -jar mcs_scs.jar %d %s
% 3.96/4.09
% 3.96/4.09 % Result :Theorem 3.490000s
% 3.96/4.09 % Output :CNFRefutation 3.490000s
% 3.96/4.09 %-------------------------------------------
% 3.96/4.09 %--------------------------------------------------------------------------
% 3.96/4.09 % File : GRP030-1 : TPTP v8.2.0. Released v1.0.0.
% 3.96/4.09 % Domain : Group Theory (Semigroups)
% 3.96/4.09 % Problem : In semigroups, left id and inverse => left id=right id
% 3.96/4.09 % Version : [MOW76] axioms.
% 3.96/4.09 % English : If there are a left identity and left inverse, then the left
% 3.96/4.09 % identity is also a right identity.
% 3.96/4.09
% 3.96/4.09 % Refs : [Wos65] Wos (1965), Unpublished Note
% 3.96/4.09 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 3.96/4.09 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 3.96/4.09 % Source : [SPRFN]
% 3.96/4.09 % Names : Problem 2 [Wos65]
% 3.96/4.09 % : wos2 [WM76]
% 3.96/4.09 % : G3 [MOW76]
% 3.96/4.09 % : ident1.ver1.in [ANL]
% 3.96/4.09
% 3.96/4.09 % Status : Unsatisfiable
% 3.96/4.09 % Rating : 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.29 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.0.0
% 3.96/4.09 % Syntax : Number of clauses : 7 ( 4 unt; 0 nHn; 4 RR)
% 3.96/4.09 % Number of literals : 15 ( 1 equ; 9 neg)
% 3.96/4.09 % Maximal clause size : 4 ( 2 avg)
% 3.96/4.09 % Maximal term depth : 2 ( 1 avg)
% 3.96/4.09 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 3.96/4.09 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 3.96/4.09 % Number of variables : 20 ( 0 sgn)
% 3.96/4.09 % SPC : CNF_UNS_RFO_SEQ_HRN
% 3.96/4.09
% 3.96/4.09 % Comments : This can also be viewed as a group theory problem, showing
% 3.96/4.09 % that the right identity axiom is dependant on the rest of the
% 3.96/4.09 % axiom set; i.e., if e is the left identity, then e is also
% 3.96/4.09 % a right identity.
% 3.96/4.09 %--------------------------------------------------------------------------
% 3.96/4.09 %----Include semi-group axioms
% 3.96/4.09 include('Axioms/GRP002-0.ax').
% 3.96/4.09 %--------------------------------------------------------------------------
% 3.96/4.09 cnf(left_identity,hypothesis,
% 3.96/4.09 product(identity,A,A) ).
% 3.96/4.09
% 3.96/4.09 cnf(left_inverse,hypothesis,
% 3.96/4.09 product(inverse(A),A,identity) ).
% 3.96/4.09
% 3.96/4.09 cnf(prove_identity_is_a_right_identity,negated_conjecture,
% 3.96/4.09 ~ product(a,identity,a) ).
% 3.96/4.09
% 3.96/4.09 %--------------------------------------------------------------------------
% 3.96/4.09 %-------------------------------------------
% 3.96/4.09 % Proof found
% 3.96/4.09 % SZS status Theorem for theBenchmark
% 3.96/4.09 % SZS output start Proof
% 3.96/4.10 %ClaNum:16(EqnAxiom:9)
% 3.96/4.10 %VarNum:40(SingletonVarNum:20)
% 3.96/4.10 %MaxLitNum:4
% 3.96/4.10 %MaxfuncDepth:1
% 3.96/4.10 %SharedTerms:3
% 3.96/4.10 %goalClause: 13
% 3.96/4.10 %singleGoalClaCount:1
% 3.96/4.10 [13]~P1(a2,a1,a2)
% 3.96/4.10 [10]P1(a1,x101,x101)
% 3.96/4.10 [11]P1(f3(x111),x111,a1)
% 3.96/4.10 [12]P1(x121,x122,f4(x121,x122))
% 3.96/4.10 [14]~P1(x143,x144,x141)+E(x141,x142)+~P1(x143,x144,x142)
% 3.96/4.10 [15]~P1(x156,x154,x151)+P1(x151,x152,x153)+~P1(x154,x152,x155)+~P1(x156,x155,x153)
% 3.96/4.10 [16]~P1(x161,x166,x164)+P1(x161,x162,x163)+~P1(x164,x165,x163)+~P1(x166,x165,x162)
% 3.96/4.10 %EqnAxiom
% 3.96/4.10 [1]E(x11,x11)
% 3.96/4.10 [2]E(x22,x21)+~E(x21,x22)
% 3.96/4.10 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 3.96/4.10 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 3.96/4.10 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 3.96/4.10 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 3.96/4.10 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 3.96/4.10 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 3.96/4.10 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 3.96/4.10
% 3.96/4.10 %-------------------------------------------
% 3.96/4.10 cnf(17,plain,
% 3.96/4.10 (E(x171,f4(a1,x171))),
% 3.96/4.10 inference(scs_inference,[],[10,12,14])).
% 3.96/4.10 cnf(18,plain,
% 3.96/4.10 (P1(x181,x182,f4(x181,x182))),
% 3.96/4.10 inference(rename_variables,[],[12])).
% 3.96/4.10 cnf(20,plain,
% 3.96/4.10 (P1(a1,f4(a1,x201),x201)),
% 3.96/4.10 inference(scs_inference,[],[10,12,14,8])).
% 3.96/4.10 cnf(21,plain,
% 3.96/4.10 (~E(f4(a2,a1),a2)),
% 3.96/4.10 inference(scs_inference,[],[13,10,12,18,14,8,9])).
% 3.96/4.10 cnf(22,plain,
% 3.96/4.10 (P1(x221,x222,f4(x221,x222))),
% 3.96/4.10 inference(rename_variables,[],[12])).
% 3.96/4.10 cnf(23,plain,
% 3.96/4.10 (P1(f4(f3(x231),a1),x231,a1)),
% 3.96/4.10 inference(scs_inference,[],[13,10,12,18,22,11,14,8,9,15])).
% 3.96/4.10 cnf(24,plain,
% 3.96/4.10 (P1(f3(x241),x241,a1)),
% 3.96/4.10 inference(rename_variables,[],[11])).
% 3.96/4.10 cnf(25,plain,
% 3.96/4.10 (P1(x251,x252,f4(x251,x252))),
% 3.96/4.10 inference(rename_variables,[],[12])).
% 3.96/4.10 cnf(27,plain,
% 3.96/4.10 (P1(a1,a1,f4(f3(x271),x271))),
% 3.96/4.10 inference(scs_inference,[],[13,10,12,18,22,25,11,24,14,8,9,15,16])).
% 3.96/4.10 cnf(29,plain,
% 3.96/4.10 (P1(a1,x291,x291)),
% 3.96/4.10 inference(rename_variables,[],[10])).
% 3.96/4.10 cnf(33,plain,
% 3.96/4.10 (P1(x331,x332,x332)+~E(a1,x331)),
% 3.96/4.10 inference(scs_inference,[],[13,10,29,12,18,22,25,11,24,14,8,9,15,16,2,7])).
% 3.96/4.10 cnf(35,plain,
% 3.96/4.10 (P1(f4(a1,a1),x351,x351)),
% 3.96/4.10 inference(scs_inference,[],[17,33])).
% 3.96/4.10 cnf(36,plain,
% 3.96/4.10 (E(x361,f4(a1,x361))),
% 3.96/4.10 inference(rename_variables,[],[17])).
% 3.96/4.10 cnf(37,plain,
% 3.96/4.10 (E(f4(a1,x371),x371)),
% 3.96/4.10 inference(scs_inference,[],[17,36,33,2])).
% 3.96/4.10 cnf(38,plain,
% 3.96/4.10 (~E(f4(a2,a1),f4(a1,a2))),
% 3.96/4.10 inference(scs_inference,[],[17,36,21,33,2,3])).
% 3.96/4.10 cnf(39,plain,
% 3.96/4.10 (E(f4(f3(x391),x391),a1)),
% 3.96/4.10 inference(scs_inference,[],[17,36,21,12,11,33,2,3,14])).
% 3.96/4.10 cnf(41,plain,
% 3.96/4.10 (P1(x411,x412,f4(x411,x412))),
% 3.96/4.10 inference(rename_variables,[],[12])).
% 3.96/4.10 cnf(44,plain,
% 3.96/4.10 (E(x441,f4(a1,x441))),
% 3.96/4.10 inference(rename_variables,[],[17])).
% 3.96/4.10 cnf(46,plain,
% 3.96/4.10 (E(x461,f4(a1,x461))),
% 3.96/4.10 inference(rename_variables,[],[17])).
% 3.96/4.10 cnf(47,plain,
% 3.96/4.10 (P1(f4(f3(x471),a1),f4(a1,x471),a1)),
% 3.96/4.10 inference(scs_inference,[],[23,27,17,36,44,46,21,12,11,33,2,3,14,9,7,8])).
% 3.96/4.10 cnf(48,plain,
% 3.96/4.10 (P1(f4(f3(x481),a1),x481,a1)),
% 3.96/4.10 inference(rename_variables,[],[23])).
% 3.96/4.10 cnf(49,plain,
% 3.96/4.10 (P1(f4(f3(x491),x491),x492,x492)),
% 3.96/4.10 inference(scs_inference,[],[23,27,17,36,44,46,20,21,12,41,11,33,2,3,14,9,7,8,15])).
% 3.96/4.10 cnf(53,plain,
% 3.96/4.10 (P1(a1,f4(f3(a1),a1),a1)),
% 3.96/4.10 inference(scs_inference,[],[23,48,27,17,36,44,46,20,21,12,41,11,33,2,3,14,9,7,8,15,16])).
% 3.96/4.10 cnf(57,plain,
% 3.96/4.10 (E(a1,f4(f3(x571),x571))),
% 3.96/4.10 inference(scs_inference,[],[39,2])).
% 3.96/4.10 cnf(58,plain,
% 3.96/4.10 (~E(f4(a2,a1),f4(a1,f4(a1,a2)))),
% 3.96/4.10 inference(scs_inference,[],[37,38,39,2,3])).
% 3.96/4.10 cnf(59,plain,
% 3.96/4.10 (E(f4(a1,x591),x591)),
% 3.96/4.10 inference(rename_variables,[],[37])).
% 3.96/4.10 cnf(60,plain,
% 3.96/4.10 (P1(f4(f3(x601),x601),f4(a1,x602),x602)),
% 3.96/4.10 inference(scs_inference,[],[49,37,59,38,39,2,3,9])).
% 3.96/4.10 cnf(61,plain,
% 3.96/4.10 (P1(f4(f3(x611),x611),x612,x612)),
% 3.96/4.10 inference(rename_variables,[],[49])).
% 3.96/4.10 cnf(64,plain,
% 3.96/4.10 (P1(f4(f3(x641),x641),x642,f4(a1,x642))),
% 3.96/4.10 inference(scs_inference,[],[49,61,53,37,59,38,39,17,2,3,9,7,8])).
% 3.96/4.10 cnf(73,plain,
% 3.96/4.10 (E(x731,f4(f4(a1,a1),x731))),
% 3.96/4.10 inference(scs_inference,[],[35,12,14])).
% 3.96/4.10 cnf(74,plain,
% 3.96/4.10 (P1(x741,x742,f4(x741,x742))),
% 3.96/4.10 inference(rename_variables,[],[12])).
% 3.96/4.10 cnf(76,plain,
% 3.96/4.10 (E(f4(a1,a1),f4(f3(x761),x761))),
% 3.96/4.10 inference(scs_inference,[],[35,57,37,12,14,3])).
% 3.96/4.10 cnf(78,plain,
% 3.96/4.11 (P1(f4(a1,f3(x781)),x781,a1)),
% 3.96/4.11 inference(scs_inference,[],[35,57,37,17,12,11,14,3,7])).
% 3.96/4.11 cnf(83,plain,
% 3.96/4.11 (P1(f4(a1,a1),x831,x831)),
% 3.96/4.11 inference(rename_variables,[],[35])).
% 3.96/4.11 cnf(84,plain,
% 3.96/4.11 (P1(f4(f3(x841),f4(a1,a1)),x841,a1)),
% 3.96/4.11 inference(scs_inference,[],[35,83,57,37,20,17,12,74,11,14,3,7,9,8,15])).
% 3.96/4.11 cnf(88,plain,
% 3.96/4.11 (P1(f4(a1,a1),x881,f4(a1,x881))),
% 3.96/4.11 inference(scs_inference,[],[35,83,49,60,57,37,20,17,12,74,11,14,3,7,9,8,15,16])).
% 3.96/4.11 cnf(93,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),a1),x931,x931)),
% 3.96/4.11 inference(scs_inference,[],[35,83,49,60,57,37,20,17,12,74,11,14,3,7,9,8,15,16,33])).
% 3.96/4.11 cnf(95,plain,
% 3.96/4.11 (E(f4(f4(a1,a1),x951),x951)),
% 3.96/4.11 inference(scs_inference,[],[73,2])).
% 3.96/4.11 cnf(96,plain,
% 3.96/4.11 (E(a1,f4(a1,f4(a1,a1)))),
% 3.96/4.11 inference(scs_inference,[],[84,73,64,2,14])).
% 3.96/4.11 cnf(98,plain,
% 3.96/4.11 (P1(f4(f3(x981),f4(a1,a1)),x981,a1)),
% 3.96/4.11 inference(rename_variables,[],[84])).
% 3.96/4.11 cnf(100,plain,
% 3.96/4.11 (P1(f4(a1,a1),x1001,f4(f4(a1,a1),f4(a1,x1001)))),
% 3.96/4.11 inference(scs_inference,[],[88,84,73,64,2,14,9])).
% 3.96/4.11 cnf(101,plain,
% 3.96/4.11 (E(x1011,f4(f4(a1,a1),x1011))),
% 3.96/4.11 inference(rename_variables,[],[73])).
% 3.96/4.11 cnf(102,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f4(a1,a1)),x1021,f4(a1,x1021))),
% 3.96/4.11 inference(scs_inference,[],[88,84,73,101,64,2,14,9,7])).
% 3.96/4.11 cnf(103,plain,
% 3.96/4.11 (E(x1031,f4(f4(a1,a1),x1031))),
% 3.96/4.11 inference(rename_variables,[],[73])).
% 3.96/4.11 cnf(106,plain,
% 3.96/4.11 (P1(a1,f4(f4(a1,a1),a1),a1)),
% 3.96/4.11 inference(scs_inference,[],[93,88,84,98,73,101,103,64,2,14,9,7,8,15])).
% 3.96/4.11 cnf(108,plain,
% 3.96/4.11 (P1(f4(f3(x1081),f4(a1,a1)),x1081,a1)),
% 3.96/4.11 inference(rename_variables,[],[84])).
% 3.96/4.11 cnf(109,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),a1),x1091,x1091)),
% 3.96/4.11 inference(rename_variables,[],[93])).
% 3.96/4.11 cnf(111,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),a1),f4(a1,a1),a1)),
% 3.96/4.11 inference(scs_inference,[],[93,109,88,84,98,108,49,73,101,103,64,2,14,9,7,8,15,16])).
% 3.96/4.11 cnf(117,plain,
% 3.96/4.11 (E(f4(f3(x1171),x1171),f4(a1,a1))),
% 3.96/4.11 inference(scs_inference,[],[76,2])).
% 3.96/4.11 cnf(118,plain,
% 3.96/4.11 (P1(f4(a1,f4(a1,a1)),f4(a1,x1181),x1181)),
% 3.96/4.11 inference(scs_inference,[],[76,96,20,2,7])).
% 3.96/4.11 cnf(121,plain,
% 3.96/4.11 (P1(a1,x1211,f4(f4(a1,a1),x1211))),
% 3.96/4.11 inference(scs_inference,[],[35,95,76,96,20,10,2,7,9,8])).
% 3.96/4.11 cnf(130,plain,
% 3.96/4.11 (P1(f4(a1,a1),x1301,x1301)),
% 3.96/4.11 inference(rename_variables,[],[35])).
% 3.96/4.11 cnf(133,plain,
% 3.96/4.11 (E(f4(f3(x1331),x1331),f4(a1,a1))),
% 3.96/4.11 inference(rename_variables,[],[117])).
% 3.96/4.11 cnf(135,plain,
% 3.96/4.11 (P1(f4(a1,a1),x1351,x1351)),
% 3.96/4.11 inference(rename_variables,[],[35])).
% 3.96/4.11 cnf(136,plain,
% 3.96/4.11 (~P1(f4(a1,a2),a1,f4(a1,a2))),
% 3.96/4.11 inference(scs_inference,[],[13,118,84,35,130,117,133,96,2,9,7,8,15])).
% 3.96/4.11 cnf(138,plain,
% 3.96/4.11 (P1(f4(a1,f4(a1,a1)),f4(a1,x1381),x1381)),
% 3.96/4.11 inference(rename_variables,[],[118])).
% 3.96/4.11 cnf(140,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,x1401),x1401)),
% 3.96/4.11 inference(scs_inference,[],[13,102,118,138,84,35,130,135,117,133,96,2,9,7,8,15,16])).
% 3.96/4.11 cnf(142,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f4(a1,a1)),x1421,f4(a1,x1421))),
% 3.96/4.11 inference(rename_variables,[],[102])).
% 3.96/4.11 cnf(144,plain,
% 3.96/4.11 (E(f4(a1,f4(a1,x1441)),x1441)),
% 3.96/4.11 inference(scs_inference,[],[13,102,142,118,138,84,35,130,135,117,133,96,2,9,7,8,15,16,14])).
% 3.96/4.11 cnf(147,plain,
% 3.96/4.11 (E(x1471,f4(a1,f4(a1,x1471)))),
% 3.96/4.11 inference(scs_inference,[],[144,2])).
% 3.96/4.11 cnf(148,plain,
% 3.96/4.11 (P1(f4(a1,a1),f4(a1,x1481),x1481)),
% 3.96/4.11 inference(scs_inference,[],[140,144,95,2,7])).
% 3.96/4.11 cnf(162,plain,
% 3.96/4.11 (E(x1621,f4(f4(a1,a1),f4(a1,x1621)))),
% 3.96/4.11 inference(scs_inference,[],[148,12,14])).
% 3.96/4.11 cnf(163,plain,
% 3.96/4.11 (P1(x1631,x1632,f4(x1631,x1632))),
% 3.96/4.11 inference(rename_variables,[],[12])).
% 3.96/4.11 cnf(166,plain,
% 3.96/4.11 (P1(f4(a1,a1),x1661,x1661)),
% 3.96/4.11 inference(rename_variables,[],[35])).
% 3.96/4.11 cnf(167,plain,
% 3.96/4.11 (P1(f4(a1,f4(a1,x1671)),x1672,f4(x1671,x1672))),
% 3.96/4.11 inference(scs_inference,[],[148,35,147,12,163,14,9,7])).
% 3.96/4.11 cnf(178,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f4(a1,a1)),x1781,x1781)),
% 3.96/4.11 inference(scs_inference,[],[148,136,106,111,140,102,35,166,147,121,12,163,14,9,7,8,15,16,33])).
% 3.96/4.11 cnf(180,plain,
% 3.96/4.11 (E(f4(f4(a1,a1),f4(a1,x1801)),x1801)),
% 3.96/4.11 inference(scs_inference,[],[162,2])).
% 3.96/4.11 cnf(181,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f4(a1,x1811)),x1812,f4(x1811,x1812))),
% 3.96/4.11 inference(scs_inference,[],[162,12,2,7])).
% 3.96/4.11 cnf(193,plain,
% 3.96/4.11 (P1(a1,x1931,x1931)),
% 3.96/4.11 inference(rename_variables,[],[10])).
% 3.96/4.11 cnf(194,plain,
% 3.96/4.11 (P1(a1,f4(f4(a1,a1),f4(a1,x1941)),x1941)),
% 3.96/4.11 inference(scs_inference,[],[180,10,193,8,9])).
% 3.96/4.11 cnf(196,plain,
% 3.96/4.11 (P1(f4(a1,x1961),x1962,f4(x1961,x1962))),
% 3.96/4.11 inference(scs_inference,[],[167,180,37,10,193,8,9,7])).
% 3.96/4.11 cnf(205,plain,
% 3.96/4.11 (E(f4(f4(a1,x2051),x2052),f4(x2051,x2052))),
% 3.96/4.11 inference(scs_inference,[],[196,167,14])).
% 3.96/4.11 cnf(210,plain,
% 3.96/4.11 (P1(a1,f4(f3(x2101),x2101),f4(a1,a1))),
% 3.96/4.11 inference(scs_inference,[],[196,167,58,76,10,14,3,8])).
% 3.96/4.11 cnf(224,plain,
% 3.96/4.11 (E(f4(x2241,x2242),f4(f4(a1,x2241),x2242))),
% 3.96/4.11 inference(scs_inference,[],[205,2])).
% 3.96/4.11 cnf(226,plain,
% 3.96/4.11 (P1(f4(a1,a1),x2261,x2261)),
% 3.96/4.11 inference(rename_variables,[],[35])).
% 3.96/4.11 cnf(227,plain,
% 3.96/4.11 (P1(f4(a1,a1),f4(f4(a1,x2271),x2272),f4(x2271,x2272))),
% 3.96/4.11 inference(scs_inference,[],[35,226,205,2,8,9])).
% 3.96/4.11 cnf(238,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),x2381),x2382,f4(x2381,x2382))),
% 3.96/4.11 inference(scs_inference,[],[196,224,7])).
% 3.96/4.11 cnf(240,plain,
% 3.96/4.11 (E(f4(x2401,x2402),f4(f4(a1,x2401),x2402))),
% 3.96/4.11 inference(rename_variables,[],[224])).
% 3.96/4.11 cnf(241,plain,
% 3.96/4.11 (P1(a1,f4(f4(a1,a1),x2411),x2411)),
% 3.96/4.11 inference(scs_inference,[],[196,224,240,20,7,8])).
% 3.96/4.11 cnf(243,plain,
% 3.96/4.11 (E(f4(x2431,x2432),f4(f4(a1,x2431),x2432))),
% 3.96/4.11 inference(rename_variables,[],[224])).
% 3.96/4.11 cnf(244,plain,
% 3.96/4.11 (P1(a1,f4(x2441,x2442),f4(f4(a1,x2441),x2442))),
% 3.96/4.11 inference(scs_inference,[],[196,224,240,243,20,10,7,8,9])).
% 3.96/4.11 cnf(251,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f3(x2511)),x2511,a1)),
% 3.96/4.11 inference(scs_inference,[],[78,224,7])).
% 3.96/4.11 cnf(259,plain,
% 3.96/4.11 (P1(x2591,x2592,f4(f4(a1,x2591),x2592))),
% 3.96/4.11 inference(scs_inference,[],[238,180,7])).
% 3.96/4.11 cnf(261,plain,
% 3.96/4.11 (~E(f4(f4(a1,a2),a1),a2)),
% 3.96/4.11 inference(scs_inference,[],[13,238,180,7,9])).
% 3.96/4.11 cnf(272,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(a1,a1))),
% 3.96/4.11 inference(scs_inference,[],[251,210,16])).
% 3.96/4.11 cnf(275,plain,
% 3.96/4.11 (E(f4(a1,a1),f4(f3(a1),f4(a1,a1)))),
% 3.96/4.11 inference(scs_inference,[],[272,238,14])).
% 3.96/4.11 cnf(278,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f3(a1)),f4(x2781,x2782),f4(x2781,x2782))),
% 3.96/4.11 inference(scs_inference,[],[272,238,227,14,16])).
% 3.96/4.11 cnf(280,plain,
% 3.96/4.11 (E(f4(f3(a1),f4(a1,a1)),f4(a1,a1))),
% 3.96/4.11 inference(scs_inference,[],[272,238,227,14,16,2])).
% 3.96/4.11 cnf(281,plain,
% 3.96/4.11 (E(f4(x2811,x2812),f4(f3(a1),f4(x2811,x2812)))),
% 3.96/4.11 inference(scs_inference,[],[278,238,14])).
% 3.96/4.11 cnf(292,plain,
% 3.96/4.11 (P1(f4(f4(a1,a1),f3(a1)),x2921,x2921)),
% 3.96/4.11 inference(scs_inference,[],[278,178,238,196,148,35,280,261,275,37,14,3,7,9,8,16])).
% 3.96/4.11 cnf(295,plain,
% 3.96/4.11 (E(f4(f3(a1),f4(x2951,x2952)),f4(x2951,x2952))),
% 3.96/4.11 inference(scs_inference,[],[281,2])).
% 4.11/4.11 cnf(296,plain,
% 4.11/4.11 (E(x2961,f4(f3(a1),x2961))),
% 4.11/4.11 inference(scs_inference,[],[292,238,281,2,14])).
% 4.11/4.11 cnf(299,plain,
% 4.11/4.11 (P1(f4(f3(a1),f4(a1,x2991)),x2992,f4(x2991,x2992))),
% 4.11/4.11 inference(scs_inference,[],[292,238,196,281,2,14,7])).
% 4.11/4.11 cnf(301,plain,
% 4.11/4.11 (E(f4(x3011,x3012),f4(f3(a1),f4(x3011,x3012)))),
% 4.11/4.11 inference(rename_variables,[],[281])).
% 4.11/4.11 cnf(307,plain,
% 4.11/4.11 (P1(f4(f4(a1,a1),f3(a1)),x3071,f4(a1,x3071))),
% 4.11/4.11 inference(scs_inference,[],[292,181,178,238,196,148,35,281,301,2,14,7,9,8,16])).
% 4.11/4.11 cnf(312,plain,
% 4.11/4.11 (E(f4(f3(a1),x3121),x3121)),
% 4.11/4.11 inference(scs_inference,[],[296,2])).
% 4.11/4.11 cnf(317,plain,
% 4.11/4.11 (E(x3171,f4(f3(a1),x3171))),
% 4.11/4.11 inference(rename_variables,[],[296])).
% 4.11/4.11 cnf(320,plain,
% 4.11/4.11 (P1(a1,f4(f3(a1),f4(a1,x3201)),x3201)),
% 4.11/4.11 inference(scs_inference,[],[307,238,148,35,295,296,317,20,2,14,7,9,8])).
% 4.11/4.11 cnf(336,plain,
% 4.11/4.11 (E(f4(f3(a1),f4(a1,x3361)),x3361)),
% 4.11/4.11 inference(scs_inference,[],[10,320,14])).
% 4.11/4.11 cnf(363,plain,
% 4.11/4.11 (P1(f3(a1),x3631,f4(a1,x3631))),
% 4.11/4.11 inference(scs_inference,[],[307,95,7])).
% 4.11/4.11 cnf(370,plain,
% 4.11/4.11 (P1(f4(a1,f3(a1)),x3701,x3701)),
% 4.11/4.11 inference(scs_inference,[],[292,205,7])).
% 4.11/4.11 cnf(381,plain,
% 4.11/4.11 (P1(f3(a1),a1,f4(f3(x3811),x3811))),
% 4.11/4.11 inference(scs_inference,[],[363,76,9])).
% 4.11/4.11 cnf(383,plain,
% 4.11/4.11 (P1(a1,f4(a1,f3(a1)),a1)),
% 4.11/4.11 inference(scs_inference,[],[370,363,47,76,9,15])).
% 4.11/4.11 cnf(388,plain,
% 4.11/4.11 (P1(a1,f3(a1),a1)),
% 4.11/4.11 inference(scs_inference,[],[10,383,20,16])).
% 4.11/4.11 cnf(390,plain,
% 4.11/4.11 (P1(a1,x3901,x3901)),
% 4.11/4.11 inference(rename_variables,[],[10])).
% 4.11/4.11 cnf(392,plain,
% 4.11/4.11 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),a1)),
% 4.11/4.11 inference(scs_inference,[],[10,383,162,20,16,7])).
% 4.11/4.11 cnf(393,plain,
% 4.11/4.11 (E(x3931,f4(f4(a1,a1),f4(a1,x3931)))),
% 4.11/4.11 inference(rename_variables,[],[162])).
% 4.11/4.11 cnf(398,plain,
% 4.11/4.11 (E(x3981,a1)+~P1(f3(a1),x3981,f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[10,390,383,162,393,20,16,7,9,15,14])).
% 4.11/4.11 cnf(402,plain,
% 4.11/4.11 (P1(f4(a1,f4(a1,a1)),f3(a1),a1)),
% 4.11/4.11 inference(scs_inference,[],[388,147,7])).
% 4.11/4.11 cnf(408,plain,
% 4.11/4.11 (E(a1,f4(a1,f3(a1)))),
% 4.11/4.11 inference(scs_inference,[],[392,181,14])).
% 4.11/4.11 cnf(412,plain,
% 4.11/4.11 (E(x4121,f4(f4(a1,a1),x4121))),
% 4.11/4.11 inference(rename_variables,[],[73])).
% 4.11/4.11 cnf(413,plain,
% 4.11/4.11 (P1(a1,f4(f4(a1,a1),f3(a1)),a1)),
% 4.11/4.11 inference(scs_inference,[],[392,388,181,73,412,14,7,8])).
% 4.11/4.11 cnf(414,plain,
% 4.11/4.11 (E(x4141,f4(f4(a1,a1),x4141))),
% 4.11/4.11 inference(rename_variables,[],[73])).
% 4.11/4.11 cnf(418,plain,
% 4.11/4.11 (E(f3(a1),a1)),
% 4.11/4.11 inference(scs_inference,[],[392,388,181,73,412,414,17,14,7,8,9,2,3])).
% 4.11/4.11 cnf(420,plain,
% 4.11/4.11 (E(a1,f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[418,2])).
% 4.11/4.11 cnf(421,plain,
% 4.11/4.11 (E(f4(a1,f4(a1,a1)),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[144,418,2,3])).
% 4.11/4.11 cnf(423,plain,
% 4.11/4.11 (E(a1,f4(f4(a1,a1),f3(a1)))),
% 4.11/4.11 inference(scs_inference,[],[402,196,144,418,2,3,14])).
% 4.11/4.11 cnf(430,plain,
% 4.11/4.11 (P1(f3(a1),x4301,x4301)),
% 4.11/4.11 inference(scs_inference,[],[388,402,196,363,147,144,418,2,3,14,8,9,33])).
% 4.11/4.11 cnf(432,plain,
% 4.11/4.11 (E(f4(a1,a1),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[17,421,2,3])).
% 4.11/4.11 cnf(439,plain,
% 4.11/4.11 (E(f4(f3(x4391),x4391),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[39,423,420,2,3])).
% 4.11/4.11 cnf(441,plain,
% 4.11/4.11 (E(x4411,f4(a1,x4411))),
% 4.11/4.11 inference(rename_variables,[],[17])).
% 4.11/4.11 cnf(446,plain,
% 4.11/4.11 (P1(f4(x4461,a1),a1,f4(x4461,a1))),
% 4.11/4.11 inference(scs_inference,[],[392,388,299,196,17,441,39,423,420,2,3,7,8,9,15])).
% 4.11/4.11 cnf(449,plain,
% 4.11/4.11 (E(f3(a1),f4(a1,a1))),
% 4.11/4.11 inference(scs_inference,[],[432,2])).
% 4.11/4.11 cnf(450,plain,
% 4.11/4.11 (E(f4(f4(a1,a1),a1),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[95,432,420,2,3])).
% 4.11/4.11 cnf(461,plain,
% 4.11/4.11 (E(f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[180,439,420,2,3])).
% 4.11/4.11 cnf(463,plain,
% 4.11/4.11 (P1(f4(f4(a1,a1),f4(x4631,a1)),a1,f4(x4631,a1))),
% 4.11/4.11 inference(scs_inference,[],[446,73,180,439,420,2,3,7])).
% 4.11/4.11 cnf(477,plain,
% 4.11/4.11 (E(f4(f3(a1),f3(a1)),f4(a1,a1))),
% 4.11/4.11 inference(scs_inference,[],[312,449,450,2,3])).
% 4.11/4.11 cnf(488,plain,
% 4.11/4.11 (E(f4(a1,a1),f4(f3(a1),f3(a1)))),
% 4.11/4.11 inference(scs_inference,[],[477,2])).
% 4.11/4.11 cnf(489,plain,
% 4.11/4.11 (E(f4(f3(a1),f4(a1,a1)),f3(a1))),
% 4.11/4.11 inference(scs_inference,[],[336,477,420,2,3])).
% 4.11/4.11 cnf(502,plain,
% 4.11/4.11 (E(f4(a1,a1),f4(a1,f3(a1)))),
% 4.11/4.11 inference(scs_inference,[],[37,408,461,2,3])).
% 4.11/4.11 cnf(514,plain,
% 4.11/4.11 (E(a1,f4(f3(a1),f3(a1)))),
% 4.11/4.11 inference(scs_inference,[],[17,502,488,2,3])).
% 4.11/4.11 cnf(515,plain,
% 4.11/4.11 (E(x5151,f4(a1,x5151))),
% 4.11/4.11 inference(rename_variables,[],[17])).
% 4.11/4.11 cnf(517,plain,
% 4.11/4.11 (E(x5171,f4(a1,x5171))),
% 4.11/4.11 inference(rename_variables,[],[17])).
% 4.11/4.11 cnf(518,plain,
% 4.11/4.11 (P1(f4(a1,x5181),f4(a1,x5182),f4(x5181,x5182))),
% 4.11/4.11 inference(scs_inference,[],[196,383,17,515,517,502,488,2,3,7,8])).
% 4.11/4.11 cnf(532,plain,
% 4.11/4.11 (~P1(f4(f4(a1,a2),f3(x5321)),x5321,a2)),
% 4.11/4.11 inference(scs_inference,[],[13,259,147,12,489,11,2,8,9,16])).
% 4.11/4.11 cnf(535,plain,
% 4.11/4.11 (~E(a1,f4(f4(a1,a2),f3(a2)))),
% 4.11/4.11 inference(scs_inference,[],[10,13,259,147,12,489,11,2,8,9,16,7])).
% 4.11/4.11 cnf(546,plain,
% 4.11/4.11 (~E(f4(a1,a1),f4(f4(a1,a2),f3(a2)))),
% 4.11/4.11 inference(scs_inference,[],[35,532,535,224,514,2,3,7])).
% 4.11/4.11 cnf(563,plain,
% 4.11/4.11 (P1(f4(a1,f4(x5631,a1)),a1,f4(x5631,a1))),
% 4.11/4.11 inference(scs_inference,[],[546,446,17,224,3,7])).
% 4.11/4.11 cnf(569,plain,
% 4.11/4.11 (~E(f3(a1),f4(f4(a1,a2),f3(a2)))),
% 4.11/4.11 inference(scs_inference,[],[532,430,7])).
% 4.11/4.11 cnf(591,plain,
% 4.11/4.11 (E(x5911,f4(f4(a1,a1),x5911))),
% 4.11/4.11 inference(rename_variables,[],[73])).
% 4.11/4.11 cnf(592,plain,
% 4.11/4.11 (P1(f3(x5921),x5921,f4(f4(a1,a1),a1))),
% 4.11/4.11 inference(scs_inference,[],[446,73,591,11,8,9])).
% 4.11/4.11 cnf(596,plain,
% 4.11/4.11 (P1(x5961,f4(f4(a1,a1),x5962),f4(x5961,x5962))),
% 4.11/4.11 inference(scs_inference,[],[73,12,8])).
% 4.11/4.11 cnf(618,plain,
% 4.11/4.11 (P1(f4(x6181,a1),f3(a1),f4(x6181,a1))),
% 4.11/4.11 inference(scs_inference,[],[388,463,15])).
% 4.11/4.11 cnf(626,plain,
% 4.11/4.11 (E(x6261,f4(a1,x6261))),
% 4.11/4.11 inference(rename_variables,[],[17])).
% 4.11/4.11 cnf(627,plain,
% 4.11/4.11 (P1(f3(x6271),f4(a1,x6271),a1)),
% 4.11/4.11 inference(scs_inference,[],[11,618,17,626,7,8])).
% 4.11/4.11 cnf(649,plain,
% 4.11/4.11 (P1(f4(a1,f3(x6491)),f4(a1,x6491),a1)),
% 4.11/4.11 inference(scs_inference,[],[17,627,7])).
% 4.11/4.11 cnf(664,plain,
% 4.11/4.11 (E(x6641,f4(a1,x6641))),
% 4.11/4.11 inference(rename_variables,[],[17])).
% 4.11/4.11 cnf(665,plain,
% 4.11/4.11 (P1(x6651,f4(a1,x6652),f4(x6651,x6652))),
% 4.11/4.11 inference(scs_inference,[],[12,17,664,518,9,8])).
% 4.11/4.11 cnf(704,plain,
% 4.11/4.12 (~P1(f3(a1),f4(f4(a1,a2),f3(a2)),f3(a1))),
% 4.11/4.12 inference(scs_inference,[],[535,2,398])).
% 4.11/4.12 cnf(713,plain,
% 4.11/4.12 (~E(f4(f4(a1,a2),f3(a2)),a1)),
% 4.11/4.12 inference(scs_inference,[],[12,259,704,430,73,420,665,9,8,16,3])).
% 4.11/4.12 cnf(776,plain,
% 4.11/4.12 (~E(f4(a2,f3(a2)),f3(a1))),
% 4.11/4.12 inference(scs_inference,[],[388,713,244,14,8])).
% 4.11/4.12 cnf(791,plain,
% 4.11/4.12 (~P1(f4(a2,a1),f4(f4(a1,a1),a1),a2)),
% 4.11/4.12 inference(scs_inference,[],[12,13,196,546,17,241,420,776,381,14,3,8,16])).
% 4.11/4.12 cnf(798,plain,
% 4.11/4.12 (P1(x7981,x7982,f4(x7981,x7982))),
% 4.11/4.12 inference(rename_variables,[],[12])).
% 4.11/4.12 cnf(800,plain,
% 4.11/4.12 (~P1(f4(a2,a1),f4(f4(a1,a1),f4(a1,a1)),a2)),
% 4.11/4.12 inference(scs_inference,[],[12,798,13,569,194,14,16])).
% 4.11/4.12 cnf(827,plain,
% 4.11/4.12 (~P1(f4(a2,a1),f4(f4(a1,a1),f3(a1)),a2)),
% 4.11/4.12 inference(scs_inference,[],[12,13,196,535,413,14,16])).
% 4.11/4.12 cnf(830,plain,
% 4.11/4.12 (~P1(f4(a1,a1),f4(f4(a1,a2),f3(a2)),f4(a1,a1))),
% 4.11/4.12 inference(scs_inference,[],[17,546,33,14])).
% 4.11/4.12 cnf(836,plain,
% 4.11/4.12 (~P1(a1,f4(f4(a1,a2),f3(a2)),a1)),
% 4.11/4.12 inference(scs_inference,[],[196,563,569,830,227,14,9,15])).
% 4.11/4.12 cnf(839,plain,
% 4.11/4.12 (~P1(f4(f4(a2,a1),f3(x8391)),x8391,a2)),
% 4.11/4.12 inference(scs_inference,[],[12,196,791,563,569,830,592,227,14,9,15,16])).
% 4.11/4.12 cnf(842,plain,
% 4.11/4.12 (~E(f4(f4(a2,a1),f3(a2)),a1)),
% 4.11/4.12 inference(scs_inference,[],[839,33,2])).
% 4.11/4.12 cnf(847,plain,
% 4.11/4.12 (~E(f4(f4(a2,a1),f3(a2)),f3(a1))),
% 4.11/4.12 inference(scs_inference,[],[388,842,418,398,14,3])).
% 4.11/4.12 cnf(848,plain,
% 4.11/4.12 (~E(f4(a1,a1),f4(f4(a2,a1),f3(a2)))),
% 4.11/4.12 inference(scs_inference,[],[388,35,839,842,418,398,14,3,7])).
% 4.11/4.12 cnf(853,plain,
% 4.11/4.12 (~P1(f4(a1,x8531),f4(f4(a1,a2),f3(a2)),f4(a1,x8531))),
% 4.11/4.12 inference(scs_inference,[],[388,35,800,649,836,839,596,842,418,398,14,3,7,9,15])).
% 4.11/4.12 cnf(860,plain,
% 4.11/4.12 (P1(x8601,x8602,f4(x8601,x8602))),
% 4.11/4.12 inference(rename_variables,[],[12])).
% 4.11/4.12 cnf(865,plain,
% 4.11/4.12 (~P1(x8651,f4(f4(a1,a2),f3(a2)),x8651)),
% 4.11/4.12 inference(scs_inference,[],[12,860,848,827,853,432,847,596,14,3,9,15])).
% 4.11/4.12 cnf(878,plain,
% 4.11/4.12 (P1(x8781,x8782,f4(x8781,x8782))),
% 4.11/4.12 inference(rename_variables,[],[12])).
% 4.11/4.12 cnf(879,plain,
% 4.11/4.12 (~P1(x8791,f4(f4(a1,a2),f3(a2)),x8791)),
% 4.11/4.12 inference(rename_variables,[],[865])).
% 4.11/4.12 cnf(881,plain,
% 4.11/4.12 ($false),
% 4.11/4.12 inference(scs_inference,[],[12,878,196,259,865,879,848,49,100,14,15,16]),
% 4.11/4.12 ['proof']).
% 4.11/4.12 % SZS output end Proof
% 4.11/4.12 % Total time :3.490000s
%------------------------------------------------------------------------------