%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP001-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 : 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:23 EDT 2024
% Result : Unsatisfiable 3.74s 3.78s
% Output : CNFRefutation 3.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP001-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n026.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:40:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 3.74/3.78 %-------------------------------------------
% 3.74/3.78 % File :CSE---1.7
% 3.74/3.78 % Problem :theBenchmark
% 3.74/3.78 % Transform :cnf
% 3.74/3.78 % Format :tptp:raw
% 3.74/3.78 % Command :java -jar mcs_scs.jar %d %s
% 3.74/3.78
% 3.74/3.78 % Result :Theorem 3.200000s
% 3.74/3.78 % Output :CNFRefutation 3.200000s
% 3.74/3.78 %-------------------------------------------
% 3.74/3.78 %------------------------------------------------------------------------------
% 3.74/3.78 % File : GRP001-1 : TPTP v8.2.0. Released v1.0.0.
% 3.74/3.78 % Domain : Group Theory
% 3.74/3.78 % Problem : X^2 = identity => commutativity
% 3.74/3.78 % Version : [MOW76] axioms.
% 3.74/3.78 % English : If the square of every element is the identity, the system
% 3.74/3.78 % is commutative.
% 3.74/3.78
% 3.74/3.78 % Refs : [Rob63] Robinson (1963), Theorem Proving on the Computer
% 3.74/3.78 % : [Wos65] Wos (1965), Unpublished Note
% 3.74/3.78 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 3.74/3.78 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 3.74/3.78 % : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
% 3.74/3.78 % : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
% 3.74/3.78 % : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
% 3.74/3.78 % Source : [MOW76]
% 3.74/3.78 % Names : - [Rob63]
% 3.74/3.78 % : wos10 [WM76]
% 3.74/3.78 % : G1 [MOW76]
% 3.74/3.78 % : CADE-11 Competition 1 [Ove90]
% 3.74/3.78 % : THEOREM 1 [LM93]
% 3.74/3.78 % : xsquared.ver1.in [ANL]
% 3.74/3.78
% 3.74/3.78 % Status : Unsatisfiable
% 3.74/3.78 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.00 v2.0.0
% 3.74/3.78 % Syntax : Number of clauses : 11 ( 8 unt; 0 nHn; 5 RR)
% 3.74/3.78 % Number of literals : 19 ( 1 equ; 9 neg)
% 3.74/3.78 % Maximal clause size : 4 ( 1 avg)
% 3.74/3.78 % Maximal term depth : 2 ( 1 avg)
% 3.74/3.78 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 3.74/3.78 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 3.74/3.78 % Number of variables : 23 ( 0 sgn)
% 3.74/3.78 % SPC : CNF_UNS_RFO_SEQ_HRN
% 3.74/3.78
% 3.74/3.78 % Comments :
% 3.74/3.78 %------------------------------------------------------------------------------
% 3.74/3.78 %----Include group theory axioms
% 3.74/3.78 include('Axioms/GRP003-0.ax').
% 3.74/3.78 %------------------------------------------------------------------------------
% 3.74/3.78 cnf(square_element,hypothesis,
% 3.74/3.78 product(X,X,identity) ).
% 3.74/3.78
% 3.74/3.78 cnf(a_times_b_is_c,negated_conjecture,
% 3.74/3.78 product(a,b,c) ).
% 3.74/3.78
% 3.74/3.78 cnf(prove_b_times_a_is_c,negated_conjecture,
% 3.74/3.78 ~ product(b,a,c) ).
% 3.74/3.78
% 3.74/3.78 %------------------------------------------------------------------------------
% 3.74/3.78 %-------------------------------------------
% 3.74/3.78 % Proof found
% 3.74/3.78 % SZS status Theorem for theBenchmark
% 3.74/3.78 % SZS output start Proof
% 3.74/3.78 %ClaNum:20(EqnAxiom:9)
% 3.74/3.78 %VarNum:46(SingletonVarNum:23)
% 3.74/3.78 %MaxLitNum:4
% 3.74/3.78 %MaxfuncDepth:1
% 3.74/3.78 %SharedTerms:6
% 3.74/3.78 %goalClause: 10 17
% 3.74/3.78 %singleGoalClaCount:2
% 3.74/3.78 [10]P1(a1,a2,a3)
% 3.74/3.78 [17]~P1(a2,a1,a3)
% 3.74/3.78 [11]P1(x111,x111,a4)
% 3.74/3.78 [12]P1(x121,a4,x121)
% 3.74/3.79 [13]P1(a4,x131,x131)
% 3.74/3.79 [14]P1(x141,f5(x141),a4)
% 3.74/3.79 [15]P1(f5(x151),x151,a4)
% 3.74/3.79 [16]P1(x161,x162,f6(x161,x162))
% 3.74/3.79 [18]~P1(x183,x184,x181)+E(x181,x182)+~P1(x183,x184,x182)
% 3.74/3.79 [19]~P1(x196,x194,x191)+P1(x191,x192,x193)+~P1(x194,x192,x195)+~P1(x196,x195,x193)
% 3.74/3.79 [20]~P1(x201,x206,x204)+P1(x201,x202,x203)+~P1(x204,x205,x203)+~P1(x206,x205,x202)
% 3.74/3.79 %EqnAxiom
% 3.74/3.79 [1]E(x11,x11)
% 3.74/3.79 [2]E(x22,x21)+~E(x21,x22)
% 3.74/3.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 3.74/3.79 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 3.74/3.79 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53))
% 3.74/3.79 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62))
% 3.74/3.79 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 3.74/3.79 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 3.74/3.79 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 3.74/3.79
% 3.74/3.79 %-------------------------------------------
% 3.74/3.79 cnf(21,plain,
% 3.74/3.79 (E(a3,f6(a1,a2))),
% 3.74/3.79 inference(scs_inference,[],[10,16,18])).
% 3.74/3.79 cnf(24,plain,
% 3.74/3.79 (P1(f6(a1,a2),a3,a4)),
% 3.74/3.79 inference(scs_inference,[],[10,11,16,18,7])).
% 3.74/3.79 cnf(25,plain,
% 3.74/3.79 (P1(x251,x251,a4)),
% 3.74/3.79 inference(rename_variables,[],[11])).
% 3.74/3.79 cnf(26,plain,
% 3.74/3.79 (P1(a3,f6(a1,a2),a4)),
% 3.74/3.79 inference(scs_inference,[],[10,11,25,16,18,7,8])).
% 3.74/3.79 cnf(27,plain,
% 3.74/3.79 (P1(x271,x271,a4)),
% 3.74/3.79 inference(rename_variables,[],[11])).
% 3.74/3.79 cnf(28,plain,
% 3.74/3.79 (P1(a3,a4,f6(a1,a2))),
% 3.74/3.79 inference(scs_inference,[],[10,11,25,12,16,18,7,8,9])).
% 3.74/3.79 cnf(29,plain,
% 3.74/3.79 (P1(x291,a4,x291)),
% 3.74/3.79 inference(rename_variables,[],[12])).
% 3.74/3.79 cnf(30,plain,
% 3.74/3.79 (P1(a3,a2,a1)),
% 3.74/3.79 inference(scs_inference,[],[10,11,25,27,12,29,16,18,7,8,9,19])).
% 3.74/3.79 cnf(32,plain,
% 3.74/3.79 (P1(x321,x321,a4)),
% 3.74/3.79 inference(rename_variables,[],[11])).
% 3.74/3.79 cnf(34,plain,
% 3.74/3.79 (P1(a1,a3,a2)),
% 3.74/3.79 inference(scs_inference,[],[10,11,25,27,32,12,29,13,16,18,7,8,9,19,20])).
% 3.74/3.79 cnf(38,plain,
% 3.74/3.79 (E(f6(a1,a2),a3)),
% 3.74/3.79 inference(scs_inference,[],[10,11,25,27,32,12,29,13,16,18,7,8,9,19,20,2])).
% 3.74/3.79 cnf(39,plain,
% 3.74/3.79 (E(a4,f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[15,12,18])).
% 3.74/3.79 cnf(41,plain,
% 3.74/3.79 (P1(f5(x411),x411,a4)),
% 3.74/3.79 inference(rename_variables,[],[15])).
% 3.74/3.79 cnf(43,plain,
% 3.74/3.79 (P1(f6(a1,a2),a2,a1)),
% 3.74/3.79 inference(scs_inference,[],[21,30,15,12,18,7])).
% 3.74/3.79 cnf(44,plain,
% 3.74/3.79 (P1(f6(a1,a2),a3,f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[21,24,30,15,12,18,7,9])).
% 3.74/3.79 cnf(45,plain,
% 3.74/3.79 (P1(a1,f6(a1,a2),a2)),
% 3.74/3.79 inference(scs_inference,[],[21,24,30,34,15,12,18,7,9,8])).
% 3.74/3.79 cnf(46,plain,
% 3.74/3.79 (P1(a4,f5(f5(a4)),a4)),
% 3.74/3.79 inference(scs_inference,[],[21,24,30,34,14,15,41,11,12,18,7,9,8,19])).
% 3.74/3.79 cnf(47,plain,
% 3.74/3.79 (P1(f5(x471),x471,a4)),
% 3.74/3.79 inference(rename_variables,[],[15])).
% 3.74/3.79 cnf(51,plain,
% 3.74/3.79 (P1(f5(a1),a3,a2)),
% 3.74/3.79 inference(scs_inference,[],[10,21,24,30,34,14,15,41,47,11,12,13,18,7,9,8,19,20])).
% 3.74/3.79 cnf(55,plain,
% 3.74/3.79 (E(f5(a4),a4)),
% 3.74/3.79 inference(scs_inference,[],[10,21,24,30,34,14,15,41,47,11,12,13,18,7,9,8,19,20,2])).
% 3.74/3.79 cnf(56,plain,
% 3.74/3.79 (E(f6(x561,f5(x561)),a4)),
% 3.74/3.79 inference(scs_inference,[],[16,14,18])).
% 3.74/3.79 cnf(58,plain,
% 3.74/3.79 (P1(x581,x582,f6(x581,x582))),
% 3.74/3.79 inference(rename_variables,[],[16])).
% 3.74/3.79 cnf(60,plain,
% 3.74/3.79 (P1(a3,a3,f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[38,44,16,14,18,7])).
% 3.74/3.79 cnf(61,plain,
% 3.74/3.79 (P1(f5(a1),f6(a1,a2),a2)),
% 3.74/3.79 inference(scs_inference,[],[51,21,38,44,16,14,18,7,8])).
% 3.74/3.79 cnf(62,plain,
% 3.74/3.79 (P1(a4,f5(f5(a4)),f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[39,46,51,21,38,44,16,14,18,7,8,9])).
% 3.74/3.79 cnf(63,plain,
% 3.74/3.79 (P1(f6(a1,a2),f5(f5(a4)),f6(a1,a2))),
% 3.74/3.79 inference(scs_inference,[],[39,46,51,21,38,44,28,16,14,18,7,8,9,19])).
% 3.74/3.79 cnf(65,plain,
% 3.74/3.79 (P1(a1,a1,f6(a2,a2))),
% 3.74/3.79 inference(scs_inference,[],[43,39,46,51,21,38,44,45,28,16,58,14,18,7,8,9,19,20])).
% 3.74/3.79 cnf(69,plain,
% 3.74/3.79 (E(f5(a4),f6(x691,f5(x691)))),
% 3.74/3.79 inference(scs_inference,[],[43,39,46,51,21,38,55,44,45,28,16,58,14,18,7,8,9,19,20,2,3])).
% 3.74/3.79 cnf(71,plain,
% 3.74/3.79 (E(a4,f5(f5(a4)))),
% 3.74/3.79 inference(scs_inference,[],[46,69,13,2,18])).
% 3.74/3.79 cnf(74,plain,
% 3.74/3.79 (P1(a3,f5(f5(a4)),f6(a1,a2))),
% 3.74/3.79 inference(scs_inference,[],[63,46,69,38,13,2,18,7])).
% 3.74/3.79 cnf(75,plain,
% 3.74/3.79 (P1(f6(a1,a2),f5(f5(a4)),a3)),
% 3.74/3.79 inference(scs_inference,[],[63,46,69,38,13,2,18,7,9])).
% 3.74/3.79 cnf(76,plain,
% 3.74/3.79 (P1(a3,f6(a1,a2),f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[63,60,46,21,69,38,13,2,18,7,9,8])).
% 3.74/3.79 cnf(77,plain,
% 3.74/3.79 (P1(a2,f5(f5(a4)),a2)),
% 3.74/3.79 inference(scs_inference,[],[63,60,46,21,69,61,38,13,2,18,7,9,8,19])).
% 3.74/3.79 cnf(79,plain,
% 3.74/3.79 (P1(a1,a3,f6(f6(a2,a2),a2))),
% 3.74/3.79 inference(scs_inference,[],[10,63,60,65,46,21,69,61,38,13,16,2,18,7,9,8,19,20])).
% 3.74/3.79 cnf(82,plain,
% 3.74/3.79 (E(f5(f5(a4)),a4)),
% 3.74/3.79 inference(scs_inference,[],[71,2])).
% 3.74/3.79 cnf(83,plain,
% 3.74/3.79 (P1(a3,f5(f5(a4)),a3)),
% 3.74/3.79 inference(scs_inference,[],[71,75,38,2,7])).
% 3.74/3.79 cnf(84,plain,
% 3.74/3.79 (P1(f6(a1,a2),a3,f5(f5(a4)))),
% 3.74/3.79 inference(scs_inference,[],[71,24,75,38,2,7,9])).
% 3.74/3.79 cnf(86,plain,
% 3.74/3.79 (P1(a1,f5(f5(a4)),a1)),
% 3.74/3.79 inference(scs_inference,[],[79,71,77,43,24,21,75,38,2,7,9,8,19])).
% 3.74/3.79 cnf(88,plain,
% 3.74/3.79 (P1(a3,a1,f6(f5(a4),a2))),
% 3.74/3.79 inference(scs_inference,[],[79,71,77,43,24,21,75,76,38,16,2,7,9,8,19,20])).
% 3.74/3.79 cnf(92,plain,
% 3.74/3.79 (P1(f6(a1,a2),f6(a1,a2),f5(f5(a4)))),
% 3.74/3.79 inference(scs_inference,[],[88,21,84,7,8])).
% 3.74/3.79 cnf(93,plain,
% 3.74/3.79 (P1(f5(x931),x931,f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[88,39,21,84,15,7,8,9])).
% 3.74/3.79 cnf(94,plain,
% 3.74/3.79 (P1(f5(a4),f5(f5(a4)),f5(a4))),
% 3.74/3.79 inference(scs_inference,[],[83,88,39,60,21,84,15,7,8,9,19])).
% 3.74/3.79 cnf(96,plain,
% 3.74/3.79 (P1(f5(f5(a1)),a2,a3)),
% 3.74/3.80 inference(scs_inference,[],[83,88,39,51,60,21,84,15,13,7,8,9,19,20])).
% 3.74/3.80 cnf(100,plain,
% 3.74/3.80 (E(f6(a2,a2),a4)),
% 3.74/3.80 inference(scs_inference,[],[65,11,18])).
% 3.74/3.80 cnf(103,plain,
% 3.74/3.80 (P1(a3,f6(a1,a2),f5(f5(a4)))),
% 3.74/3.80 inference(scs_inference,[],[65,92,11,38,18,7])).
% 3.74/3.80 cnf(106,plain,
% 3.74/3.80 (P1(f6(a2,a2),f5(f5(a4)),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[86,96,65,21,82,92,62,11,38,18,7,8,9,19])).
% 3.74/3.80 cnf(112,plain,
% 3.74/3.80 (E(f6(x1121,f5(x1121)),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[86,96,56,65,21,82,92,62,11,38,16,18,7,8,9,19,20,2,3])).
% 3.74/3.80 cnf(114,plain,
% 3.74/3.80 (E(f6(a2,a2),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[100,39,112,2,3])).
% 3.74/3.80 cnf(115,plain,
% 3.74/3.80 (P1(a4,f5(f5(a4)),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[106,100,39,112,2,3,7])).
% 3.74/3.80 cnf(117,plain,
% 3.74/3.80 (P1(f6(a2,a2),f5(f5(a4)),a4)),
% 3.74/3.80 inference(scs_inference,[],[106,103,100,39,112,38,2,3,7,8,9])).
% 3.74/3.80 cnf(118,plain,
% 3.74/3.80 (P1(a3,f5(a2),a1)),
% 3.74/3.80 inference(scs_inference,[],[10,106,103,100,39,112,12,14,38,2,3,7,8,9,19])).
% 3.74/3.80 cnf(122,plain,
% 3.74/3.80 (P1(a3,f5(a4),f6(f5(a4),a3))),
% 3.74/3.80 inference(scs_inference,[],[10,106,103,100,39,60,112,12,14,38,16,2,3,7,8,9,19,20])).
% 3.74/3.80 cnf(125,plain,
% 3.74/3.80 (E(f5(a4),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[114,2])).
% 3.74/3.80 cnf(126,plain,
% 3.74/3.80 (E(f6(a2,a2),f5(f5(a4)))),
% 3.74/3.80 inference(scs_inference,[],[115,114,13,2,18])).
% 3.74/3.80 cnf(127,plain,
% 3.74/3.80 (P1(a4,x1271,x1271)),
% 3.74/3.80 inference(rename_variables,[],[13])).
% 3.74/3.80 cnf(129,plain,
% 3.74/3.80 (P1(f6(a1,a2),f5(a4),f6(f5(a4),a3))),
% 3.74/3.80 inference(scs_inference,[],[122,115,21,114,13,2,18,7])).
% 3.74/3.80 cnf(130,plain,
% 3.74/3.80 (P1(a3,a4,f6(f5(a4),a3))),
% 3.74/3.80 inference(scs_inference,[],[122,115,21,114,55,13,2,18,7,8])).
% 3.74/3.80 cnf(131,plain,
% 3.74/3.80 (P1(x1311,x1311,f5(f5(a4)))),
% 3.74/3.80 inference(scs_inference,[],[122,115,71,21,114,55,11,13,2,18,7,8,9])).
% 3.74/3.80 cnf(132,plain,
% 3.74/3.80 (P1(f6(a2,a2),f5(a4),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[122,115,71,21,93,114,55,11,13,127,2,18,7,8,9,19])).
% 3.74/3.80 cnf(134,plain,
% 3.74/3.80 (P1(f5(x1341),x1341,f5(a4))),
% 3.74/3.80 inference(rename_variables,[],[93])).
% 3.74/3.80 cnf(136,plain,
% 3.74/3.80 (P1(f5(a4),f6(a2,a2),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[94,122,115,71,21,93,134,114,55,11,13,127,2,18,7,8,9,19,20])).
% 3.74/3.80 cnf(140,plain,
% 3.74/3.80 (E(f5(a4),f5(f5(a4)))),
% 3.74/3.80 inference(scs_inference,[],[126,60,131,2,18])).
% 3.74/3.80 cnf(143,plain,
% 3.74/3.80 (P1(f6(a2,a2),f6(a2,a2),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[136,126,60,131,125,2,18,7])).
% 3.74/3.80 cnf(145,plain,
% 3.74/3.80 (P1(f5(a4),f6(a2,a2),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[136,129,126,60,131,125,2,18,7,8,9])).
% 3.74/3.80 cnf(146,plain,
% 3.74/3.80 (P1(a3,f6(f5(a4),a3),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[136,129,126,103,60,131,125,93,2,18,7,8,9,20])).
% 3.74/3.80 cnf(153,plain,
% 3.74/3.80 (E(f6(f5(a4),a3),a3)),
% 3.74/3.80 inference(scs_inference,[],[140,130,12,2,18])).
% 3.74/3.80 cnf(156,plain,
% 3.74/3.80 (P1(f6(a1,a2),f5(a2),a1)),
% 3.74/3.80 inference(scs_inference,[],[118,140,21,130,12,2,18,7])).
% 3.74/3.80 cnf(159,plain,
% 3.74/3.80 (P1(f6(a2,a2),a4,f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[118,140,132,143,94,21,117,130,12,2,18,7,9,8,20])).
% 3.74/3.80 cnf(167,plain,
% 3.74/3.80 (E(f6(f5(x1671),x1671),f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[153,16,93,2,18])).
% 3.74/3.80 cnf(171,plain,
% 3.74/3.80 (E(f6(f5(a4),a3),f6(a1,a2))),
% 3.74/3.80 inference(scs_inference,[],[153,21,16,93,2,18,3])).
% 3.74/3.80 cnf(183,plain,
% 3.74/3.80 (P1(f5(x1831),x1831,a4)),
% 3.74/3.80 inference(rename_variables,[],[15])).
% 3.74/3.80 cnf(184,plain,
% 3.74/3.80 (P1(x1841,x1842,f6(x1841,x1842))),
% 3.74/3.80 inference(rename_variables,[],[16])).
% 3.74/3.80 cnf(194,plain,
% 3.74/3.80 (P1(f6(a1,a2),a1,f6(a4,a2))),
% 3.74/3.80 inference(scs_inference,[],[30,143,94,24,126,39,167,159,140,145,16,184,93,15,183,2,18,3,7,8,9,19,20])).
% 3.74/3.80 cnf(197,plain,
% 3.74/3.80 (E(f6(a1,a2),f6(f5(a4),a3))),
% 3.74/3.80 inference(scs_inference,[],[171,2])).
% 3.74/3.80 cnf(198,plain,
% 3.74/3.80 (P1(a3,a1,f6(a4,a2))),
% 3.74/3.80 inference(scs_inference,[],[194,171,38,2,7])).
% 3.74/3.80 cnf(201,plain,
% 3.74/3.80 (P1(f6(a4,a2),f5(f5(a4)),f6(a4,a2))),
% 3.74/3.80 inference(scs_inference,[],[86,39,194,122,153,28,171,38,2,7,8,9,19])).
% 3.74/3.80 cnf(206,plain,
% 3.74/3.80 (P1(f6(f5(a4),a3),a2,a1)),
% 3.74/3.80 inference(scs_inference,[],[43,197,7])).
% 3.74/3.80 cnf(208,plain,
% 3.74/3.80 (P1(f6(a1,a2),f5(a4),a3)),
% 3.74/3.80 inference(scs_inference,[],[43,129,153,26,197,7,8,9])).
% 3.74/3.80 cnf(215,plain,
% 3.74/3.80 (P1(f6(f5(a4),a3),a3,a4)),
% 3.74/3.80 inference(scs_inference,[],[24,197,7])).
% 3.74/3.80 cnf(228,plain,
% 3.74/3.80 (P1(f6(f5(a4),a3),f5(a2),a1)),
% 3.74/3.80 inference(scs_inference,[],[156,197,7])).
% 3.74/3.80 cnf(229,plain,
% 3.74/3.80 (P1(f6(f5(a4),a3),f6(a1,a2),a4)),
% 3.74/3.80 inference(scs_inference,[],[21,156,215,197,7,8])).
% 3.74/3.80 cnf(233,plain,
% 3.74/3.80 (P1(f5(f5(a4)),a4,f5(a4))),
% 3.74/3.80 inference(scs_inference,[],[126,159,7])).
% 3.74/3.80 cnf(234,plain,
% 3.74/3.80 (P1(f6(a1,a2),a4,a3)),
% 3.74/3.80 inference(scs_inference,[],[126,159,82,75,7,8])).
% 3.74/3.80 cnf(236,plain,
% 3.74/3.80 (P1(a3,a1,f6(f5(a4),f5(a2)))),
% 3.74/3.80 inference(scs_inference,[],[126,146,140,228,159,93,82,75,16,7,8,9,20])).
% 3.74/3.80 cnf(248,plain,
% 3.74/3.80 (P1(a2,f5(a4),a2)),
% 3.74/3.80 inference(scs_inference,[],[56,39,21,77,233,236,14,11,12,7,8,9,20])).
% 3.74/3.80 cnf(256,plain,
% 3.74/3.80 (P1(f5(f5(a4)),a4,a4)),
% 3.74/3.80 inference(scs_inference,[],[39,136,46,248,233,194,14,197,11,45,7,8,9,19,20])).
% 3.74/3.80 cnf(259,plain,
% 3.74/3.80 (P1(a4,f6(x2591,f5(x2591)),a4)),
% 3.74/3.80 inference(scs_inference,[],[56,11,7])).
% 3.74/3.80 cnf(262,plain,
% 3.74/3.80 (~E(f6(a2,a1),a3)),
% 3.74/3.80 inference(scs_inference,[],[17,56,197,11,61,16,7,8,9])).
% 3.74/3.80 cnf(264,plain,
% 3.74/3.80 (P1(f6(a2,a2),a4,a4)),
% 3.74/3.80 inference(scs_inference,[],[17,56,115,256,197,11,61,13,16,7,8,9,19])).
% 3.74/3.80 cnf(267,plain,
% 3.74/3.80 (P1(f5(a4),f6(a2,a2),a4)),
% 3.74/3.80 inference(scs_inference,[],[17,56,106,136,115,256,14,197,11,61,13,16,7,8,9,19,20])).
% 3.74/3.80 cnf(272,plain,
% 3.74/3.80 (P1(f5(f5(a4)),f6(a2,a2),a4)),
% 3.74/3.80 inference(scs_inference,[],[140,267,7])).
% 3.74/3.80 cnf(275,plain,
% 3.74/3.80 (P1(a3,f6(a2,a2),a3)),
% 3.74/3.80 inference(scs_inference,[],[39,140,136,267,259,264,208,7,8,9,19])).
% 3.74/3.80 cnf(277,plain,
% 3.74/3.80 (P1(f6(a2,a2),f6(a2,a2),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[39,140,136,115,267,259,264,208,7,8,9,19,20])).
% 3.74/3.80 cnf(279,plain,
% 3.74/3.80 (P1(f5(f5(a4)),f6(a2,a2),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[126,277,7])).
% 3.74/3.80 cnf(282,plain,
% 3.74/3.80 (P1(a4,f6(a2,a2),a4)),
% 3.74/3.80 inference(scs_inference,[],[126,39,21,46,277,272,275,12,13,7,8,9,19])).
% 3.74/3.80 cnf(285,plain,
% 3.74/3.80 (P1(a1,f6(a4,a2),f6(a2,a1))),
% 3.74/3.80 inference(scs_inference,[],[126,39,21,34,46,198,277,272,275,12,13,16,7,8,9,19,20])).
% 3.74/3.80 cnf(289,plain,
% 3.74/3.80 (P1(a4,a4,f6(x2891,f5(x2891)))),
% 3.74/3.80 inference(scs_inference,[],[56,39,259,13,7,8])).
% 3.74/3.80 cnf(294,plain,
% 3.74/3.80 (P1(a3,f6(a2,a2),f6(f6(a1,a2),f6(a2,a2)))),
% 3.74/3.80 inference(scs_inference,[],[56,39,74,201,279,285,259,13,16,229,7,8,9,19,20])).
% 3.74/3.80 cnf(342,plain,
% 3.74/3.80 (P1(f5(a4),x3421,x3421)),
% 3.74/3.80 inference(scs_inference,[],[39,13,7])).
% 3.74/3.80 cnf(350,plain,
% 3.74/3.80 (P1(a4,f5(a4),f6(x3501,f5(x3501)))),
% 3.74/3.80 inference(scs_inference,[],[39,289,8])).
% 3.74/3.80 cnf(352,plain,
% 3.74/3.80 (P1(a3,a1,a2)),
% 3.74/3.80 inference(scs_inference,[],[39,140,146,206,342,289,8,7,20])).
% 3.74/3.80 cnf(360,plain,
% 3.74/3.80 (P1(f6(a1,a2),a1,a2)),
% 3.74/3.80 inference(scs_inference,[],[21,352,7])).
% 3.74/3.80 cnf(361,plain,
% 3.74/3.80 (P1(a3,a1,f5(a2))),
% 3.74/3.80 inference(scs_inference,[],[21,146,228,352,342,7,20])).
% 3.74/3.80 cnf(372,plain,
% 3.74/3.80 (P1(f6(a1,a2),f6(a1,a2),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[24,74,115,360,197,7,20])).
% 3.74/3.80 cnf(382,plain,
% 3.74/3.80 (P1(f6(a1,a2),f6(f5(a4),a3),f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[21,361,372,197,7,8])).
% 3.74/3.80 cnf(393,plain,
% 3.74/3.80 (P1(f6(a1,a2),a3,f6(a2,a2))),
% 3.74/3.80 inference(scs_inference,[],[153,372,197,382,7,8])).
% 3.74/3.80 cnf(434,plain,
% 3.74/3.80 (P1(f6(f5(a4),a3),a4,f6(a1,a2))),
% 3.74/3.80 inference(scs_inference,[],[39,21,197,234,7,8,9])).
% 3.74/3.80 cnf(440,plain,
% 3.74/3.80 (P1(f6(a1,a2),f6(f6(a1,a2),f6(a2,a2)),a4)),
% 3.74/3.80 inference(scs_inference,[],[39,24,282,294,197,393,434,7,8,20])).
% 3.74/3.80 cnf(452,plain,
% 3.74/3.80 (P1(a1,a2,f6(a2,a1))),
% 3.74/3.80 inference(scs_inference,[],[39,34,352,440,16,350,7,9,20])).
% 3.74/3.80 cnf(893,plain,
% 3.74/3.80 ($false),
% 3.74/3.80 inference(scs_inference,[],[10,452,262,18]),
% 3.74/3.80 ['proof']).
% 3.74/3.80 % SZS output end Proof
% 3.74/3.80 % Total time :3.200000s
%------------------------------------------------------------------------------