%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP043-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:37 EDT 2024
% Result : Unsatisfiable 58.73s 58.79s
% Output : CNFRefutation 58.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP043-2 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n027.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 09:23:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 58.73/58.78 %-------------------------------------------
% 58.73/58.78 % File :CSE---1.7
% 58.73/58.78 % Problem :theBenchmark
% 58.73/58.78 % Transform :cnf
% 58.73/58.78 % Format :tptp:raw
% 58.73/58.78 % Command :java -jar mcs_scs.jar %d %s
% 58.73/58.78
% 58.73/58.78 % Result :Theorem 58.150000s
% 58.73/58.78 % Output :CNFRefutation 58.150000s
% 58.73/58.78 %-------------------------------------------
% 58.73/58.78 %--------------------------------------------------------------------------
% 58.73/58.79 % File : GRP043-2 : TPTP v8.2.0. Released v1.0.0.
% 58.73/58.79 % Domain : Group Theory
% 58.73/58.79 % Problem : Transitivity is dependent
% 58.73/58.79 % Version : [Ver92] axioms.
% 58.73/58.79 % English :
% 58.73/58.79
% 58.73/58.79 % Refs : [Ver92] Veroff (1992), Email to G. Sutcliffe
% 58.73/58.79 % Source : [Ver92]
% 58.73/58.79 % Names : - [Ver92]
% 58.73/58.79
% 58.73/58.79 % Status : Unsatisfiable
% 58.73/58.79 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.00 v2.0.0
% 58.73/58.79 % Syntax : Number of clauses : 10 ( 6 unt; 0 nHn; 7 RR)
% 58.73/58.79 % Number of literals : 20 ( 0 equ; 11 neg)
% 58.73/58.79 % Maximal clause size : 4 ( 2 avg)
% 58.73/58.79 % Maximal term depth : 2 ( 1 avg)
% 58.73/58.79 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 58.73/58.79 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 58.73/58.79 % Number of variables : 24 ( 0 sgn)
% 58.73/58.79 % SPC : CNF_UNS_RFO_NEQ_HRN
% 58.73/58.79
% 58.73/58.79 % Comments :
% 58.73/58.79 %--------------------------------------------------------------------------
% 58.73/58.79 %----Include Veroff's minimal axiom set
% 58.73/58.79 include('Axioms/GRP005-0.ax').
% 58.73/58.79 %--------------------------------------------------------------------------
% 58.73/58.79 cnf(a_equals_b,hypothesis,
% 58.73/58.79 equalish(a,b) ).
% 58.73/58.79
% 58.73/58.79 cnf(b_equals_c,hypothesis,
% 58.73/58.79 equalish(b,c) ).
% 58.73/58.79
% 58.73/58.79 cnf(prove_transitivity,negated_conjecture,
% 58.73/58.79 ~ equalish(a,c) ).
% 58.73/58.79
% 58.73/58.79 %--------------------------------------------------------------------------
% 58.73/58.79 %-------------------------------------------
% 58.73/58.79 % Proof found
% 58.73/58.79 % SZS status Theorem for theBenchmark
% 58.73/58.79 % SZS output start Proof
% 58.73/58.79 %ClaNum:10(EqnAxiom:0)
% 58.73/58.79 %VarNum:48(SingletonVarNum:24)
% 58.73/58.79 %MaxLitNum:4
% 58.73/58.79 %MaxfuncDepth:1
% 58.73/58.79 %SharedTerms:7
% 58.73/58.79 %goalClause: 6
% 58.73/58.79 %singleGoalClaCount:1
% 58.73/58.79 [1]P1(a1,a2)
% 58.73/58.79 [2]P1(a2,a3)
% 58.73/58.79 [6]~P1(a1,a3)
% 58.73/58.79 [3]P2(a4,x31,x31)
% 58.73/58.79 [4]P2(f5(x41),x41,a4)
% 58.73/58.79 [5]P2(x51,x52,f6(x51,x52))
% 58.73/58.79 [7]~P2(x71,x72,x74)+P2(x71,x72,x73)+~P1(x74,x73)
% 58.73/58.79 [8]~P2(x83,x84,x81)+P1(x81,x82)+~P2(x83,x84,x82)
% 58.73/58.79 [9]~P2(x96,x94,x91)+P2(x91,x92,x93)+~P2(x94,x92,x95)+~P2(x96,x95,x93)
% 58.73/58.79 [10]~P2(x101,x106,x104)+P2(x101,x102,x103)+~P2(x104,x105,x103)+~P2(x106,x105,x102)
% 58.73/58.79 %EqnAxiom
% 58.73/58.79
% 58.73/58.79 %-------------------------------------------
% 58.73/58.80 cnf(13,plain,
% 58.73/58.80 (P2(a4,a1,a2)),
% 58.73/58.80 inference(scs_inference,[],[3,1,8,7])).
% 58.73/58.80 cnf(14,plain,
% 58.73/58.80 (P2(a4,x141,x141)),
% 58.73/58.80 inference(rename_variables,[],[3])).
% 58.73/58.80 cnf(16,plain,
% 58.73/58.80 (P2(f6(f5(x161),a4),x161,a4)),
% 58.73/58.80 inference(scs_inference,[],[3,14,5,4,1,8,7,9])).
% 58.73/58.80 cnf(25,plain,
% 58.73/58.80 (P2(a4,a2,a3)),
% 58.73/58.80 inference(scs_inference,[],[3,2,7])).
% 58.73/58.80 cnf(26,plain,
% 58.73/58.80 (P2(a4,x261,x261)),
% 58.73/58.80 inference(rename_variables,[],[3])).
% 58.73/58.80 cnf(28,plain,
% 58.73/58.80 (P1(x281,f6(a4,x281))),
% 58.73/58.80 inference(scs_inference,[],[3,26,5,2,7,8])).
% 58.73/58.80 cnf(29,plain,
% 58.73/58.80 (P2(x291,x292,f6(x291,x292))),
% 58.73/58.80 inference(rename_variables,[],[5])).
% 58.73/58.80 cnf(36,plain,
% 58.73/58.80 (P2(a2,x361,a2)+~P2(a1,x361,a1)),
% 58.73/58.80 inference(scs_inference,[],[3,26,13,5,29,4,2,7,8,10,9])).
% 58.73/58.80 cnf(42,plain,
% 58.73/58.80 (P2(a4,f6(f5(x421),x421),a4)),
% 58.73/58.80 inference(scs_inference,[],[3,5,4,8,7])).
% 58.73/58.80 cnf(45,plain,
% 58.73/58.80 (P2(a3,x451,a3)+~P2(a2,x451,a2)),
% 58.73/58.80 inference(scs_inference,[],[3,25,5,4,8,7,9])).
% 58.73/58.80 cnf(60,plain,
% 58.73/58.80 (P2(f5(x601),x601,f6(a4,a4))),
% 58.73/58.80 inference(scs_inference,[],[4,28,7])).
% 58.73/58.80 cnf(63,plain,
% 58.73/58.80 (P1(a4,f6(f5(x631),x631))),
% 58.73/58.80 inference(scs_inference,[],[4,28,5,7,8])).
% 58.73/58.80 cnf(64,plain,
% 58.73/58.80 (P2(x641,x642,f6(x641,x642))),
% 58.73/58.80 inference(rename_variables,[],[5])).
% 58.73/58.80 cnf(66,plain,
% 58.73/58.80 (P2(f5(a4),x661,x661)),
% 58.73/58.80 inference(scs_inference,[],[4,3,28,5,7,8,10])).
% 58.73/58.80 cnf(67,plain,
% 58.73/58.80 (P2(f5(x671),x671,a4)),
% 58.73/58.80 inference(rename_variables,[],[4])).
% 58.73/58.80 cnf(69,plain,
% 58.73/58.80 (P2(a4,x691,f6(f5(a4),x691))),
% 58.73/58.80 inference(scs_inference,[],[4,67,3,28,5,64,7,8,10,9])).
% 58.73/58.80 cnf(74,plain,
% 58.73/58.80 (P2(f5(x741),x741,f6(f5(x742),x742))),
% 58.73/58.80 inference(scs_inference,[],[4,63,7])).
% 58.73/58.80 cnf(76,plain,
% 58.73/58.80 (P1(x761,f6(f5(a4),x761))),
% 58.73/58.80 inference(scs_inference,[],[4,3,63,69,7,8])).
% 58.73/58.80 cnf(79,plain,
% 58.73/58.80 (P2(f5(x791),f6(x791,x792),x792)),
% 58.73/58.80 inference(scs_inference,[],[4,3,63,5,69,7,8,10])).
% 58.73/58.80 cnf(83,plain,
% 58.73/58.80 (P1(f6(f5(x831),f6(x831,x832)),x832)),
% 58.73/58.80 inference(scs_inference,[],[5,79,8])).
% 58.73/58.80 cnf(86,plain,
% 58.73/58.80 (P2(a4,f6(a4,x861),x861)),
% 58.73/58.80 inference(scs_inference,[],[4,3,5,79,8,9])).
% 58.73/58.80 cnf(88,plain,
% 58.73/58.80 (P2(f5(x881),x881,a4)),
% 58.73/58.80 inference(rename_variables,[],[4])).
% 58.73/58.80 cnf(89,plain,
% 58.73/58.80 (P2(a4,x891,x891)),
% 58.73/58.80 inference(rename_variables,[],[3])).
% 58.73/58.80 cnf(91,plain,
% 58.73/58.80 (P2(f5(f5(x911)),f6(a4,a4),x911)),
% 58.73/58.81 inference(scs_inference,[],[4,88,3,89,5,60,79,8,9,10])).
% 58.73/58.81 cnf(95,plain,
% 58.73/58.81 (P2(a4,f6(f5(a4),f6(a4,x951)),x951)),
% 58.73/58.81 inference(scs_inference,[],[4,88,3,89,5,60,79,8,9,10,7])).
% 58.73/58.81 cnf(99,plain,
% 58.73/58.81 (P2(a4,f6(f5(x991),f6(x991,x992)),x992)),
% 58.73/58.81 inference(scs_inference,[],[3,83,7])).
% 58.73/58.81 cnf(100,plain,
% 58.73/58.81 (P2(a4,x1001,x1001)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(103,plain,
% 58.73/58.81 (P2(a4,x1031,x1031)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(105,plain,
% 58.73/58.81 (P2(f5(a4),x1051,f6(f5(a4),f6(a4,x1051)))),
% 58.73/58.81 inference(scs_inference,[],[4,3,100,103,83,95,86,7,8,10])).
% 58.73/58.81 cnf(110,plain,
% 58.73/58.81 (P2(f5(a4),x1101,f6(f5(a4),f6(a4,x1101)))),
% 58.73/58.81 inference(rename_variables,[],[105])).
% 58.73/58.81 cnf(111,plain,
% 58.73/58.81 (P2(f5(x1111),x1111,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(115,plain,
% 58.73/58.81 (P2(f5(x1151),x1151,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(117,plain,
% 58.73/58.81 (P2(f5(a4),x1171,f6(f5(x1172),f6(x1172,x1171)))),
% 58.73/58.81 inference(scs_inference,[],[4,111,115,3,99,105,110,8,9,10])).
% 58.73/58.81 cnf(125,plain,
% 58.73/58.81 (P2(f5(a4),x1251,f6(f5(x1252),f6(x1252,x1251)))),
% 58.73/58.81 inference(rename_variables,[],[117])).
% 58.73/58.81 cnf(126,plain,
% 58.73/58.81 (P2(f5(x1261),x1261,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(128,plain,
% 58.73/58.81 (P2(a4,x1281,f6(f5(x1282),f6(x1282,x1281)))),
% 58.73/58.81 inference(scs_inference,[],[4,126,3,117,125,8,9])).
% 58.73/58.81 cnf(130,plain,
% 58.73/58.81 (P2(f5(x1301),x1301,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(132,plain,
% 58.73/58.81 (P2(f5(f5(a4)),x1321,x1321)),
% 58.73/58.81 inference(scs_inference,[],[4,126,130,3,66,117,125,8,9,10])).
% 58.73/58.81 cnf(139,plain,
% 58.73/58.81 (P1(a4,f5(a4))),
% 58.73/58.81 inference(scs_inference,[],[4,132,8])).
% 58.73/58.81 cnf(141,plain,
% 58.73/58.81 (P2(f5(x1411),x1411,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(143,plain,
% 58.73/58.81 (P2(f5(a4),f6(f5(x1431),f6(x1431,x1432)),x1432)),
% 58.73/58.81 inference(scs_inference,[],[4,141,3,132,128,8,10])).
% 58.73/58.81 cnf(145,plain,
% 58.73/58.81 (P2(f5(x1451),x1451,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(147,plain,
% 58.73/58.81 (P2(f5(x1471),x1471,f5(a4))),
% 58.73/58.81 inference(scs_inference,[],[4,141,145,3,132,128,8,10,7])).
% 58.73/58.81 cnf(149,plain,
% 58.73/58.81 (P2(a4,a4,f5(a4))),
% 58.73/58.81 inference(scs_inference,[],[4,141,145,3,132,128,8,10,7,9])).
% 58.73/58.81 cnf(154,plain,
% 58.73/58.81 (P1(x1541,f6(f5(x1542),f6(x1542,x1541)))),
% 58.73/58.81 inference(scs_inference,[],[3,128,8])).
% 58.73/58.81 cnf(157,plain,
% 58.73/58.81 (P2(f5(f5(x1571)),f5(a4),x1571)),
% 58.73/58.81 inference(scs_inference,[],[4,3,147,128,8,10])).
% 58.73/58.81 cnf(166,plain,
% 58.73/58.81 (P2(f5(a4),f6(f5(a4),x1661),x1661)),
% 58.73/58.81 inference(scs_inference,[],[4,3,69,10])).
% 58.73/58.81 cnf(172,plain,
% 58.73/58.81 (P2(f5(x1721),x1721,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(173,plain,
% 58.73/58.81 (P2(a4,x1731,x1731)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(175,plain,
% 58.73/58.81 (P2(f5(a4),x1751,f6(a4,x1751))),
% 58.73/58.81 inference(scs_inference,[],[4,172,3,173,166,86,9,10])).
% 58.73/58.81 cnf(187,plain,
% 58.73/58.81 (P2(f5(f5(x1871)),x1872,f6(x1871,x1872))),
% 58.73/58.81 inference(scs_inference,[],[4,3,79,10])).
% 58.73/58.81 cnf(188,plain,
% 58.73/58.81 (P2(f5(x1881),x1881,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(192,plain,
% 58.73/58.81 (P2(f5(x1921),x1921,a4)),
% 58.73/58.81 inference(rename_variables,[],[4])).
% 58.73/58.81 cnf(194,plain,
% 58.73/58.81 (P2(f5(x1941),x1941,f6(x1942,f5(x1942)))),
% 58.73/58.81 inference(scs_inference,[],[4,188,192,3,79,10,8,7])).
% 58.73/58.81 cnf(201,plain,
% 58.73/58.81 (P2(x2011,x2012,f6(a4,f6(x2011,x2012)))),
% 58.73/58.81 inference(scs_inference,[],[5,28,7])).
% 58.73/58.81 cnf(204,plain,
% 58.73/58.81 (P1(f6(f5(x2041),x2041),f6(a4,a4))),
% 58.73/58.81 inference(scs_inference,[],[5,28,60,7,8])).
% 58.73/58.81 cnf(206,plain,
% 58.73/58.81 (P2(x2061,x2062,f6(x2061,x2062))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(208,plain,
% 58.73/58.81 (P2(f6(x2081,a4),a4,f6(x2081,a4))),
% 58.73/58.81 inference(scs_inference,[],[5,206,3,28,60,7,8,9])).
% 58.73/58.81 cnf(219,plain,
% 58.73/58.81 (P2(x2191,x2192,f6(f5(a4),f6(x2191,x2192)))),
% 58.73/58.81 inference(scs_inference,[],[5,76,7])).
% 58.73/58.81 cnf(249,plain,
% 58.73/58.81 (P1(a2,f6(a2,x2491))+~P2(a1,x2491,a1)),
% 58.73/58.81 inference(scs_inference,[],[5,36,8])).
% 58.73/58.81 cnf(252,plain,
% 58.73/58.81 (P2(x2521,x2522,f6(x2521,x2522))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(256,plain,
% 58.73/58.81 (P2(x2561,x2562,f6(x2561,x2562))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(257,plain,
% 58.73/58.81 (P2(x2571,x2572,f6(x2571,x2572))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(259,plain,
% 58.73/58.81 (P2(x2591,x2592,f6(f6(x2591,a4),x2592))),
% 58.73/58.81 inference(scs_inference,[],[5,252,257,256,3,166,69,8,9,10])).
% 58.73/58.81 cnf(265,plain,
% 58.73/58.81 (P1(f6(x2651,x2652),f6(f6(x2651,a4),x2652))),
% 58.73/58.81 inference(scs_inference,[],[5,259,8])).
% 58.73/58.81 cnf(266,plain,
% 58.73/58.81 (P2(x2661,x2662,f6(f6(x2661,a4),x2662))),
% 58.73/58.81 inference(rename_variables,[],[259])).
% 58.73/58.81 cnf(270,plain,
% 58.73/58.81 (P2(x2701,x2702,f6(x2701,x2702))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(271,plain,
% 58.73/58.81 (P2(x2711,x2712,f6(x2711,x2712))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(273,plain,
% 58.73/58.81 (P2(x2731,a2,f6(f6(x2731,a4),a1))),
% 58.73/58.81 inference(scs_inference,[],[5,271,270,13,259,266,8,9,10])).
% 58.73/58.81 cnf(330,plain,
% 58.73/58.81 (P1(f6(a2,x3301),a2)+~P2(a1,x3301,a1)),
% 58.73/58.81 inference(scs_inference,[],[5,36,8])).
% 58.73/58.81 cnf(339,plain,
% 58.73/58.81 (P2(a4,x3391,x3391)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(341,plain,
% 58.73/58.81 (P1(x3411,f6(a4,f6(a4,x3411)))),
% 58.73/58.81 inference(scs_inference,[],[3,339,204,201,7,8])).
% 58.73/58.81 cnf(349,plain,
% 58.73/58.81 (P2(a4,x3491,x3491)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(351,plain,
% 58.73/58.81 (P1(x3511,f6(f6(a4,a4),x3511))),
% 58.73/58.81 inference(scs_inference,[],[3,349,265,259,7,8])).
% 58.73/58.81 cnf(371,plain,
% 58.73/58.81 (P1(a3,f6(a3,x3711))+~P2(a2,x3711,a2)),
% 58.73/58.81 inference(scs_inference,[],[5,45,8])).
% 58.73/58.81 cnf(403,plain,
% 58.73/58.81 (P1(f6(a3,x4031),a3)+~P2(a2,x4031,a2)),
% 58.73/58.81 inference(scs_inference,[],[5,45,8])).
% 58.73/58.81 cnf(416,plain,
% 58.73/58.81 (P2(a4,a1,f6(a4,a2))),
% 58.73/58.81 inference(scs_inference,[],[13,28,7])).
% 58.73/58.81 cnf(419,plain,
% 58.73/58.81 (P1(a2,a1)),
% 58.73/58.81 inference(scs_inference,[],[13,3,28,7,8])).
% 58.73/58.81 cnf(420,plain,
% 58.73/58.81 (P2(a4,x4201,x4201)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(422,plain,
% 58.73/58.81 (P2(a2,x4221,f6(a1,x4221))),
% 58.73/58.81 inference(scs_inference,[],[13,3,420,28,5,7,8,9])).
% 58.73/58.81 cnf(434,plain,
% 58.73/58.81 (P1(a2,f6(a4,a1))),
% 58.73/58.81 inference(scs_inference,[],[13,154,5,7,8])).
% 58.73/58.81 cnf(435,plain,
% 58.73/58.81 (P2(x4351,x4352,f6(x4351,x4352))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(437,plain,
% 58.73/58.81 (P2(f6(a2,a4),a1,f6(a1,a2))),
% 58.73/58.81 inference(scs_inference,[],[13,154,5,435,422,7,8,9])).
% 58.73/58.81 cnf(452,plain,
% 58.73/58.81 (P2(a2,x4521,f6(f6(a4,a4),f6(a1,x4521)))),
% 58.73/58.81 inference(scs_inference,[],[13,351,5,219,259,7,8,9])).
% 58.73/58.81 cnf(480,plain,
% 58.73/58.81 (P1(f6(a2,x4801),f6(f6(a4,a4),f6(a1,x4801)))),
% 58.73/58.81 inference(scs_inference,[],[13,76,5,452,7,8])).
% 58.73/58.81 cnf(482,plain,
% 58.73/58.81 (P2(x4821,x4822,f6(x4821,x4822))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(484,plain,
% 58.73/58.81 (P2(a2,x4841,f6(f5(a4),f6(a1,x4841)))),
% 58.73/58.81 inference(scs_inference,[],[13,76,5,482,452,69,7,8,9])).
% 58.73/58.81 cnf(497,plain,
% 58.73/58.81 (P1(f6(a2,x4971),f6(f5(a4),f6(a1,x4971)))),
% 58.73/58.81 inference(scs_inference,[],[3,480,5,484,7,8])).
% 58.73/58.81 cnf(513,plain,
% 58.73/58.81 (P1(f6(a2,x5131),f6(a1,x5131))),
% 58.73/58.81 inference(scs_inference,[],[3,497,5,422,7,8])).
% 58.73/58.81 cnf(515,plain,
% 58.73/58.81 (P2(x5151,x5152,f6(x5151,x5152))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(521,plain,
% 58.73/58.81 (P2(f6(a4,a2),x5211,f6(a4,a2))+~P2(a1,x5211,a1)),
% 58.73/58.81 inference(scs_inference,[],[13,3,497,5,515,416,422,273,7,8,10,9])).
% 58.73/58.81 cnf(523,plain,
% 58.73/58.81 (P1(f6(a4,a2),f6(f6(a4,a2),x5231))+~P2(a1,x5231,a1)),
% 58.73/58.81 inference(scs_inference,[],[5,521,8])).
% 58.73/58.81 cnf(527,plain,
% 58.73/58.81 (P1(a2,f6(f5(x5271),f6(x5271,a1)))),
% 58.73/58.81 inference(scs_inference,[],[13,3,513,128,7,8])).
% 58.73/58.81 cnf(543,plain,
% 58.73/58.81 (P2(a4,a1,a3)),
% 58.73/58.81 inference(scs_inference,[],[13,2,7])).
% 58.73/58.81 cnf(552,plain,
% 58.73/58.81 (P2(a2,x5521,x5522)+~P2(a1,x5521,f6(f5(x5523),f6(x5523,x5522)))),
% 58.73/58.81 inference(scs_inference,[],[13,5,99,2,259,69,7,8,10,9])).
% 58.73/58.81 cnf(565,plain,
% 58.73/58.81 (P2(a3,x5651,a3)+~P2(a1,x5651,a1)),
% 58.73/58.81 inference(scs_inference,[],[13,3,543,128,10,9])).
% 58.73/58.81 cnf(567,plain,
% 58.73/58.81 (P1(f6(a3,x5671),a3)+~P2(a1,x5671,a1)),
% 58.73/58.81 inference(scs_inference,[],[13,3,5,543,128,10,9,8])).
% 58.73/58.81 cnf(581,plain,
% 58.73/58.81 (P2(f6(f5(a2),a4),a1,f5(a4))),
% 58.73/58.81 inference(scs_inference,[],[13,5,147,9])).
% 58.73/58.81 cnf(590,plain,
% 58.73/58.81 (P2(f6(f5(a2),a4),a1,f6(a4,a4))),
% 58.73/58.81 inference(scs_inference,[],[13,5,60,9])).
% 58.73/58.81 cnf(607,plain,
% 58.73/58.81 (P2(f6(f5(a4),a4),a1,f6(a4,a2))),
% 58.73/58.81 inference(scs_inference,[],[13,5,175,9])).
% 58.73/58.81 cnf(622,plain,
% 58.73/58.81 (P2(a2,x6221,f6(f6(a4,a4),a1))+~P2(a1,x6221,a2)),
% 58.73/58.81 inference(scs_inference,[],[13,273,9])).
% 58.73/58.81 cnf(627,plain,
% 58.73/58.81 (P2(x6271,x6272,f6(x6271,x6272))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(629,plain,
% 58.73/58.81 (P1(f6(a2,x6291),f6(f6(a4,a4),a1))+~P2(a1,x6291,a2)),
% 58.73/58.81 inference(scs_inference,[],[13,3,5,627,273,9,10,8])).
% 58.73/58.81 cnf(633,plain,
% 58.73/58.81 (P1(f5(a4),a4)),
% 58.73/58.81 inference(scs_inference,[],[147,4,8])).
% 58.73/58.81 cnf(647,plain,
% 58.73/58.81 (P2(f6(a4,f6(a2,a4)),a1,f6(a1,a2))),
% 58.73/58.81 inference(scs_inference,[],[13,147,201,74,422,8,9])).
% 58.73/58.81 cnf(692,plain,
% 58.73/58.81 (P2(a4,f6(a1,a2),f6(f6(a1,a2),x6921))+~P2(a1,x6921,a1)),
% 58.73/58.81 inference(scs_inference,[],[3,5,437,9,10])).
% 58.73/58.81 cnf(694,plain,
% 58.73/58.81 (P2(x6941,x6942,f6(x6941,x6942))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(696,plain,
% 58.73/58.81 (P1(f6(f6(a1,a2),x6961),f6(a1,a2))+~P2(a1,x6961,a1)),
% 58.73/58.81 inference(scs_inference,[],[3,5,694,437,9,10,8])).
% 58.73/58.81 cnf(710,plain,
% 58.73/58.81 (P2(x7101,x7102,f6(x7101,x7102))),
% 58.73/58.81 inference(rename_variables,[],[5])).
% 58.73/58.81 cnf(712,plain,
% 58.73/58.81 (P1(f6(f5(a4),x7121),f5(a4))+~P2(a1,x7121,a1)),
% 58.73/58.81 inference(scs_inference,[],[3,5,710,581,9,10,8])).
% 58.73/58.81 cnf(736,plain,
% 58.73/58.81 (P2(a4,x7361,x7361)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(744,plain,
% 58.73/58.81 (~P2(a2,x7441,a2)+P1(a2,f6(a2,x7441))),
% 58.73/58.81 inference(scs_inference,[],[16,3,736,419,86,7,10,9,249])).
% 58.73/58.81 cnf(750,plain,
% 58.73/58.81 (~P2(a2,x7501,a2)+P1(f6(f6(a1,a2),x7501),f6(a1,a2))),
% 58.73/58.81 inference(scs_inference,[],[16,3,736,419,86,7,10,9,249,330,523,696])).
% 58.73/58.81 cnf(752,plain,
% 58.73/58.81 (~P2(a2,x7521,a2)+P1(f6(f5(a4),x7521),f5(a4))),
% 58.73/58.81 inference(scs_inference,[],[16,3,736,419,86,7,10,9,249,330,523,696,712])).
% 58.73/58.81 cnf(776,plain,
% 58.73/58.81 (P2(a4,x7761,x7761)),
% 58.73/58.81 inference(rename_variables,[],[3])).
% 58.73/58.81 cnf(778,plain,
% 58.73/58.81 (P2(f6(f5(a2),a4),f6(a1,x7781),x7781)),
% 58.73/58.81 inference(scs_inference,[],[16,3,776,434,422,7,10])).
% 58.73/58.81 cnf(782,plain,
% 58.73/58.81 (P2(f6(a4,a1),x7821,f6(a4,a1))+~P2(a2,x7821,a2)),
% 58.73/58.81 inference(scs_inference,[],[16,3,776,434,422,7,10,9])).
% 58.73/58.81 cnf(793,plain,
% 58.73/58.81 (P2(a4,a2,f6(a4,a3))),
% 58.73/58.81 inference(scs_inference,[],[25,28,7])).
% 58.73/58.81 cnf(796,plain,
% 58.73/58.81 (P1(a3,a2)),
% 58.73/58.81 inference(scs_inference,[],[25,3,28,7,8])).
% 58.73/58.82 cnf(811,plain,
% 58.73/58.82 (P1(a3,f6(a4,f6(a4,a2)))),
% 58.73/58.82 inference(scs_inference,[],[25,154,201,7,8])).
% 58.73/58.82 cnf(812,plain,
% 58.73/58.82 (P2(x8121,x8122,f6(a4,f6(x8121,x8122)))),
% 58.73/58.82 inference(rename_variables,[],[201])).
% 58.73/58.82 cnf(814,plain,
% 58.73/58.82 (P2(a3,x8141,f6(a2,x8141))),
% 58.73/58.82 inference(scs_inference,[],[25,154,201,812,86,7,8,9])).
% 58.73/58.82 cnf(826,plain,
% 58.73/58.82 (P1(a3,f6(a4,a2))),
% 58.73/58.82 inference(scs_inference,[],[25,351,5,7,8])).
% 58.73/58.82 cnf(833,plain,
% 58.73/58.82 (P2(f6(a4,f6(a2,a4)),a2,f6(a1,a3))),
% 58.73/58.82 inference(scs_inference,[],[25,3,351,201,5,69,422,7,8,10,9])).
% 58.73/58.82 cnf(844,plain,
% 58.73/58.82 (P2(f6(a4,f6(a3,a4)),a2,f6(a2,a3))),
% 58.73/58.82 inference(scs_inference,[],[25,341,201,219,814,7,8,9])).
% 58.73/58.82 cnf(869,plain,
% 58.73/58.82 (P2(a3,x8691,x8692)+~P2(a2,x8691,f6(f5(x8693),f6(x8693,x8692)))),
% 58.73/58.82 inference(scs_inference,[],[25,99,128,8,9])).
% 58.73/58.82 cnf(875,plain,
% 58.73/58.82 (P2(a4,f6(f5(a4),x8751),f5(a4))+~P2(a2,x8751,a2)),
% 58.73/58.82 inference(scs_inference,[],[3,752,7])).
% 58.73/58.82 cnf(879,plain,
% 58.73/58.82 (P2(f6(a4,a3),x8791,f6(a4,a3))+~P2(a2,x8791,a2)),
% 58.73/58.82 inference(scs_inference,[],[25,793,273,8,9])).
% 58.73/58.82 cnf(950,plain,
% 58.73/58.82 (P2(x9501,x9502,f6(x9501,x9502))),
% 58.73/58.82 inference(rename_variables,[],[5])).
% 58.73/58.82 cnf(952,plain,
% 58.73/58.82 (P2(f6(a2,a4),a2,f6(a1,a3))),
% 58.73/58.82 inference(scs_inference,[],[25,5,950,422,273,10,9])).
% 58.73/58.82 cnf(956,plain,
% 58.73/58.82 (P1(f6(a4,a1),f6(f6(a4,a1),x9561))+~P2(a2,x9561,a2)),
% 58.73/58.82 inference(scs_inference,[],[5,782,8])).
% 58.73/58.82 cnf(980,plain,
% 58.73/58.82 (P2(f6(a4,a4),f6(f5(a4),x9801),f5(a4))+~P2(a2,x9801,a2)),
% 58.73/58.82 inference(scs_inference,[],[3,5,875,9])).
% 58.73/58.82 cnf(989,plain,
% 58.73/58.82 (P1(f6(a4,a3),f6(f6(a4,a3),x9891))+~P2(a2,x9891,a2)),
% 58.73/58.82 inference(scs_inference,[],[5,879,8])).
% 58.73/58.82 cnf(1049,plain,
% 58.73/58.82 (P2(a4,f6(a2,x10491),f6(f6(a4,a4),a1))+~P2(a1,x10491,a2)),
% 58.73/58.82 inference(scs_inference,[],[3,629,7])).
% 58.73/58.82 cnf(1050,plain,
% 58.73/58.82 (P2(a3,x10501,f6(f6(a4,a4),a1))+~P2(a2,x10501,a2)),
% 58.73/58.82 inference(scs_inference,[],[25,273,9])).
% 58.73/58.82 cnf(1054,plain,
% 58.73/58.82 (P2(f6(a1,a3),x10541,f6(a1,a3))+~P2(a2,x10541,a2)),
% 58.73/58.82 inference(scs_inference,[],[833,9])).
% 58.73/58.82 cnf(1057,plain,
% 58.73/58.82 (P2(f6(a2,a3),x10571,f6(a2,a3))+~P2(a2,x10571,a2)),
% 58.73/58.82 inference(scs_inference,[],[844,9])).
% 58.73/58.82 cnf(1084,plain,
% 58.73/58.82 (P2(a4,a3,a2)),
% 58.73/58.82 inference(scs_inference,[],[3,796,7])).
% 58.73/58.82 cnf(1095,plain,
% 58.73/58.82 (P2(a2,x10951,a2)+~P2(a3,x10951,a3)),
% 58.73/58.82 inference(scs_inference,[],[3,811,1084,7,9])).
% 58.73/58.82 cnf(1097,plain,
% 58.73/58.82 (~P2(a3,x10971,a3)+P1(a2,f6(a2,x10971))),
% 58.73/58.82 inference(scs_inference,[],[3,811,1084,7,9,744])).
% 58.73/58.82 cnf(1154,plain,
% 58.73/58.82 (P2(f6(a4,a2),x11541,f6(a4,a2))+~P2(a3,x11541,a3)),
% 58.73/58.82 inference(scs_inference,[],[3,826,7,9])).
% 58.73/58.82 cnf(1172,plain,
% 58.73/58.82 (P2(a4,f6(a4,a2),a1)),
% 58.73/58.82 inference(scs_inference,[],[42,3,607,10])).
% 58.73/58.82 cnf(1191,plain,
% 58.73/58.82 (~P2(f6(a4,a2),x11911,f6(a4,a2))+P2(a2,x11911,a2)),
% 58.73/58.82 inference(scs_inference,[],[1172,9,567,565,1095])).
% 58.73/58.82 cnf(1297,plain,
% 58.73/58.82 (P2(f5(x12971),x12971,f6(a4,f6(a4,a4)))),
% 58.73/58.82 inference(scs_inference,[],[60,28,7])).
% 58.73/58.82 cnf(1315,plain,
% 58.73/58.82 (P2(f5(x13151),x13151,f5(a4))),
% 58.73/58.82 inference(rename_variables,[],[147])).
% 58.73/58.82 cnf(1318,plain,
% 58.73/58.82 (P2(f5(x13181),x13181,f6(a4,a4))),
% 58.73/58.82 inference(rename_variables,[],[60])).
% 58.73/58.82 cnf(1320,plain,
% 58.73/58.82 (P2(f6(a4,a4),a4,f5(a4))),
% 58.73/58.82 inference(scs_inference,[],[60,1318,3,265,147,1315,149,7,8,10,9])).
% 58.73/58.82 cnf(1362,plain,
% 58.73/58.82 (~P2(f6(a4,a2),x13621,a2)+P2(a2,x13621,a2)),
% 58.73/58.82 inference(scs_inference,[],[28,1191,7])).
% 58.73/58.82 cnf(1368,plain,
% 58.73/58.82 (~P2(a1,x13681,a2)+P2(a2,x13681,a2)),
% 58.73/58.82 inference(scs_inference,[],[3,416,1362,9])).
% 58.73/58.82 cnf(1373,plain,
% 58.73/58.82 (~P2(a1,x13731,a2)+P2(a3,x13731,a3)),
% 58.73/58.82 inference(scs_inference,[],[1368,45])).
% 58.73/58.82 cnf(1378,plain,
% 58.73/58.82 (P1(a2,f6(a2,x13781))+~P2(a1,x13781,a2)),
% 58.73/58.82 inference(scs_inference,[],[1373,1097])).
% 58.73/58.82 cnf(1525,plain,
% 58.73/58.82 (P2(f5(a4),a2,a1)),
% 58.73/58.82 inference(scs_inference,[],[66,419,7])).
% 58.73/58.82 cnf(1842,plain,
% 58.73/58.82 (~P2(a2,x18421,f6(f5(x18422),f6(x18422,a2)))+P2(a2,x18421,f6(f6(a4,a4),a1))),
% 58.73/58.82 inference(scs_inference,[],[1525,143,9,629,1378,1049,622])).
% 58.73/58.82 cnf(2040,plain,
% 58.73/58.82 (P2(f5(x20401),f6(x20401,a4),f5(a4))),
% 58.73/58.82 inference(scs_inference,[],[79,139,7])).
% 58.73/58.82 cnf(2099,plain,
% 58.73/58.82 (P2(f5(x20991),f6(x20991,x20992),x20992)),
% 58.73/58.82 inference(rename_variables,[],[79])).
% 58.73/58.82 cnf(2101,plain,
% 58.73/58.82 (P2(f5(f5(a2)),f6(a4,a4),a1)),
% 58.73/58.82 inference(scs_inference,[],[79,2099,3,633,590,7,10])).
% 58.73/58.82 cnf(2202,plain,
% 58.73/58.82 (P1(a3,f6(a3,a4))),
% 58.73/58.82 inference(scs_inference,[],[79,3,28,952,208,2101,7,10,9,36,565,1054,782,1050,1057,1154,989,249,330,403,879,523,750,980,956,692,371])).
% 58.73/58.82 cnf(2510,plain,
% 58.73/58.82 (P2(f5(f5(a2)),x25101,f6(a1,x25101))),
% 58.73/58.82 inference(scs_inference,[],[79,3,778,10])).
% 58.73/58.82 cnf(2752,plain,
% 58.73/58.82 (P2(a4,x27521,x27521)),
% 58.73/58.82 inference(rename_variables,[],[3])).
% 58.73/58.82 cnf(2758,plain,
% 58.73/58.82 (P2(f5(a4),f6(x27581,a4),x27581)),
% 58.73/58.82 inference(scs_inference,[],[3,2752,2202,147,194,1297,2040,157,8,7,10,9])).
% 58.73/58.82 cnf(2836,plain,
% 58.73/58.82 (P1(f6(f5(a4),f6(x28361,a4)),x28361)),
% 58.73/58.82 inference(scs_inference,[],[5,2758,8])).
% 58.73/58.82 cnf(2857,plain,
% 58.73/58.82 (P2(a4,f6(f5(a4),f6(x28571,a4)),x28571)),
% 58.73/58.82 inference(scs_inference,[],[3,2836,4,2510,8,7])).
% 58.73/58.82 cnf(2870,plain,
% 58.73/58.82 (P2(a4,f6(a4,x28701),x28701)),
% 58.73/58.82 inference(rename_variables,[],[86])).
% 58.73/58.82 cnf(2873,plain,
% 58.73/58.82 (P2(a4,f6(a4,x28731),x28731)),
% 58.73/58.82 inference(rename_variables,[],[86])).
% 58.73/58.82 cnf(2876,plain,
% 58.73/58.82 (P2(x28761,a4,f6(a4,x28761))),
% 58.73/58.82 inference(scs_inference,[],[86,2870,2873,527,5,219,2857,647,7,10,9])).
% 58.73/58.82 cnf(2936,plain,
% 58.73/58.82 (P2(a4,f6(a4,a3),f6(a4,a2))),
% 58.73/58.82 inference(scs_inference,[],[86,826,7])).
% 58.73/58.82 cnf(3119,plain,
% 58.73/58.82 (P2(f5(f5(x31191)),x31192,f6(x31191,x31192))),
% 58.73/58.82 inference(rename_variables,[],[187])).
% 58.73/58.82 cnf(3122,plain,
% 58.73/58.82 (P2(f5(f5(x31221)),f6(a4,a4),x31221)),
% 58.73/58.82 inference(rename_variables,[],[91])).
% 58.73/58.82 cnf(3124,plain,
% 58.73/58.82 (P2(a4,f6(x31241,f6(a4,a4)),x31241)),
% 58.73/58.82 inference(scs_inference,[],[91,3122,3,139,187,3119,8,7,10])).
% 58.73/58.82 cnf(3145,plain,
% 58.73/58.82 (P1(f6(f6(a4,a4),a1),f6(a2,x31451))+~P2(a2,x31451,f6(f5(x31452),f6(x31452,a2)))),
% 58.73/58.82 inference(scs_inference,[],[5,1842,8])).
% 58.73/58.82 cnf(3260,plain,
% 58.73/58.82 (P2(a4,f6(f5(x32601),f6(x32601,x32602)),x32602)),
% 58.73/58.82 inference(rename_variables,[],[99])).
% 58.73/58.82 cnf(3262,plain,
% 58.73/58.82 (P2(x32621,a4,f6(f5(x32622),f6(x32622,x32621)))),
% 58.73/58.82 inference(scs_inference,[],[99,3260,796,219,2857,7,9])).
% 58.73/58.82 cnf(3268,plain,
% 58.73/58.82 (P2(x32681,a4,f6(f5(x32682),f6(x32682,x32681)))),
% 58.73/58.82 inference(rename_variables,[],[3262])).
% 58.73/58.82 cnf(3271,plain,
% 58.73/58.82 (P2(x32711,a4,f6(f5(x32712),f6(x32712,x32711)))),
% 58.73/58.82 inference(rename_variables,[],[3262])).
% 58.73/58.82 cnf(3273,plain,
% 58.73/58.82 (P2(a2,a4,a1)),
% 58.73/58.82 inference(scs_inference,[],[3262,3268,3271,3145,869,552])).
% 58.73/58.82 cnf(3330,plain,
% 58.73/58.82 (P2(x33301,f6(a4,a4),f6(f5(x33302),f6(x33302,x33301)))),
% 58.73/58.82 inference(scs_inference,[],[99,5,3124,9])).
% 58.73/58.82 cnf(3335,plain,
% 58.73/58.82 (P2(a3,f6(a4,a4),a2)),
% 58.73/58.82 inference(scs_inference,[],[3330,869])).
% 58.73/58.82 cnf(3642,plain,
% 58.73/58.82 (~P2(a2,a4,a3)),
% 58.73/58.82 inference(scs_inference,[],[6,3273,8])).
% 58.73/58.82 cnf(3644,plain,
% 58.73/58.82 (P2(a3,f5(a4),a1)),
% 58.73/58.82 inference(scs_inference,[],[6,3273,3335,1320,8,10])).
% 58.73/58.82 cnf(3653,plain,
% 58.73/58.82 (~P1(f6(a4,a2),a3)),
% 58.73/58.82 inference(scs_inference,[],[6,3642,3644,2876,8,7])).
% 58.73/58.82 cnf(3678,plain,
% 58.73/58.82 ($false),
% 58.73/58.82 inference(scs_inference,[],[3653,2936,86,8]),
% 58.73/58.82 ['proof']).
% 58.73/58.82 % SZS output end Proof
% 58.73/58.82 % Total time :58.150000s
%------------------------------------------------------------------------------