%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG038-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n013.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 14:00:48 EDT 2024
% Result : Unsatisfiable 0.64s 0.78s
% Output : CNFRefutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.10 % Problem : RNG038-1 : TPTP v8.2.0. Released v1.0.0.
% 0.10/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n013.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Tue Jun 18 13:35:24 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.16/0.55 start to proof:theBenchmark
% 0.64/0.77 %-------------------------------------------
% 0.64/0.77 % File :CSE---1.7
% 0.64/0.77 % Problem :theBenchmark
% 0.64/0.77 % Transform :cnf
% 0.64/0.77 % Format :tptp:raw
% 0.64/0.77 % Command :java -jar mcs_scs.jar %d %s
% 0.64/0.77
% 0.64/0.77 % Result :Theorem 0.190000s
% 0.64/0.77 % Output :CNFRefutation 0.190000s
% 0.64/0.77 %-------------------------------------------
% 0.64/0.77 %--------------------------------------------------------------------------
% 0.64/0.78 % File : RNG038-1 : TPTP v8.2.0. Released v1.0.0.
% 0.64/0.78 % Domain : Ring Theory
% 0.64/0.78 % Problem : Ring property 1
% 0.64/0.78 % Version : [Wos65] axioms.
% 0.64/0.78 % English :
% 0.64/0.78
% 0.64/0.78 % Refs : [Wos65] Wos (1965), Unpublished Note
% 0.64/0.78 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 0.64/0.78 % Source : [SPRFN]
% 0.64/0.78 % Names : Problem 27 [Wos65]
% 0.64/0.78
% 0.64/0.78 % Status : Unsatisfiable
% 0.64/0.78 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.1.0, 0.00 v2.0.0
% 0.64/0.78 % Syntax : Number of clauses : 21 ( 9 unt; 0 nHn; 14 RR)
% 0.64/0.78 % Number of literals : 55 ( 5 equ; 36 neg)
% 0.64/0.78 % Maximal clause size : 5 ( 2 avg)
% 0.64/0.78 % Maximal term depth : 2 ( 1 avg)
% 0.64/0.78 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 0.64/0.78 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 0.64/0.78 % Number of variables : 73 ( 0 sgn)
% 0.64/0.78 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.64/0.78
% 0.64/0.78 % Comments : These are the same axioms as in [MOW76].
% 0.64/0.78 %--------------------------------------------------------------------------
% 0.64/0.78 %----Include ring theory axioms
% 0.64/0.78 include('Axioms/RNG001-0.ax').
% 0.64/0.78 %--------------------------------------------------------------------------
% 0.64/0.78 cnf(some_property,hypothesis,
% 0.64/0.78 ( X != additive_identity
% 0.64/0.78 | product(X,h(X,Y),Y) ) ).
% 0.64/0.78
% 0.64/0.78 cnf(a_times_b,hypothesis,
% 0.64/0.78 product(a,b,additive_identity) ).
% 0.64/0.78
% 0.64/0.78 %----Proving either a or b is the additive_identity. Either clause will
% 0.64/0.78 %----do.
% 0.64/0.78 cnf(a_not_additive_identity,negated_conjecture,
% 0.64/0.78 a != additive_identity ).
% 0.64/0.78
% 0.64/0.78 cnf(prove_b_is_additive_identity,negated_conjecture,
% 0.64/0.78 b != additive_identity ).
% 0.64/0.78
% 0.64/0.78 %--------------------------------------------------------------------------
% 0.64/0.78 %-------------------------------------------
% 0.64/0.78 % Proof found
% 0.64/0.78 % SZS status Theorem for theBenchmark
% 0.64/0.78 % SZS output start Proof
% 0.64/0.78 %ClaNum:37(EqnAxiom:16)
% 0.64/0.78 %VarNum:151(SingletonVarNum:73)
% 0.64/0.78 %MaxLitNum:5
% 0.64/0.78 %MaxfuncDepth:1
% 0.64/0.78 %SharedTerms:6
% 0.64/0.78 %goalClause: 24 25
% 0.64/0.78 %singleGoalClaCount:2
% 0.64/0.78 [17]P1(a1,a2,a3)
% 0.64/0.78 [24]~E(a1,a3)
% 0.64/0.78 [25]~E(a2,a3)
% 0.64/0.78 [18]P2(x181,a3,x181)
% 0.64/0.78 [19]P2(a3,x191,x191)
% 0.64/0.78 [20]P2(x201,f5(x201),a3)
% 0.64/0.78 [21]P2(f5(x211),x211,a3)
% 0.64/0.78 [22]P2(x221,x222,f4(x221,x222))
% 0.64/0.78 [23]P1(x231,x232,f6(x231,x232))
% 0.64/0.78 [26]P1(x261,f7(x261,x262),x262)+~E(x261,a3)
% 0.64/0.78 [27]~P2(x272,x271,x273)+P2(x271,x272,x273)
% 0.64/0.78 [28]~P2(x283,x284,x281)+E(x281,x282)+~P2(x283,x284,x282)
% 0.64/0.78 [29]~P1(x293,x294,x291)+E(x291,x292)+~P1(x293,x294,x292)
% 0.64/0.78 [30]~P2(x306,x304,x301)+P2(x301,x302,x303)+~P2(x304,x302,x305)+~P2(x306,x305,x303)
% 0.64/0.78 [31]~P2(x311,x316,x314)+P2(x311,x312,x313)+~P2(x314,x315,x313)+~P2(x316,x315,x312)
% 0.64/0.78 [32]~P1(x326,x324,x321)+P1(x321,x322,x323)+~P1(x324,x322,x325)+~P1(x326,x325,x323)
% 0.64/0.78 [33]~P1(x331,x336,x334)+P1(x331,x332,x333)+~P1(x334,x335,x333)+~P1(x336,x335,x332)
% 0.64/0.78 [34]~P1(x347,x345,x342)+~P1(x347,x344,x341)+P2(x341,x342,x343)+~P2(x344,x345,x346)+~P1(x347,x346,x343)
% 0.64/0.78 [35]~P1(x355,x357,x352)+~P1(x354,x357,x351)+P2(x351,x352,x353)+~P2(x354,x355,x356)+~P1(x356,x357,x353)
% 0.64/0.78 [36]~P1(x367,x362,x365)+~P1(x366,x362,x364)+P1(x361,x362,x363)+~P2(x364,x365,x363)+~P2(x366,x367,x361)
% 0.64/0.78 [37]~P1(x371,x377,x375)+~P1(x371,x376,x374)+P1(x371,x372,x373)+~P2(x374,x375,x373)+~P2(x376,x377,x372)
% 0.64/0.78 %EqnAxiom
% 0.64/0.78 [1]E(x11,x11)
% 0.64/0.78 [2]E(x22,x21)+~E(x21,x22)
% 0.64/0.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.64/0.78 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 0.64/0.78 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53))
% 0.64/0.78 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62))
% 0.64/0.78 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 0.64/0.78 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 0.64/0.78 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 0.64/0.78 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 0.64/0.78 [11]P1(x112,x113,x114)+~E(x111,x112)+~P1(x111,x113,x114)
% 0.64/0.78 [12]P1(x123,x122,x124)+~E(x121,x122)+~P1(x123,x121,x124)
% 0.64/0.78 [13]P1(x133,x134,x132)+~E(x131,x132)+~P1(x133,x134,x131)
% 0.64/0.78 [14]P2(x142,x143,x144)+~E(x141,x142)+~P2(x141,x143,x144)
% 0.64/0.78 [15]P2(x153,x152,x154)+~E(x151,x152)+~P2(x153,x151,x154)
% 0.64/0.78 [16]P2(x163,x164,x162)+~E(x161,x162)+~P2(x163,x164,x161)
% 0.64/0.78
% 0.64/0.78 %-------------------------------------------
% 0.64/0.78 cnf(38,plain,
% 0.64/0.78 (P1(a3,f7(a3,x381),x381)),
% 0.64/0.78 inference(equality_inference,[],[26])).
% 0.64/0.78 cnf(39,plain,
% 0.64/0.78 (E(x391,f4(x391,a3))),
% 0.64/0.78 inference(scs_inference,[],[18,22,28])).
% 0.64/0.78 cnf(40,plain,
% 0.64/0.78 (P2(x401,x402,f4(x401,x402))),
% 0.64/0.78 inference(rename_variables,[],[22])).
% 0.64/0.78 cnf(42,plain,
% 0.64/0.78 (E(f6(a3,f7(a3,x421)),x421)),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,38,28,29])).
% 0.64/0.78 cnf(43,plain,
% 0.64/0.78 (P1(x431,x432,f6(x431,x432))),
% 0.64/0.78 inference(rename_variables,[],[23])).
% 0.64/0.78 cnf(45,plain,
% 0.64/0.78 (E(f6(a3,f7(a3,x451)),f4(x451,a3))),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,38,28,29,3])).
% 0.64/0.78 cnf(46,plain,
% 0.64/0.78 (P1(f4(x461,a3),x462,f6(x461,x462))),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,43,38,28,29,3,11])).
% 0.64/0.78 cnf(47,plain,
% 0.64/0.78 (P1(x471,x472,f6(x471,x472))),
% 0.64/0.78 inference(rename_variables,[],[23])).
% 0.64/0.78 cnf(48,plain,
% 0.64/0.78 (P1(x481,f4(x482,a3),f6(x481,x482))),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,43,47,38,28,29,3,11,12])).
% 0.64/0.78 cnf(49,plain,
% 0.64/0.78 (P1(x491,x492,f6(x491,x492))),
% 0.64/0.78 inference(rename_variables,[],[23])).
% 0.64/0.78 cnf(50,plain,
% 0.64/0.78 (P1(x501,x502,f4(f6(x501,x502),a3))),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,43,47,49,38,28,29,3,11,12,13])).
% 0.64/0.78 cnf(51,plain,
% 0.64/0.78 (P2(f4(f6(x511,x512),a3),a3,f6(x511,x512))),
% 0.64/0.78 inference(scs_inference,[],[18,22,23,43,47,49,38,28,29,3,11,12,13,14])).
% 0.64/0.78 cnf(52,plain,
% 0.64/0.78 (P2(x521,a3,x521)),
% 0.64/0.78 inference(rename_variables,[],[18])).
% 0.64/0.78 cnf(53,plain,
% 0.64/0.78 (P2(a3,f4(f6(x531,x532),a3),f6(x531,x532))),
% 0.64/0.78 inference(scs_inference,[],[18,19,22,23,43,47,49,38,28,29,3,11,12,13,14,15])).
% 0.64/0.78 cnf(54,plain,
% 0.64/0.78 (P2(a3,x541,x541)),
% 0.64/0.78 inference(rename_variables,[],[19])).
% 0.64/0.78 cnf(56,plain,
% 0.64/0.78 (P2(a3,x561,x561)),
% 0.64/0.78 inference(rename_variables,[],[19])).
% 0.64/0.78 cnf(57,plain,
% 0.64/0.78 (P2(x571,f4(a3,a3),x571)),
% 0.64/0.78 inference(scs_inference,[],[18,52,19,54,22,40,23,43,47,49,38,28,29,3,11,12,13,14,15,16,31])).
% 0.64/0.78 cnf(61,plain,
% 0.64/0.78 (P1(x611,x612,f6(x611,x612))),
% 0.64/0.78 inference(rename_variables,[],[23])).
% 0.64/0.78 cnf(66,plain,
% 0.64/0.78 (P1(x661,x662,f6(x661,x662))),
% 0.64/0.78 inference(rename_variables,[],[23])).
% 0.64/0.78 cnf(67,plain,
% 0.64/0.78 (P2(x671,a3,x671)),
% 0.64/0.78 inference(rename_variables,[],[18])).
% 0.64/0.78 cnf(69,plain,
% 0.64/0.79 (P2(f6(a3,x691),f6(a3,x691),f6(a3,x691))),
% 0.64/0.79 inference(scs_inference,[],[18,52,67,19,54,22,40,23,43,47,49,61,66,38,28,29,3,11,12,13,14,15,16,31,32,34,35])).
% 0.64/0.79 cnf(72,plain,
% 0.64/0.79 (P1(x721,x722,f6(x721,x722))),
% 0.64/0.79 inference(rename_variables,[],[23])).
% 0.64/0.79 cnf(73,plain,
% 0.64/0.79 (P2(x731,a3,x731)),
% 0.64/0.79 inference(rename_variables,[],[18])).
% 0.64/0.79 cnf(75,plain,
% 0.64/0.79 (P1(a1,a2,f6(a3,a2))),
% 0.64/0.79 inference(scs_inference,[],[18,52,67,73,19,54,56,22,40,23,43,47,49,61,66,72,38,17,28,29,3,11,12,13,14,15,16,31,32,34,35,36])).
% 0.64/0.79 cnf(76,plain,
% 0.64/0.79 (P2(a3,x761,x761)),
% 0.64/0.79 inference(rename_variables,[],[19])).
% 0.64/0.79 cnf(77,plain,
% 0.64/0.79 (P2(x771,a3,x771)),
% 0.64/0.79 inference(rename_variables,[],[18])).
% 0.64/0.79 cnf(78,plain,
% 0.64/0.79 (P1(x781,x782,f6(x781,x782))),
% 0.64/0.79 inference(rename_variables,[],[23])).
% 0.64/0.79 cnf(80,plain,
% 0.64/0.79 (P1(a1,a2,f6(a1,a3))),
% 0.64/0.79 inference(scs_inference,[],[18,52,67,73,77,19,54,56,76,22,40,23,43,47,49,61,66,72,78,38,17,28,29,3,11,12,13,14,15,16,31,32,34,35,36,37])).
% 0.64/0.79 cnf(85,plain,
% 0.64/0.79 (E(f4(f6(x851,x851),a3),f6(x851,x851))),
% 0.64/0.79 inference(scs_inference,[],[18,52,67,73,77,19,54,56,76,22,40,23,43,47,49,61,66,72,78,38,17,28,29,3,11,12,13,14,15,16,31,32,34,35,36,37,2])).
% 0.64/0.79 cnf(91,plain,
% 0.64/0.79 (E(f4(x911,a3),x911)),
% 0.64/0.79 inference(scs_inference,[],[39,2])).
% 0.75/0.79 cnf(92,plain,
% 0.75/0.79 (P2(x921,f4(f4(a3,a3),a3),x921)),
% 0.75/0.79 inference(scs_inference,[],[39,57,2,15])).
% 0.75/0.79 cnf(93,plain,
% 0.75/0.79 (E(x931,f4(x931,a3))),
% 0.75/0.79 inference(rename_variables,[],[39])).
% 0.75/0.79 cnf(95,plain,
% 0.75/0.79 (P2(x951,f4(a3,a3),x951)),
% 0.75/0.79 inference(rename_variables,[],[57])).
% 0.75/0.79 cnf(96,plain,
% 0.75/0.79 (E(f5(f4(a3,a3)),a3)),
% 0.75/0.79 inference(scs_inference,[],[85,39,57,95,21,2,15,14,28])).
% 0.75/0.79 cnf(97,plain,
% 0.75/0.79 (P2(f5(x971),x971,a3)),
% 0.75/0.79 inference(rename_variables,[],[21])).
% 0.75/0.79 cnf(98,plain,
% 0.75/0.79 (P2(x981,f4(a3,a3),x981)),
% 0.75/0.79 inference(rename_variables,[],[57])).
% 0.75/0.79 cnf(100,plain,
% 0.75/0.79 (P1(f4(a1,a3),a2,f6(a3,a2))),
% 0.75/0.79 inference(scs_inference,[],[85,39,93,57,95,21,75,2,15,14,28,11])).
% 0.75/0.79 cnf(101,plain,
% 0.75/0.79 (E(x1011,f4(x1011,a3))),
% 0.75/0.79 inference(rename_variables,[],[39])).
% 0.75/0.79 cnf(103,plain,
% 0.75/0.79 (P2(x1031,f4(a3,a3),x1031)),
% 0.75/0.79 inference(rename_variables,[],[57])).
% 0.75/0.79 cnf(105,plain,
% 0.75/0.79 (E(x1051,f4(x1051,a3))),
% 0.75/0.79 inference(rename_variables,[],[39])).
% 0.75/0.79 cnf(106,plain,
% 0.75/0.79 (P1(f4(x1061,a3),x1062,f4(f6(x1061,x1062),a3))),
% 0.75/0.79 inference(scs_inference,[],[85,39,93,101,105,46,57,95,98,21,75,2,15,14,28,11,16,12,13])).
% 0.75/0.79 cnf(110,plain,
% 0.75/0.79 (P2(f5(a3),f5(f4(a3,a3)),a3)),
% 0.75/0.79 inference(scs_inference,[],[24,85,39,93,101,105,42,46,57,95,98,103,20,21,97,75,2,15,14,28,11,16,12,13,3,30])).
% 0.75/0.79 cnf(112,plain,
% 0.75/0.79 (P2(x1121,f4(a3,a3),x1121)),
% 0.75/0.79 inference(rename_variables,[],[57])).
% 0.75/0.79 cnf(113,plain,
% 0.75/0.79 (P2(x1131,f5(x1131),a3)),
% 0.75/0.79 inference(rename_variables,[],[20])).
% 0.75/0.79 cnf(115,plain,
% 0.75/0.79 (P2(f4(a3,a3),a3,a3)),
% 0.75/0.79 inference(scs_inference,[],[24,85,39,93,101,105,42,46,57,95,98,103,112,20,113,21,97,75,2,15,14,28,11,16,12,13,3,30,31])).
% 0.75/0.79 cnf(134,plain,
% 0.75/0.79 (P1(f4(a3,a3),f7(f4(a3,a3),x1341),x1341)),
% 0.75/0.79 inference(scs_inference,[],[91,26])).
% 0.75/0.79 cnf(135,plain,
% 0.75/0.79 (E(f4(x1351,a3),x1351)),
% 0.75/0.79 inference(rename_variables,[],[91])).
% 0.75/0.79 cnf(137,plain,
% 0.75/0.79 (E(f4(x1371,a3),f6(a3,f7(a3,x1371)))),
% 0.75/0.79 inference(scs_inference,[],[91,45,26,2])).
% 0.75/0.79 cnf(138,plain,
% 0.75/0.79 (P2(f4(f6(x1381,x1382),a3),f4(a3,a3),f6(x1381,x1382))),
% 0.75/0.79 inference(scs_inference,[],[91,45,39,51,26,2,15])).
% 0.75/0.79 cnf(139,plain,
% 0.75/0.79 (E(x1391,f4(x1391,a3))),
% 0.75/0.79 inference(rename_variables,[],[39])).
% 0.75/0.79 cnf(140,plain,
% 0.75/0.79 (E(a3,f4(f4(a3,a3),a3))),
% 0.75/0.79 inference(scs_inference,[],[91,45,39,92,51,19,26,2,15,28])).
% 0.75/0.79 cnf(141,plain,
% 0.75/0.79 (P2(a3,x1411,x1411)),
% 0.75/0.79 inference(rename_variables,[],[19])).
% 0.75/0.79 cnf(142,plain,
% 0.75/0.79 (P2(x1421,f4(f4(a3,a3),a3),x1421)),
% 0.75/0.79 inference(rename_variables,[],[92])).
% 0.75/0.79 cnf(144,plain,
% 0.75/0.79 (P1(f4(a1,a3),f4(a2,a3),f6(a3,a2))),
% 0.75/0.79 inference(scs_inference,[],[91,45,39,139,92,51,100,19,26,2,15,28,12])).
% 0.75/0.79 cnf(146,plain,
% 0.75/0.79 (P1(a3,f4(f7(a3,x1461),a3),f4(x1461,a3))),
% 0.75/0.79 inference(scs_inference,[],[91,45,39,139,48,92,51,100,19,26,2,15,28,12,13])).
% 0.75/0.79 cnf(147,plain,
% 0.75/0.79 (P1(x1471,f4(x1472,a3),f6(x1471,x1472))),
% 0.75/0.79 inference(rename_variables,[],[48])).
% 0.75/0.79 cnf(149,plain,
% 0.75/0.79 (P2(x1491,f4(f4(a3,a3),a3),x1491)),
% 0.75/0.79 inference(rename_variables,[],[92])).
% 0.75/0.79 cnf(150,plain,
% 0.75/0.79 (P1(x1501,f4(x1502,a3),f6(f4(x1501,a3),x1502))),
% 0.75/0.79 inference(scs_inference,[],[91,135,45,39,139,48,147,92,142,51,100,19,26,2,15,28,12,13,14,11])).
% 0.75/0.79 cnf(156,plain,
% 0.75/0.79 (P2(f6(a3,x1561),f5(f6(a3,x1561)),f6(a3,x1561))),
% 0.75/0.79 inference(scs_inference,[],[24,91,135,45,39,139,69,48,147,92,142,149,51,100,19,20,18,26,2,15,28,12,13,14,11,16,3,30])).
% 0.75/0.79 cnf(161,plain,
% 0.75/0.79 (P2(a3,x1611,x1611)),
% 0.75/0.79 inference(rename_variables,[],[19])).
% 0.75/0.79 cnf(164,plain,
% 0.75/0.79 (P2(f4(x1641,a3),f4(x1641,a3),f4(x1641,a3))),
% 0.75/0.79 inference(scs_inference,[],[24,91,135,45,39,139,69,48,147,92,142,149,51,100,19,141,161,20,18,26,2,15,28,12,13,14,11,16,3,30,31,35])).
% 0.75/0.79 cnf(170,plain,
% 0.75/0.79 (E(a3,f5(f4(a3,a3)))),
% 0.75/0.79 inference(scs_inference,[],[96,2])).
% 0.75/0.79 cnf(174,plain,
% 0.75/0.79 (E(f6(a3,x1741),f4(f6(a3,x1741),f6(a3,x1741)))),
% 0.75/0.79 inference(scs_inference,[],[96,69,100,106,22,2,29,28])).
% 0.75/0.79 cnf(175,plain,
% 0.75/0.79 (P2(x1751,x1752,f4(x1751,x1752))),
% 0.75/0.79 inference(rename_variables,[],[22])).
% 0.75/0.79 cnf(177,plain,
% 0.75/0.79 (P2(f4(x1771,a3),f6(a3,f7(a3,x1771)),f4(x1771,a3))),
% 0.75/0.79 inference(scs_inference,[],[137,96,69,100,164,106,22,2,29,28,15])).
% 0.75/0.79 cnf(178,plain,
% 0.75/0.79 (P2(f4(x1781,a3),f4(x1781,a3),f4(x1781,a3))),
% 0.75/0.79 inference(rename_variables,[],[164])).
% 0.75/0.79 cnf(180,plain,
% 0.75/0.79 (E(f4(x1801,a3),f6(a3,f7(a3,x1801)))),
% 0.75/0.79 inference(rename_variables,[],[137])).
% 0.75/0.79 cnf(182,plain,
% 0.75/0.79 (P2(f4(x1821,a3),f4(x1821,a3),f4(x1821,a3))),
% 0.75/0.79 inference(rename_variables,[],[164])).
% 0.75/0.79 cnf(183,plain,
% 0.75/0.79 (P1(f4(a1,a3),f6(a3,f7(a3,a2)),f6(a3,a2))),
% 0.75/0.79 inference(scs_inference,[],[137,180,96,69,100,144,164,178,106,22,2,29,28,15,11,14,12])).
% 0.75/0.79 cnf(184,plain,
% 0.75/0.79 (E(f4(x1841,a3),f6(a3,f7(a3,x1841)))),
% 0.75/0.79 inference(rename_variables,[],[137])).
% 0.75/0.79 cnf(188,plain,
% 0.75/0.79 (P2(f4(x1881,a3),f4(x1881,a3),f4(x1881,a3))),
% 0.75/0.79 inference(rename_variables,[],[164])).
% 0.75/0.79 cnf(191,plain,
% 0.75/0.79 (P2(f4(x1911,a3),f4(x1911,a3),f4(x1911,a3))),
% 0.75/0.79 inference(rename_variables,[],[164])).
% 0.75/0.79 cnf(198,plain,
% 0.75/0.79 (P2(f4(x1981,a3),f4(x1981,a3),f4(x1981,a3))),
% 0.75/0.79 inference(rename_variables,[],[164])).
% 0.75/0.79 cnf(204,plain,
% 0.75/0.79 (P2(x2041,x2041,x2041)),
% 0.75/0.79 inference(scs_inference,[],[24,137,180,184,96,39,69,100,134,50,138,144,164,178,182,188,191,198,106,53,46,48,22,175,2,29,28,15,11,14,12,13,16,3,30,32,31,34,35])).
% 0.75/0.79 cnf(216,plain,
% 0.75/0.79 (P1(x2161,x2162,f6(x2161,x2162))),
% 0.75/0.79 inference(rename_variables,[],[23])).
% 0.75/0.79 cnf(218,plain,
% 0.75/0.79 (E(x2181,f4(x2181,x2181))),
% 0.75/0.79 inference(scs_inference,[],[174,100,204,23,22,2,29,28])).
% 0.75/0.79 cnf(219,plain,
% 0.75/0.79 (P2(x2191,x2192,f4(x2191,x2192))),
% 0.75/0.79 inference(rename_variables,[],[22])).
% 0.75/0.79 cnf(221,plain,
% 0.75/0.79 (P2(f4(x2211,a3),x2211,f4(x2211,a3))),
% 0.75/0.79 inference(scs_inference,[],[91,174,100,204,23,22,2,29,28,15])).
% 0.75/0.79 cnf(222,plain,
% 0.75/0.79 (P2(x2221,x2221,x2221)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(223,plain,
% 0.75/0.79 (P1(x2231,x2232,f6(f4(x2231,a3),x2232))),
% 0.75/0.79 inference(scs_inference,[],[91,174,100,204,150,23,22,2,29,28,15,12])).
% 0.75/0.79 cnf(225,plain,
% 0.75/0.79 (P1(f4(a1,a3),a2,f4(f6(a3,a2),f6(a3,a2)))),
% 0.75/0.79 inference(scs_inference,[],[91,174,100,204,150,23,22,2,29,28,15,12,13])).
% 0.75/0.79 cnf(228,plain,
% 0.75/0.79 (E(f4(x2281,a3),x2281)),
% 0.75/0.79 inference(rename_variables,[],[91])).
% 0.75/0.79 cnf(229,plain,
% 0.75/0.79 (P2(x2291,f4(x2291,a3),f4(x2291,a3))),
% 0.75/0.79 inference(scs_inference,[],[91,228,174,100,204,222,150,183,23,22,2,29,28,15,12,13,11,14])).
% 0.75/0.79 cnf(230,plain,
% 0.75/0.79 (P2(x2301,x2301,x2301)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(232,plain,
% 0.75/0.79 (P2(x2321,x2321,x2321)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(234,plain,
% 0.75/0.79 (P2(x2341,x2341,x2341)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(236,plain,
% 0.75/0.79 (P2(x2361,f4(x2361,x2361),x2361)),
% 0.75/0.79 inference(scs_inference,[],[91,228,174,100,204,222,230,232,234,150,183,23,110,22,219,2,29,28,15,12,13,11,14,16,30,31])).
% 0.75/0.79 cnf(241,plain,
% 0.75/0.79 (P2(x2411,x2411,x2411)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(243,plain,
% 0.75/0.79 (P2(f6(a3,a2),f6(a3,a2),f6(f4(a1,a3),a2))),
% 0.75/0.79 inference(scs_inference,[],[91,228,174,100,204,222,230,232,234,241,150,183,106,23,216,110,22,219,2,29,28,15,12,13,11,14,16,30,31,34,35])).
% 0.75/0.79 cnf(252,plain,
% 0.75/0.79 (E(f6(f4(a3,a3),f7(a3,x2521)),x2521)),
% 0.75/0.79 inference(scs_inference,[],[140,223,38,2,29])).
% 0.75/0.79 cnf(256,plain,
% 0.75/0.79 (P2(x2561,x2561,x2561)),
% 0.75/0.79 inference(rename_variables,[],[204])).
% 0.75/0.79 cnf(259,plain,
% 0.75/0.79 (P2(x2591,f4(x2591,x2591),x2591)),
% 0.75/0.79 inference(rename_variables,[],[236])).
% 0.75/0.79 cnf(260,plain,
% 0.75/0.79 (E(f4(x2601,a3),f6(a3,f7(a3,x2601)))),
% 0.75/0.80 inference(rename_variables,[],[137])).
% 0.75/0.80 cnf(262,plain,
% 0.75/0.80 (E(f4(x2621,a3),f6(a3,f7(a3,x2621)))),
% 0.75/0.80 inference(rename_variables,[],[137])).
% 0.75/0.80 cnf(265,plain,
% 0.75/0.80 (P1(f4(a1,a3),f4(a2,a3),f4(f6(a3,a2),f6(a3,a2)))),
% 0.75/0.80 inference(scs_inference,[],[140,137,260,262,39,236,243,225,223,221,144,38,204,2,29,28,15,11,14,12])).
% 0.75/0.80 cnf(266,plain,
% 0.75/0.80 (E(x2661,f4(x2661,a3))),
% 0.75/0.80 inference(rename_variables,[],[39])).
% 0.75/0.80 cnf(270,plain,
% 0.75/0.80 (P2(x2701,f4(x2701,x2701),x2701)),
% 0.75/0.80 inference(rename_variables,[],[236])).
% 0.75/0.80 cnf(272,plain,
% 0.75/0.80 (P2(f6(x2721,x2722),f4(f4(a3,a3),f4(a3,a3)),f6(x2721,x2722))),
% 0.75/0.80 inference(scs_inference,[],[24,170,140,137,260,262,39,266,236,259,270,243,225,223,221,144,38,204,138,2,29,28,15,11,14,12,13,16,3,30])).
% 0.75/0.80 cnf(279,plain,
% 0.75/0.80 (P2(f6(a3,a2),f6(a3,a2),f6(a1,a2))),
% 0.75/0.80 inference(scs_inference,[],[24,170,140,137,260,262,39,266,100,236,259,270,243,225,223,156,221,144,38,21,204,256,46,138,2,29,28,15,11,14,12,13,16,3,30,31,34])).
% 0.75/0.80 cnf(296,plain,
% 0.75/0.80 (E(x2961,f6(a3,f7(a3,x2961)))),
% 0.75/0.80 inference(scs_inference,[],[42,2])).
% 0.75/0.80 cnf(300,plain,
% 0.75/0.80 (E(f6(a3,x3001),a3)),
% 0.75/0.80 inference(scs_inference,[],[42,146,150,156,20,2,29,28])).
% 0.75/0.80 cnf(303,plain,
% 0.75/0.80 (P2(f6(a3,a2),f4(f6(a3,a2),a3),f6(a1,a2))),
% 0.75/0.80 inference(scs_inference,[],[42,39,146,279,150,156,20,2,29,28,15])).
% 0.75/0.80 cnf(304,plain,
% 0.75/0.80 (E(x3041,f4(x3041,a3))),
% 0.75/0.80 inference(rename_variables,[],[39])).
% 0.75/0.80 cnf(306,plain,
% 0.75/0.80 (E(f4(x3061,a3),x3061)),
% 0.75/0.80 inference(rename_variables,[],[91])).
% 0.75/0.80 cnf(308,plain,
% 0.75/0.80 (P1(a3,f4(f7(a3,x3081),a3),f4(x3081,a3))),
% 0.75/0.80 inference(rename_variables,[],[146])).
% 0.75/0.80 cnf(320,plain,
% 0.75/0.80 (P2(f4(x3201,a3),f4(f4(a3,a3),f4(a3,a3)),f4(x3201,a3))),
% 0.75/0.80 inference(scs_inference,[],[24,91,306,42,170,39,304,252,100,146,308,272,265,279,115,177,150,156,20,46,2,29,28,15,12,13,11,14,16,3,33,30])).
% 0.75/0.80 cnf(343,plain,
% 0.75/0.80 (P1(x3431,x3432,f6(x3431,x3432))),
% 0.75/0.80 inference(rename_variables,[],[23])).
% 0.75/0.80 cnf(346,plain,
% 0.75/0.80 (P2(x3461,f4(x3461,a3),f4(x3461,a3))),
% 0.75/0.80 inference(rename_variables,[],[229])).
% 0.75/0.80 cnf(349,plain,
% 0.75/0.80 (P2(x3491,f4(x3491,a3),f4(x3491,a3))),
% 0.75/0.80 inference(rename_variables,[],[229])).
% 0.75/0.80 cnf(351,plain,
% 0.75/0.80 (E(x3511,f4(x3511,a3))),
% 0.75/0.80 inference(rename_variables,[],[39])).
% 0.75/0.80 cnf(360,plain,
% 0.75/0.80 ($false),
% 0.75/0.80 inference(scs_inference,[],[24,91,39,351,218,296,300,23,343,80,303,229,346,349,320,48,2,29,28,15,11,14,12,13,16,3]),
% 0.75/0.80 ['proof']).
% 0.75/0.80 % SZS output end Proof
% 0.75/0.80 % Total time :0.190000s
%------------------------------------------------------------------------------