%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN005-6 : 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 : n022.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 07:26:48 EDT 2024
% Result : Unsatisfiable 24.19s 24.25s
% Output : CNFRefutation 24.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : HEN005-6 : 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.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sat Jun 22 05:33:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 24.19/24.24 %-------------------------------------------
% 24.19/24.24 % File :CSE---1.7
% 24.19/24.24 % Problem :theBenchmark
% 24.19/24.24 % Transform :cnf
% 24.19/24.24 % Format :tptp:raw
% 24.19/24.24 % Command :java -jar mcs_scs.jar %d %s
% 24.19/24.24
% 24.19/24.24 % Result :Theorem 23.610000s
% 24.19/24.24 % Output :CNFRefutation 23.610000s
% 24.19/24.24 %-------------------------------------------
% 24.19/24.25 %--------------------------------------------------------------------------
% 24.19/24.25 % File : HEN005-6 : TPTP v8.2.0. Released v1.0.0.
% 24.19/24.25 % Domain : Henkin Models
% 24.19/24.25 % Problem : The relation less_equal is transitive
% 24.19/24.25 % Version : [MOW76] axioms : Augmented.
% 24.19/24.25 % English :
% 24.19/24.25
% 24.19/24.25 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 24.19/24.25 % Source : [ANL]
% 24.19/24.25 % Names : hp5.ver2.in [ANL]
% 24.19/24.25
% 24.19/24.25 % Status : Unsatisfiable
% 24.19/24.25 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.33 v5.2.0, 0.12 v5.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.40 v2.0.0
% 24.19/24.25 % Syntax : Number of clauses : 12 ( 9 unt; 0 nHn; 6 RR)
% 24.19/24.25 % Number of literals : 16 ( 5 equ; 5 neg)
% 24.19/24.25 % Maximal clause size : 3 ( 1 avg)
% 24.19/24.25 % Maximal term depth : 3 ( 1 avg)
% 24.19/24.25 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 24.19/24.25 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 24.19/24.25 % Number of variables : 15 ( 5 sgn)
% 24.19/24.25 % SPC : CNF_UNS_RFO_SEQ_HRN
% 24.19/24.25
% 24.19/24.25 % Comments :
% 24.19/24.25 %--------------------------------------------------------------------------
% 24.19/24.25 %----Include Henkin model axioms for equality formulation
% 24.19/24.25 include('Axioms/HEN002-0.ax').
% 24.19/24.25 %--------------------------------------------------------------------------
% 24.19/24.25 cnf(everything_divide_id_is_zero,axiom,
% 24.19/24.25 divide(X,identity) = zero ).
% 24.19/24.25
% 24.19/24.25 cnf(zero_divide_anything_is_zero,axiom,
% 24.19/24.25 divide(zero,X) = zero ).
% 24.19/24.25
% 24.19/24.25 cnf(a_LE_b,hypothesis,
% 24.19/24.25 less_equal(a,b) ).
% 24.19/24.25
% 24.19/24.25 cnf(b_LE_c,hypothesis,
% 24.19/24.25 less_equal(b,c) ).
% 24.19/24.25
% 24.19/24.25 cnf(prove_a_LE_c,negated_conjecture,
% 24.19/24.25 ~ less_equal(a,c) ).
% 24.19/24.25
% 24.19/24.25 %--------------------------------------------------------------------------
% 24.19/24.25 %-------------------------------------------
% 24.19/24.25 % Proof found
% 24.19/24.25 % SZS status Theorem for theBenchmark
% 24.19/24.25 % SZS output start Proof
% 24.19/24.26 %ClaNum:19(EqnAxiom:7)
% 24.19/24.26 %VarNum:28(SingletonVarNum:15)
% 24.19/24.26 %MaxLitNum:3
% 24.19/24.26 %MaxfuncDepth:2
% 24.19/24.26 %SharedTerms:8
% 24.19/24.26 %goalClause: 16
% 24.19/24.26 %singleGoalClaCount:1
% 24.19/24.26 [8]P1(a1,a2)
% 24.19/24.26 [9]P1(a2,a3)
% 24.19/24.26 [16]~P1(a1,a3)
% 24.19/24.26 [12]P1(x121,a4)
% 24.19/24.26 [13]P1(a6,x131)
% 24.19/24.26 [10]E(f5(x101,a4),a6)
% 24.19/24.26 [11]E(f5(a6,x111),a6)
% 24.19/24.26 [14]P1(f5(x141,x142),x141)
% 24.19/24.26 [15]P1(f5(f5(x151,x152),f5(x153,x152)),f5(f5(x151,x153),x152))
% 24.19/24.26 [17]~P1(x171,x172)+E(f5(x171,x172),a6)
% 24.19/24.26 [18]P1(x181,x182)+~E(f5(x181,x182),a6)
% 24.19/24.26 [19]~P1(x192,x191)+~P1(x191,x192)+E(x191,x192)
% 24.19/24.26 %EqnAxiom
% 24.19/24.26 [1]E(x11,x11)
% 24.19/24.26 [2]E(x22,x21)+~E(x21,x22)
% 24.19/24.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 24.19/24.26 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 24.19/24.26 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 24.19/24.26 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 24.19/24.26 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 24.19/24.26
% 24.19/24.26 %-------------------------------------------
% 24.19/24.27 cnf(20,plain,
% 24.19/24.27 (E(a6,f5(x201,a4))),
% 24.19/24.27 inference(scs_inference,[],[10,2])).
% 24.19/24.27 cnf(21,plain,
% 24.19/24.27 (~E(a6,a1)),
% 24.19/24.27 inference(scs_inference,[],[16,13,10,2,6])).
% 24.19/24.27 cnf(22,plain,
% 24.19/24.27 (P1(a6,x221)),
% 24.19/24.27 inference(rename_variables,[],[13])).
% 24.19/24.27 cnf(25,plain,
% 24.19/24.27 (~P1(a1,a6)),
% 24.19/24.27 inference(scs_inference,[],[16,12,13,22,10,2,6,7,19])).
% 24.19/24.27 cnf(28,plain,
% 24.19/24.27 (E(a6,f5(a6,x281))),
% 24.19/24.27 inference(scs_inference,[],[11,2])).
% 24.19/24.27 cnf(29,plain,
% 24.19/24.27 (E(f5(a6,x291),f5(x292,a4))),
% 24.19/24.27 inference(scs_inference,[],[20,11,2,3])).
% 24.19/24.27 cnf(30,plain,
% 24.19/24.27 (P1(f5(a6,x301),f5(x302,a4))),
% 24.19/24.27 inference(scs_inference,[],[14,20,11,2,3,7])).
% 24.19/24.27 cnf(31,plain,
% 24.19/24.27 (P1(f5(x311,x312),x311)),
% 24.19/24.27 inference(rename_variables,[],[14])).
% 24.19/24.27 cnf(32,plain,
% 24.19/24.27 (~E(f5(a3,x321),a1)),
% 24.19/24.27 inference(scs_inference,[],[16,14,31,20,11,2,3,7,6])).
% 24.19/24.27 cnf(34,plain,
% 24.19/24.27 (E(a1,a2)+~P1(a2,a1)),
% 24.19/24.27 inference(scs_inference,[],[16,14,31,20,8,11,2,3,7,6,19])).
% 24.19/24.27 cnf(36,plain,
% 24.19/24.27 (E(f5(x361,a4),f5(a6,x362))),
% 24.19/24.27 inference(scs_inference,[],[29,2])).
% 24.19/24.27 cnf(37,plain,
% 24.19/24.27 (E(f5(x371,a4),f5(x372,a4))),
% 24.19/24.27 inference(scs_inference,[],[10,29,20,2,3])).
% 24.19/24.27 cnf(38,plain,
% 24.19/24.27 (~E(a2,a1)),
% 24.19/24.27 inference(scs_inference,[],[16,10,29,9,20,2,3,6])).
% 24.19/24.27 cnf(39,plain,
% 24.19/24.27 (P1(f5(f5(x391,a4),f5(x392,a4)),a6)),
% 24.19/24.27 inference(scs_inference,[],[16,10,29,9,15,20,2,3,6,7])).
% 24.19/24.27 cnf(48,plain,
% 24.19/24.27 (P1(f5(f5(x481,a4),f5(x482,a4)),f5(a6,x483))),
% 24.19/24.27 inference(scs_inference,[],[39,11,28,13,19,3,7])).
% 24.19/24.27 cnf(50,plain,
% 24.19/24.27 (P1(f5(x501,a4),f5(x502,a4))),
% 24.19/24.27 inference(scs_inference,[],[39,11,25,28,13,19,3,7,6,18])).
% 24.19/24.27 cnf(52,plain,
% 24.19/24.27 (E(a6,f5(f5(x521,a4),f5(x522,a4)))),
% 24.19/24.27 inference(scs_inference,[],[39,11,25,28,13,19,3,7,6,18,2])).
% 24.19/24.27 cnf(53,plain,
% 24.19/24.27 (E(f5(a6,x531),f5(f5(x532,a4),f5(x533,a4)))),
% 24.19/24.27 inference(scs_inference,[],[11,52,3])).
% 24.19/24.27 cnf(54,plain,
% 24.19/24.27 (P1(f5(x541,a4),a6)),
% 24.19/24.27 inference(scs_inference,[],[50,11,52,3,7])).
% 24.19/24.27 cnf(60,plain,
% 24.19/24.27 (~E(f5(x601,a4),a1)),
% 24.19/24.27 inference(scs_inference,[],[50,48,11,52,25,3,7,2,19,6])).
% 24.19/24.27 cnf(61,plain,
% 24.19/24.27 (E(f5(f5(x611,a4),f5(x612,a4)),f5(a6,x613))),
% 24.19/24.27 inference(scs_inference,[],[53,2])).
% 24.19/24.27 cnf(66,plain,
% 24.19/24.27 (E(f5(x661,a4),f5(f5(x662,a4),f5(x663,a4)))),
% 24.19/24.27 inference(scs_inference,[],[60,14,53,36,2,19,3])).
% 24.19/24.27 cnf(68,plain,
% 24.19/24.27 (~E(f5(a6,x681),a1)),
% 24.19/24.27 inference(scs_inference,[],[30,60,14,53,36,2,19,3,6])).
% 24.19/24.27 cnf(71,plain,
% 24.19/24.27 (E(f5(f5(x711,a4),f5(x712,a4)),f5(x713,a4))),
% 24.19/24.27 inference(scs_inference,[],[66,2])).
% 24.19/24.27 cnf(76,plain,
% 24.19/24.27 (P1(x761,a2)+~E(a1,x761)),
% 24.19/24.27 inference(scs_inference,[],[54,61,66,8,52,2,3,7,6])).
% 24.19/24.27 cnf(82,plain,
% 24.19/24.27 (~P1(a3,a2)),
% 24.19/24.27 inference(scs_inference,[],[16,8,9,7,19])).
% 24.19/24.27 cnf(84,plain,
% 24.19/24.27 (~E(a1,a3)),
% 24.19/24.27 inference(scs_inference,[],[16,8,9,7,19,6])).
% 24.19/24.27 cnf(85,plain,
% 24.19/24.27 (P1(f5(f5(x851,a4),x852),a6)),
% 24.19/24.27 inference(scs_inference,[],[10,14,7])).
% 24.19/24.27 cnf(87,plain,
% 24.19/24.27 (E(f5(f5(x871,a4),x872),a6)),
% 24.19/24.27 inference(scs_inference,[],[10,13,14,7,19])).
% 24.19/24.27 cnf(90,plain,
% 24.19/24.27 (~E(f5(f5(x901,a4),x902),a1)),
% 24.19/24.27 inference(scs_inference,[],[10,13,14,25,7,19,6])).
% 24.19/24.27 cnf(91,plain,
% 24.19/24.27 (P1(f5(x911,a4),x912)),
% 24.19/24.27 inference(scs_inference,[],[10,13,14,25,7,19,6,18])).
% 24.19/24.27 cnf(93,plain,
% 24.19/24.27 (E(a6,f5(f5(x931,a4),x932))),
% 24.19/24.27 inference(scs_inference,[],[10,13,14,25,7,19,6,18,2])).
% 24.19/24.27 cnf(94,plain,
% 24.19/24.27 (E(f5(x941,a4),f5(f5(x941,a4),x942))),
% 24.19/24.27 inference(scs_inference,[],[10,13,14,25,7,19,6,18,2,3])).
% 24.19/24.27 cnf(100,plain,
% 24.19/24.27 (E(f5(f5(x1001,a4),f5(x1002,a4)),f5(f5(x1003,a4),x1004))),
% 24.19/24.27 inference(scs_inference,[],[91,90,94,71,2,19,3])).
% 24.19/24.27 cnf(103,plain,
% 24.19/24.27 (E(f5(f5(x1031,a4),x1032),f5(f5(x1033,a4),f5(x1034,a4)))),
% 24.19/24.27 inference(scs_inference,[],[100,2])).
% 24.19/24.27 cnf(108,plain,
% 24.19/24.27 (E(f5(x1081,a4),f5(f5(x1082,a4),x1083))),
% 24.19/24.27 inference(scs_inference,[],[91,32,10,100,93,2,19,3])).
% 24.19/24.27 cnf(109,plain,
% 24.19/24.27 (P1(a2,x1091)+~E(a3,x1091)),
% 24.19/24.27 inference(scs_inference,[],[91,32,9,10,100,93,2,19,3,7])).
% 24.19/24.27 cnf(111,plain,
% 24.19/24.27 (E(f5(f5(x1111,a4),x1112),f5(x1113,a4))),
% 24.19/24.27 inference(scs_inference,[],[108,2])).
% 24.19/24.27 cnf(116,plain,
% 24.19/24.27 (E(f5(f5(x1161,a4),x1162),f5(a6,x1163))),
% 24.19/24.27 inference(scs_inference,[],[91,68,103,108,61,2,19,3])).
% 24.19/24.27 cnf(118,plain,
% 24.19/24.27 (P1(f5(f5(a6,x1181),x1182),a6)),
% 24.19/24.27 inference(scs_inference,[],[91,68,11,14,103,108,61,2,19,3,7])).
% 24.19/24.27 cnf(120,plain,
% 24.19/24.27 (~E(f5(f5(a6,x1201),x1202),a1)),
% 24.19/24.27 inference(scs_inference,[],[91,68,11,14,103,108,61,25,2,19,3,7,6])).
% 24.19/24.27 cnf(121,plain,
% 24.19/24.27 (E(f5(a6,x1211),f5(f5(x1212,a4),x1213))),
% 24.19/24.27 inference(scs_inference,[],[116,2])).
% 24.19/24.27 cnf(126,plain,
% 24.19/24.27 (E(f5(f5(x1261,a4),x1262),f5(f5(x1263,a4),x1264))),
% 24.19/24.27 inference(scs_inference,[],[91,120,111,116,2,19,3])).
% 24.19/24.27 cnf(129,plain,
% 24.19/24.27 (E(f5(f5(a6,x1291),x1292),a6)),
% 24.19/24.27 inference(scs_inference,[],[118,13,19])).
% 24.19/24.27 cnf(132,plain,
% 24.19/24.27 (P1(f5(a6,x1321),x1322)),
% 24.19/24.27 inference(scs_inference,[],[118,13,19,18])).
% 24.19/24.27 cnf(134,plain,
% 24.19/24.27 (E(a6,f5(f5(a6,x1341),x1342))),
% 24.19/24.27 inference(scs_inference,[],[118,13,19,18,2])).
% 24.19/24.27 cnf(135,plain,
% 24.19/24.27 (E(f5(x1351,a4),f5(f5(a6,x1352),x1353))),
% 24.19/24.27 inference(scs_inference,[],[118,10,13,19,18,2,3])).
% 24.19/24.27 cnf(136,plain,
% 24.19/24.27 (E(f5(f5(a6,x1361),x1362),f5(x1363,a4))),
% 24.19/24.27 inference(scs_inference,[],[135,2])).
% 24.19/24.27 cnf(137,plain,
% 24.19/24.27 (E(f5(a6,x1371),f5(f5(a6,x1372),x1373))),
% 24.19/24.27 inference(scs_inference,[],[11,135,134,2,3])).
% 24.19/24.27 cnf(139,plain,
% 24.19/24.27 (~P1(a2,a1)),
% 24.19/24.27 inference(scs_inference,[],[38,34,2])).
% 24.19/24.27 cnf(141,plain,
% 24.19/24.27 (E(f5(f5(a6,x1411),x1412),f5(f5(x1413,a4),x1414))),
% 24.19/24.27 inference(scs_inference,[],[136,121,137,2,3])).
% 24.19/24.27 cnf(145,plain,
% 24.19/24.27 (E(f5(f5(x1451,a4),x1452),f5(f5(a6,x1453),x1454))),
% 24.19/24.27 inference(scs_inference,[],[141,2])).
% 24.19/24.27 cnf(149,plain,
% 24.19/24.27 (~E(a1,x1491)+E(f5(x1491,a2),a6)),
% 24.19/24.27 inference(scs_inference,[],[17,76])).
% 24.19/24.27 cnf(150,plain,
% 24.19/24.27 (E(f5(a1,a2),a6)),
% 24.19/24.27 inference(equality_inference,[],[149])).
% 24.19/24.27 cnf(151,plain,
% 24.19/24.27 (E(a6,f5(a1,a2))),
% 24.19/24.28 inference(scs_inference,[],[150,2])).
% 24.19/24.28 cnf(152,plain,
% 24.19/24.28 (E(f5(x1521,a4),f5(a1,a2))),
% 24.19/24.28 inference(scs_inference,[],[10,150,2,3])).
% 24.19/24.28 cnf(154,plain,
% 24.19/24.28 (E(f5(a1,a2),f5(x1541,a4))),
% 24.19/24.28 inference(scs_inference,[],[152,2])).
% 24.19/24.28 cnf(155,plain,
% 24.19/24.28 (P1(f5(f5(x1551,a4),x1552),f5(a1,a2))),
% 24.19/24.28 inference(scs_inference,[],[85,152,151,2,7])).
% 24.19/24.28 cnf(156,plain,
% 24.19/24.28 (E(f5(f5(x1561,a4),x1562),f5(a1,a2))),
% 24.19/24.28 inference(scs_inference,[],[85,126,152,151,2,7,3])).
% 24.19/24.28 cnf(159,plain,
% 24.19/24.28 (E(f5(x1591,a6),f5(x1591,f5(x1592,a4)))),
% 24.19/24.28 inference(scs_inference,[],[10,2,5])).
% 24.19/24.28 cnf(160,plain,
% 24.19/24.28 (E(f5(x1601,f5(x1602,a4)),f5(x1601,a6))),
% 24.19/24.28 inference(scs_inference,[],[159,2])).
% 24.19/24.28 cnf(162,plain,
% 24.19/24.28 (E(f5(a6,x1621),f5(a1,a2))),
% 24.19/24.28 inference(scs_inference,[],[155,11,159,154,151,2,7,3])).
% 24.19/24.28 cnf(163,plain,
% 24.19/24.28 (~E(a1,f5(x1631,a4))),
% 24.19/24.28 inference(scs_inference,[],[21,10,2,3])).
% 24.19/24.28 cnf(166,plain,
% 24.19/24.28 (~E(a1,f5(f5(x1661,a4),x1662))),
% 24.19/24.28 inference(scs_inference,[],[118,145,156,163,151,2,7,3])).
% 24.19/24.28 cnf(176,plain,
% 24.19/24.28 (E(f5(x1761,a6),f5(x1761,f5(a6,x1762)))),
% 24.19/24.28 inference(scs_inference,[],[11,2,5])).
% 24.19/24.28 cnf(177,plain,
% 24.19/24.28 (E(f5(x1771,f5(a6,x1772)),f5(x1771,a6))),
% 24.19/24.28 inference(scs_inference,[],[176,2])).
% 24.19/24.28 cnf(181,plain,
% 24.19/24.28 (~E(a1,a6)),
% 24.19/24.28 inference(scs_inference,[],[10,166,2,3])).
% 24.19/24.28 cnf(183,plain,
% 24.19/24.28 (~E(a1,f5(a6,x1831))),
% 24.19/24.28 inference(scs_inference,[],[11,181,162,2,3])).
% 24.19/24.28 cnf(184,plain,
% 24.19/24.28 (~E(x1841,a1)+~E(a3,x1841)),
% 24.19/24.28 inference(scs_inference,[],[84,2,3])).
% 24.19/24.28 cnf(185,plain,
% 24.19/24.28 (~E(x1851,a3)+~E(x1851,a1)),
% 24.19/24.28 inference(scs_inference,[],[184,2])).
% 24.19/24.28 cnf(186,plain,
% 24.19/24.28 (~E(a1,x1861)+~E(x1861,a3)),
% 24.19/24.28 inference(scs_inference,[],[185,2])).
% 24.19/24.28 cnf(187,plain,
% 24.19/24.28 (~E(a3,x1871)+~E(a1,x1871)),
% 24.19/24.28 inference(scs_inference,[],[186,2])).
% 24.19/24.28 cnf(188,plain,
% 24.19/24.28 (~P1(a4,a1)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[12,187,19])).
% 24.19/24.28 cnf(189,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(a4,a1),a6)),
% 24.19/24.28 inference(scs_inference,[],[188,18])).
% 24.19/24.28 cnf(190,plain,
% 24.19/24.28 (~E(a6,f5(a4,a1))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[189,2])).
% 24.19/24.28 cnf(191,plain,
% 24.19/24.28 (~P1(f5(a4,a1),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[13,190,19])).
% 24.19/24.28 cnf(192,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(f5(a4,a1),a6),a6)),
% 24.19/24.28 inference(scs_inference,[],[191,18])).
% 24.19/24.28 cnf(194,plain,
% 24.19/24.28 (~E(a6,f5(f5(a4,a1),a6))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[192,2])).
% 24.19/24.28 cnf(195,plain,
% 24.19/24.28 (~P1(f5(f5(a4,a1),a6),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[13,194,19])).
% 24.19/24.28 cnf(196,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(f5(f5(a4,a1),a6),a6),a6)),
% 24.19/24.28 inference(scs_inference,[],[195,18])).
% 24.19/24.28 cnf(197,plain,
% 24.19/24.28 (~E(a6,f5(f5(f5(a4,a1),a6),a6))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[196,2])).
% 24.19/24.28 cnf(198,plain,
% 24.19/24.28 (~E(a2,a6)),
% 24.19/24.28 inference(scs_inference,[],[25,8,7])).
% 24.19/24.28 cnf(199,plain,
% 24.19/24.28 (~E(a6,f5(f5(f5(a4,a1),a6),f5(x1991,a4)))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[160,197,3])).
% 24.19/24.28 cnf(200,plain,
% 24.19/24.28 (~E(a4,a6)),
% 24.19/24.28 inference(scs_inference,[],[25,12,7])).
% 24.19/24.28 cnf(203,plain,
% 24.19/24.28 (~E(f5(f5(f5(a4,a1),a6),f5(x2031,a4)),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[199,2])).
% 24.19/24.28 cnf(204,plain,
% 24.19/24.28 (~E(a4,f5(a6,x2041))),
% 24.19/24.28 inference(scs_inference,[],[11,200,3])).
% 24.19/24.28 cnf(205,plain,
% 24.19/24.28 (~P1(f5(f5(a4,a1),a6),f5(x2051,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[203,17])).
% 24.19/24.28 cnf(209,plain,
% 24.19/24.28 (~E(f5(a4,a1),f5(x2091,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[14,205,7])).
% 24.19/24.28 cnf(210,plain,
% 24.19/24.28 (~E(f5(x2101,a4),f5(a4,a1))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[209,2])).
% 24.19/24.28 cnf(212,plain,
% 24.19/24.28 (~P1(f5(a4,a1),f5(a6,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[132,210,19])).
% 24.19/24.28 cnf(214,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(f5(a4,a1),f5(a6,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[212,18])).
% 24.19/24.28 cnf(215,plain,
% 24.19/24.28 (~E(a6,f5(f5(a4,a1),f5(a6,a4)))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[214,2])).
% 24.19/24.28 cnf(216,plain,
% 24.19/24.28 (~P1(f5(f5(a4,a1),f5(a6,a4)),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[13,215,19])).
% 24.19/24.28 cnf(217,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(f5(f5(a4,a1),f5(a6,a4)),a6),a6)),
% 24.19/24.28 inference(scs_inference,[],[216,18])).
% 24.19/24.28 cnf(218,plain,
% 24.19/24.28 (~E(a6,f5(f5(f5(a4,a1),f5(a6,a4)),a6))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[217,2])).
% 24.19/24.28 cnf(219,plain,
% 24.19/24.28 (~E(a6,f5(f5(f5(a4,a1),f5(a6,a4)),f5(a6,x2191)))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[177,218,3])).
% 24.19/24.28 cnf(220,plain,
% 24.19/24.28 (~E(f5(f5(f5(a4,a1),f5(a6,a4)),f5(a6,x2201)),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[219,2])).
% 24.19/24.28 cnf(221,plain,
% 24.19/24.28 (~P1(f5(f5(a4,a1),f5(a6,a4)),f5(a6,x2211))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[220,17])).
% 24.19/24.28 cnf(225,plain,
% 24.19/24.28 (~E(f5(a6,x2251),f5(f5(a4,a1),f5(a6,a4)))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[132,221,6])).
% 24.19/24.28 cnf(226,plain,
% 24.19/24.28 (~E(f5(f5(a4,a1),f5(a6,a4)),f5(a6,x2261))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[225,2])).
% 24.19/24.28 cnf(230,plain,
% 24.19/24.28 (~E(f5(f5(a4,a1),f5(a6,a4)),f5(x2301,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[37,226,3])).
% 24.19/24.28 cnf(231,plain,
% 24.19/24.28 (~E(f5(a6,a4),a4)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[230,5])).
% 24.19/24.28 cnf(232,plain,
% 24.19/24.28 (~P1(a4,f5(a6,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[132,231,19])).
% 24.19/24.28 cnf(237,plain,
% 24.19/24.28 (~E(f5(a6,x2371),a4)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[132,232,6])).
% 24.19/24.28 cnf(243,plain,
% 24.19/24.28 (~E(a6,a4)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[10,237,3])).
% 24.19/24.28 cnf(249,plain,
% 24.19/24.28 (~P1(a4,a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[13,243,19])).
% 24.19/24.28 cnf(250,plain,
% 24.19/24.28 (~E(a6,a3)),
% 24.19/24.28 inference(scs_inference,[],[82,13,6])).
% 24.19/24.28 cnf(252,plain,
% 24.19/24.28 (~E(a3,a4)+~E(f5(a4,a6),a6)),
% 24.19/24.28 inference(scs_inference,[],[249,18])).
% 24.19/24.28 cnf(253,plain,
% 24.19/24.28 (~P1(a3,a6)),
% 24.19/24.28 inference(scs_inference,[],[250,13,19])).
% 24.19/24.28 cnf(256,plain,
% 24.19/24.28 (~E(a6,f5(a4,a6))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[252,2])).
% 24.19/24.28 cnf(258,plain,
% 24.19/24.28 (~E(a6,f5(a4,f5(x2581,a4)))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[160,256,3])).
% 24.19/24.28 cnf(259,plain,
% 24.19/24.28 (~E(f5(f5(a6,x2591),x2592),a3)),
% 24.19/24.28 inference(scs_inference,[],[118,253,6])).
% 24.19/24.28 cnf(260,plain,
% 24.19/24.28 (~E(f5(a4,f5(x2601,a4)),a6)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[258,2])).
% 24.19/24.28 cnf(261,plain,
% 24.19/24.28 (~P1(a4,f5(x2611,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[260,17])).
% 24.19/24.28 cnf(262,plain,
% 24.19/24.28 (~E(a4,f5(x2621,a4))+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[12,261,7])).
% 24.19/24.28 cnf(263,plain,
% 24.19/24.28 (~E(f5(x2631,a4),a4)+~E(a3,a4)),
% 24.19/24.28 inference(scs_inference,[],[262,2])).
% 24.19/24.28 cnf(264,plain,
% 24.19/24.28 (P1(f5(f5(x2641,x2642),f5(a4,x2642)),a6)),
% 24.19/24.28 inference(scs_inference,[],[87,15,7])).
% 24.19/24.28 cnf(266,plain,
% 24.19/24.28 (E(f5(f5(x2661,x2662),f5(a4,x2662)),a6)),
% 24.19/24.28 inference(scs_inference,[],[87,15,13,7,19])).
% 24.19/24.28 cnf(271,plain,
% 24.19/24.28 (P1(f5(x2711,x2712),f5(a4,x2712))),
% 24.19/24.28 inference(scs_inference,[],[87,15,13,181,253,7,19,6,3,18])).
% 24.19/24.28 cnf(273,plain,
% 24.19/24.28 (E(a6,f5(f5(x2731,x2732),f5(a4,x2732)))),
% 24.19/24.28 inference(scs_inference,[],[87,15,13,181,253,7,19,6,3,18,2])).
% 24.19/24.28 cnf(274,plain,
% 24.19/24.28 (~P1(a4,a3)+~E(f5(x2741,a4),a4)),
% 24.19/24.28 inference(scs_inference,[],[12,263,19])).
% 24.19/24.28 cnf(275,plain,
% 24.19/24.28 (~E(a2,f5(f5(x2751,a4),x2752))),
% 24.19/24.28 inference(scs_inference,[],[87,198,3])).
% 24.19/24.28 cnf(277,plain,
% 24.19/24.28 (~E(a4,f5(x2771,a4))+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[274,2])).
% 24.19/24.28 cnf(280,plain,
% 24.19/24.28 (~P1(a4,f5(x2801,a4))+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[91,277,19])).
% 24.19/24.28 cnf(281,plain,
% 24.19/24.28 (~E(a2,f5(f5(a6,x2811),x2812))),
% 24.19/24.28 inference(scs_inference,[],[275,136,3])).
% 24.19/24.28 cnf(284,plain,
% 24.19/24.28 (P1(f5(f5(x2841,x2842),f5(a4,x2842)),f5(f5(x2843,x2844),f5(a4,x2844)))),
% 24.19/24.28 inference(scs_inference,[],[264,275,136,273,3,7])).
% 24.19/24.28 cnf(285,plain,
% 24.19/24.28 (~P1(a4,a3)+~E(f5(a4,f5(x2851,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[280,18])).
% 24.19/24.28 cnf(294,plain,
% 24.19/24.28 (~E(a6,f5(a4,f5(x2941,a4)))+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[285,2])).
% 24.19/24.28 cnf(298,plain,
% 24.19/24.28 (P1(f5(f5(f5(x2981,a4),x2982),x2983),a6)),
% 24.19/24.28 inference(scs_inference,[],[87,14,29,281,3,7])).
% 24.19/24.28 cnf(304,plain,
% 24.19/24.28 (P1(f5(f5(x3041,a4),x3042),x3043)),
% 24.19/24.28 inference(scs_inference,[],[87,14,13,29,281,253,3,7,19,6,18])).
% 24.19/24.28 cnf(315,plain,
% 24.19/24.28 (~E(a6,f5(a4,a6))+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[159,294,3])).
% 24.19/24.28 cnf(320,plain,
% 24.19/24.28 (~E(f5(a4,a6),a6)+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[315,2])).
% 24.19/24.28 cnf(325,plain,
% 24.19/24.28 (~P1(a4,a6)+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[320,17])).
% 24.19/24.28 cnf(326,plain,
% 24.19/24.28 (~P1(a4,a6)+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[325,18])).
% 24.19/24.28 cnf(328,plain,
% 24.19/24.28 (~E(f5(a4,a3),a6)+~E(f5(a4,a6),a6)),
% 24.19/24.28 inference(scs_inference,[],[326,18])).
% 24.19/24.28 cnf(329,plain,
% 24.19/24.28 (~E(a6,f5(a4,a6))+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[328,2])).
% 24.19/24.28 cnf(330,plain,
% 24.19/24.28 (~E(a6,f5(a4,f5(a6,x3301)))+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[177,329,3])).
% 24.19/24.28 cnf(331,plain,
% 24.19/24.28 (P1(f5(f5(x3311,x3312),f5(a4,x3312)),f5(x3313,a4))),
% 24.19/24.28 inference(scs_inference,[],[111,284,7])).
% 24.19/24.28 cnf(338,plain,
% 24.19/24.28 (~E(f5(a4,f5(a6,x3381)),a6)+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[330,2])).
% 24.19/24.28 cnf(343,plain,
% 24.19/24.28 (~P1(a4,f5(a6,x3431))+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[338,17])).
% 24.19/24.28 cnf(344,plain,
% 24.19/24.28 (~E(f5(a6,x3441),a4)+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[132,343,6])).
% 24.19/24.28 cnf(345,plain,
% 24.19/24.28 (P1(f5(f5(x3451,x3452),f5(a4,x3452)),f5(a6,x3453))),
% 24.19/24.28 inference(scs_inference,[],[116,284,7])).
% 24.19/24.28 cnf(348,plain,
% 24.19/24.28 (~E(a6,a4)+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[11,344,3])).
% 24.19/24.28 cnf(356,plain,
% 24.19/24.28 (~P1(a4,a3)+~E(a6,a4)),
% 24.19/24.28 inference(scs_inference,[],[348,17])).
% 24.19/24.28 cnf(362,plain,
% 24.19/24.28 (~E(f5(f5(x3621,x3622),f5(a4,x3622)),a4)+~P1(a4,a3)),
% 24.19/24.28 inference(scs_inference,[],[273,356,3])).
% 24.19/24.28 cnf(364,plain,
% 24.19/24.28 (~E(f5(f5(x3641,x3642),f5(a4,x3642)),a4)+~E(f5(a4,a3),a6)),
% 24.19/24.28 inference(scs_inference,[],[362,18])).
% 24.19/24.28 cnf(370,plain,
% 24.19/24.28 (~E(a6,f5(a4,a3))+~E(f5(f5(x3701,x3702),f5(a4,x3702)),a4)),
% 24.19/24.28 inference(scs_inference,[],[364,2])).
% 24.19/24.28 cnf(371,plain,
% 24.19/24.28 (~E(a4,f5(f5(x3711,x3712),f5(a4,x3712)))+~E(a6,f5(a4,a3))),
% 24.19/24.28 inference(scs_inference,[],[370,2])).
% 24.19/24.28 cnf(372,plain,
% 24.19/24.28 (~P1(a4,f5(f5(x3721,a4),f5(a4,a4)))+~E(a6,f5(a4,a3))),
% 24.19/24.28 inference(scs_inference,[],[304,371,19])).
% 24.19/24.28 cnf(373,plain,
% 24.19/24.28 (~E(a6,f5(a4,a3))+~E(f5(a4,f5(f5(x3731,a4),f5(a4,a4))),a6)),
% 24.19/24.28 inference(scs_inference,[],[372,18])).
% 24.19/24.28 cnf(374,plain,
% 24.19/24.28 (~E(f5(a4,a3),a6)+~E(f5(a4,f5(f5(x3741,a4),f5(a4,a4))),a6)),
% 24.19/24.28 inference(scs_inference,[],[373,2])).
% 24.19/24.28 cnf(375,plain,
% 24.19/24.28 (~P1(a4,a3)+~E(f5(a4,f5(f5(x3751,a4),f5(a4,a4))),a6)),
% 24.19/24.28 inference(scs_inference,[],[374,17])).
% 24.19/24.28 cnf(376,plain,
% 24.19/24.28 (~E(f5(x3761,a4),a4)+~E(f5(a4,f5(f5(x3762,a4),f5(a4,a4))),a6)),
% 24.19/24.28 inference(scs_inference,[],[91,375,6])).
% 24.19/24.28 cnf(381,plain,
% 24.19/24.28 (P1(f5(f5(f5(a6,x3811),x3812),x3813),a6)),
% 24.19/24.28 inference(scs_inference,[],[129,132,345,14,19,7])).
% 24.19/24.28 cnf(385,plain,
% 24.19/24.28 (~P1(a4,f5(x3851,a4))+~E(f5(a4,f5(f5(x3852,a4),f5(a4,a4))),a6)),
% 24.19/24.28 inference(scs_inference,[],[91,376,19])).
% 24.19/24.28 cnf(386,plain,
% 24.19/24.28 (E(f5(f5(f5(a6,x3861),x3862),x3863),a6)),
% 24.19/24.28 inference(scs_inference,[],[381,13,19])).
% 24.19/24.28 cnf(390,plain,
% 24.19/24.28 (P1(f5(f5(a6,x3901),x3902),x3903)),
% 24.19/24.28 inference(scs_inference,[],[381,13,181,19,3,18])).
% 24.19/24.28 cnf(393,plain,
% 24.19/24.28 (~E(f5(a4,f5(f5(x3931,a4),f5(a4,a4))),a6)+~E(f5(a4,f5(x3932,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[385,18])).
% 24.19/24.28 cnf(399,plain,
% 24.19/24.28 (~P1(a4,f5(f5(x3991,a4),f5(a4,a4)))+~E(f5(a4,f5(x3992,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[393,17])).
% 24.19/24.28 cnf(405,plain,
% 24.19/24.28 (~E(f5(a6,x4051),a4)+~E(f5(a4,f5(x4052,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[132,399,6])).
% 24.19/24.28 cnf(406,plain,
% 24.19/24.28 (~P1(a3,f5(f5(a6,x4061),x4062))),
% 24.19/24.28 inference(scs_inference,[],[390,259,19])).
% 24.19/24.28 cnf(409,plain,
% 24.19/24.28 (~P1(a4,f5(a6,a4))+~E(f5(a4,f5(x4091,a4)),a6)),
% 24.19/24.28 inference(scs_inference,[],[91,405,19])).
% 24.19/24.28 cnf(410,plain,
% 24.19/24.28 (~P1(a4,f5(x4101,a4))+~P1(a4,f5(a6,a4))),
% 24.19/24.28 inference(scs_inference,[],[409,17])).
% 24.19/24.28 cnf(411,plain,
% 24.19/24.28 (~P1(a4,f5(a6,a4))),
% 24.19/24.28 inference(factoring_inference,[],[410])).
% 24.19/24.28 cnf(414,plain,
% 24.19/24.28 (~P1(a4,f5(f5(x4141,x4142),f5(a4,x4142)))),
% 24.19/24.28 inference(scs_inference,[],[331,12,411,6,19])).
% 24.19/24.28 cnf(427,plain,
% 24.19/24.28 (~E(f5(a6,x4271),a2)),
% 24.19/24.28 inference(scs_inference,[],[139,132,6])).
% 24.19/24.28 cnf(434,plain,
% 24.19/24.28 (~E(f5(x4341,a4),a2)),
% 24.19/24.28 inference(scs_inference,[],[139,91,132,427,19,6])).
% 24.19/24.28 cnf(436,plain,
% 24.19/24.28 (~E(a3,f5(x4361,a4))),
% 24.19/24.28 inference(scs_inference,[],[91,434,109,19])).
% 24.19/24.28 cnf(442,plain,
% 24.19/24.28 (~E(f5(a1,x4421),a2)),
% 24.19/24.28 inference(scs_inference,[],[139,14,6])).
% 24.19/24.28 cnf(444,plain,
% 24.19/24.28 (~E(a6,a2)),
% 24.19/24.28 inference(scs_inference,[],[139,13,6])).
% 24.19/24.28 cnf(446,plain,
% 24.19/24.28 (~P1(a2,a6)),
% 24.19/24.28 inference(scs_inference,[],[444,13,19])).
% 24.19/24.28 cnf(477,plain,
% 24.19/24.28 (P1(f5(f5(a1,a2),x4771),a6)),
% 24.19/24.28 inference(scs_inference,[],[150,14,7])).
% 24.19/24.28 cnf(479,plain,
% 24.19/24.28 (E(f5(f5(a1,a2),x4791),a6)),
% 24.19/24.28 inference(scs_inference,[],[150,14,13,7,19])).
% 24.19/24.28 cnf(482,plain,
% 24.19/24.28 (~E(f5(f5(a1,a2),x4821),a2)),
% 24.19/24.28 inference(scs_inference,[],[150,14,13,446,7,19,6])).
% 24.19/24.28 cnf(484,plain,
% 24.19/24.28 (P1(f5(a1,a2),x4841)),
% 24.19/24.28 inference(scs_inference,[],[150,14,13,446,181,7,19,6,3,18])).
% 24.19/24.28 cnf(489,plain,
% 24.19/24.28 (P1(f5(a1,a2),x4891)),
% 24.19/24.28 inference(rename_variables,[],[484])).
% 24.19/24.28 cnf(492,plain,
% 24.19/24.28 (~E(f5(a1,a2),a1)),
% 24.19/24.28 inference(scs_inference,[],[484,489,16,442,19,6])).
% 24.19/24.28 cnf(495,plain,
% 24.19/24.28 (P1(f5(f5(a1,a2),x4951),f5(f5(a6,x4952),x4953))),
% 24.19/24.28 inference(scs_inference,[],[484,489,16,477,442,266,134,200,19,6,3,7])).
% 24.19/24.28 cnf(504,plain,
% 24.19/24.28 (P1(f5(f5(a1,a2),x5041),f5(x5042,a4))),
% 24.19/24.28 inference(scs_inference,[],[484,495,492,477,20,386,414,198,19,6,3,7])).
% 24.19/24.28 cnf(509,plain,
% 24.19/24.28 (~E(f5(f5(a1,a2),x5091),a3)),
% 24.19/24.28 inference(scs_inference,[],[91,504,495,406,19,6])).
% 24.19/24.28 cnf(575,plain,
% 24.19/24.28 (P1(f5(f5(x5751,a6),x5752),f5(x5751,f5(x5753,a4)))),
% 24.19/24.28 inference(scs_inference,[],[159,14,7])).
% 24.19/24.28 cnf(577,plain,
% 24.19/24.28 (P1(f5(f5(x5771,a6),f5(x5772,a6)),f5(f5(x5771,x5772),f5(x5773,a4)))),
% 24.19/24.28 inference(scs_inference,[],[159,15,7])).
% 24.19/24.29 cnf(589,plain,
% 24.19/24.29 (P1(f5(f5(x5891,f5(x5892,a4)),x5893),f5(x5891,a6))),
% 24.19/24.29 inference(scs_inference,[],[160,14,7])).
% 24.19/24.29 cnf(654,plain,
% 24.19/24.29 (E(f5(f5(f5(x6541,x6542),f5(a4,x6542)),x6543),a6)),
% 24.19/24.29 inference(scs_inference,[],[266,14,13,7,19])).
% 24.19/24.29 cnf(796,plain,
% 24.19/24.29 (~E(a6,a4)),
% 24.19/24.29 inference(scs_inference,[],[414,13,6])).
% 24.19/24.29 cnf(799,plain,
% 24.19/24.29 (~P1(a4,a6)),
% 24.19/24.29 inference(scs_inference,[],[796,13,19])).
% 24.19/24.29 cnf(824,plain,
% 24.19/24.29 (~E(a3,a6)),
% 24.19/24.29 inference(scs_inference,[],[436,20,3])).
% 24.19/24.29 cnf(874,plain,
% 24.19/24.29 (P1(f5(f5(a1,a6),f5(a2,a6)),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,577,7])).
% 24.19/24.29 cnf(877,plain,
% 24.19/24.29 (E(f5(f5(a1,a6),f5(a2,a6)),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,577,13,7,19])).
% 24.19/24.29 cnf(882,plain,
% 24.19/24.29 (P1(f5(a1,a6),f5(a2,a6))),
% 24.19/24.29 inference(scs_inference,[],[479,577,13,799,824,7,19,6,3,18])).
% 24.19/24.29 cnf(887,plain,
% 24.19/24.29 (E(f5(x8871,a6),f5(x8871,f5(a6,x8872)))),
% 24.19/24.29 inference(rename_variables,[],[176])).
% 24.19/24.29 cnf(889,plain,
% 24.19/24.29 (P1(f5(a1,a6),f5(a2,f5(a6,x8891)))),
% 24.19/24.29 inference(scs_inference,[],[882,176,887,877,181,6,3,7])).
% 24.19/24.29 cnf(899,plain,
% 24.19/24.29 (P1(f5(f5(f5(a1,a2),a6),x8991),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,575,889,654,176,198,6,3,7])).
% 24.19/24.29 cnf(906,plain,
% 24.19/24.29 (E(f5(f5(f5(a1,a2),a6),x9061),a6)),
% 24.19/24.29 inference(scs_inference,[],[899,13,19])).
% 24.19/24.29 cnf(910,plain,
% 24.19/24.29 (E(f5(x9101,a6),f5(x9101,f5(x9102,a4)))),
% 24.19/24.29 inference(rename_variables,[],[159])).
% 24.19/24.29 cnf(912,plain,
% 24.19/24.29 (P1(f5(a1,a6),f5(a2,f5(x9121,a4)))),
% 24.19/24.29 inference(scs_inference,[],[882,899,13,159,910,824,19,6,3,7])).
% 24.19/24.29 cnf(914,plain,
% 24.19/24.29 (P1(f5(f5(a1,a2),a6),x9141)),
% 24.19/24.29 inference(scs_inference,[],[882,899,13,159,910,824,19,6,3,7,18])).
% 24.19/24.29 cnf(925,plain,
% 24.19/24.29 (P1(f5(f5(f5(a1,a2),f5(x9251,a4)),x9252),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,914,589,912,482,159,906,181,19,6,3,7])).
% 24.19/24.29 cnf(934,plain,
% 24.19/24.29 (P1(f5(f5(a1,a6),f5(a2,a6)),f5(a6,x9341))),
% 24.19/24.29 inference(scs_inference,[],[914,874,925,509,28,877,799,198,19,6,3,7])).
% 24.19/24.29 cnf(1001,plain,
% 24.19/24.29 (P1(f5(f5(f5(a1,a2),f5(x10011,a4)),x10012),f5(a6,x10013))),
% 24.19/24.29 inference(scs_inference,[],[132,934,925,28,19,7])).
% 24.19/24.29 cnf(1003,plain,
% 24.19/24.29 (E(f5(f5(f5(a1,a2),f5(x10031,a4)),x10032),f5(a6,x10033))),
% 24.19/24.29 inference(scs_inference,[],[132,1001,19])).
% 24.19/24.29 cnf(1008,plain,
% 24.19/24.29 (P1(f5(f5(f5(a1,a2),a6),x10081),f5(a1,a2))),
% 24.19/24.29 inference(scs_inference,[],[132,1001,899,151,183,19,3,7])).
% 24.19/24.29 cnf(1015,plain,
% 24.19/24.29 (P1(f5(f5(f5(a1,a2),x10151),x10152),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,484,1008,14,1003,204,19,3,7])).
% 24.19/24.29 cnf(1018,plain,
% 24.19/24.29 (~E(f5(f5(f5(a1,a2),x10181),x10182),a4)),
% 24.19/24.29 inference(scs_inference,[],[479,484,1008,14,1003,204,799,19,3,7,2,6])).
% 24.19/24.29 cnf(1023,plain,
% 24.19/24.29 (P1(f5(f5(a1,x10231),f5(a2,x10231)),a6)),
% 24.19/24.29 inference(scs_inference,[],[479,91,1018,15,19,7])).
% 24.19/24.29 cnf(1026,plain,
% 24.19/24.29 (E(f5(f5(f5(a1,a2),x10261),x10262),a6)),
% 24.19/24.29 inference(scs_inference,[],[1015,13,19])).
% 24.19/24.29 cnf(1031,plain,
% 24.19/24.29 (P1(f5(f5(a1,x10311),f5(a2,x10311)),f5(f5(x10312,x10313),f5(a4,x10313)))),
% 24.19/24.29 inference(scs_inference,[],[1015,1023,13,273,446,824,19,6,3,7])).
% 24.19/24.29 cnf(1032,plain,
% 24.19/24.29 (P1(f5(f5(a1,a2),x10321),x10322)),
% 24.19/24.29 inference(scs_inference,[],[1015,1023,13,273,446,824,19,6,3,7,18])).
% 24.19/24.29 cnf(1040,plain,
% 24.19/24.29 (~E(a1,f5(f5(f5(a1,a2),x10401),x10402))),
% 24.19/24.29 inference(scs_inference,[],[482,1032,1023,1026,25,181,19,6,3])).
% 24.19/24.29 cnf(1042,plain,
% 24.19/24.29 (E(f5(f5(a1,x10421),f5(a2,x10421)),f5(f5(x10422,a4),f5(a4,a4)))),
% 24.19/24.29 inference(scs_inference,[],[304,1031,19])).
% 24.19/24.29 cnf(1071,plain,
% 24.19/24.29 (P1(f5(a1,x10711),f5(a2,x10711))),
% 24.19/24.29 inference(scs_inference,[],[1015,1023,13,28,1040,1042,19,3,7,18])).
% 24.19/24.29 cnf(1273,plain,
% 24.19/24.29 (~P1(f5(a1,a3),a6)),
% 24.19/24.29 inference(scs_inference,[],[16,13,18,19])).
% 24.19/24.29 cnf(1274,plain,
% 24.19/24.29 (~E(f5(f5(a1,x12741),f5(a2,x12741)),f5(a1,a3))),
% 24.19/24.29 inference(scs_inference,[],[1023,1273,6])).
% 24.19/24.29 cnf(1275,plain,
% 24.19/24.29 (~E(f5(a4,a3),a6)),
% 24.19/24.29 inference(scs_inference,[],[271,1023,1273,6,7])).
% 24.19/24.29 cnf(1279,plain,
% 24.19/24.29 (~E(f5(a1,a3),f5(x12791,a4))),
% 24.19/24.29 inference(scs_inference,[],[16,10,18,3])).
% 24.19/24.29 cnf(1290,plain,
% 24.19/24.29 ($false),
% 24.19/24.29 inference(scs_inference,[],[304,1071,298,1274,9,11,1275,1279,1273,5,19,6,3,7,17]),
% 24.19/24.29 ['proof']).
% 24.19/24.29 % SZS output end Proof
% 24.19/24.29 % Total time :23.610000s
%------------------------------------------------------------------------------