%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG023-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 : n018.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:40 EDT 2024
% Result : Unsatisfiable 83.18s 83.41s
% Output : CNFRefutation 83.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : RNG023-6 : TPTP v8.2.0. Released v1.0.0.
% 0.05/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n018.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Jun 18 14:00:08 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.53 start to proof:theBenchmark
% 83.18/83.41 %-------------------------------------------
% 83.18/83.41 % File :CSE---1.7
% 83.18/83.41 % Problem :theBenchmark
% 83.18/83.41 % Transform :cnf
% 83.18/83.41 % Format :tptp:raw
% 83.18/83.41 % Command :java -jar mcs_scs.jar %d %s
% 83.18/83.41
% 83.18/83.41 % Result :Theorem 82.710000s
% 83.18/83.41 % Output :CNFRefutation 82.710000s
% 83.18/83.41 %-------------------------------------------
% 83.18/83.41 %--------------------------------------------------------------------------
% 83.18/83.41 % File : RNG023-6 : TPTP v8.2.0. Released v1.0.0.
% 83.18/83.41 % Domain : Ring Theory (Alternative)
% 83.18/83.41 % Problem : Left alternative
% 83.18/83.41 % Version : [Ste87] (equality) axioms.
% 83.18/83.41 % Theorem formulation : In terms of associators
% 83.18/83.41 % English :
% 83.18/83.41
% 83.18/83.41 % Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% 83.18/83.41 % : [Ste92] Stevens (1992), Unpublished Note
% 83.18/83.41 % Source : [Ste92]
% 83.18/83.41 % Names : - [Ste87]
% 83.18/83.41
% 83.18/83.41 % Status : Unsatisfiable
% 83.18/83.41 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.00 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.07 v5.3.0, 0.00 v2.1.0, 0.13 v2.0.0
% 83.18/83.41 % Syntax : Number of clauses : 16 ( 16 unt; 0 nHn; 1 RR)
% 83.18/83.41 % Number of literals : 16 ( 16 equ; 1 neg)
% 83.18/83.41 % Maximal clause size : 1 ( 1 avg)
% 83.18/83.41 % Maximal term depth : 5 ( 2 avg)
% 83.18/83.41 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 83.18/83.41 % Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% 83.18/83.41 % Number of variables : 27 ( 2 sgn)
% 83.18/83.41 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 83.18/83.41
% 83.18/83.41 % Comments :
% 83.18/83.41 %--------------------------------------------------------------------------
% 83.18/83.41 %----Include nonassociative ring axioms
% 83.18/83.41 include('Axioms/RNG003-0.ax').
% 83.18/83.41 %--------------------------------------------------------------------------
% 83.18/83.41 cnf(prove_left_alternative,negated_conjecture,
% 83.18/83.41 associator(x,x,y) != additive_identity ).
% 83.18/83.41
% 83.18/83.41 %--------------------------------------------------------------------------
% 83.18/83.41 %-------------------------------------------
% 83.18/83.41 % Proof found
% 83.18/83.41 % SZS status Theorem for theBenchmark
% 83.18/83.41 % SZS output start Proof
% 83.18/83.42 %ClaNum:22(EqnAxiom:8)
% 83.18/83.42 %VarNum:48(SingletonVarNum:22)
% 83.18/83.42 %MaxLitNum:1
% 83.18/83.42 %MaxfuncDepth:4
% 83.18/83.42 %SharedTerms:10
% 83.18/83.42 %goalClause: 22
% 83.18/83.42 %singleGoalClaCount:1
% 83.18/83.42 [22]~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),a2)
% 83.18/83.42 [10]E(f4(x101,a2),a2)
% 83.18/83.42 [11]E(f4(a2,x111),a2)
% 83.18/83.42 [12]E(f3(x121,a2),x121)
% 83.18/83.42 [13]E(f3(a2,x131),x131)
% 83.18/83.42 [9]E(f1(f1(x91)),x91)
% 83.18/83.42 [14]E(f3(x141,f1(x141)),a2)
% 83.18/83.42 [15]E(f3(f1(x151),x151),a2)
% 83.18/83.42 [16]E(f3(x161,x162),f3(x162,x161))
% 83.18/83.42 [18]E(f4(f4(x181,x182),x182),f4(x181,f4(x182,x182)))
% 83.18/83.42 [19]E(f4(f4(x191,x191),x192),f4(x191,f4(x191,x192)))
% 83.18/83.42 [17]E(f3(f3(x171,x172),x173),f3(x171,f3(x172,x173)))
% 83.18/83.42 [20]E(f3(f4(x201,x202),f4(x201,x203)),f4(x201,f3(x202,x203)))
% 83.18/83.42 [21]E(f3(f4(x211,x212),f4(x213,x212)),f4(f3(x211,x213),x212))
% 83.18/83.42 %EqnAxiom
% 83.18/83.42 [1]E(x11,x11)
% 83.18/83.42 [2]E(x22,x21)+~E(x21,x22)
% 83.18/83.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 83.18/83.42 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 83.18/83.42 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 83.18/83.42 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 83.18/83.42 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 83.18/83.42 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 83.18/83.42
% 83.18/83.42 %-------------------------------------------
% 83.18/83.42 cnf(23,plain,
% 83.18/83.43 (E(x231,f3(x231,a2))),
% 83.18/83.43 inference(scs_inference,[],[12,2])).
% 83.18/83.43 cnf(26,plain,
% 83.18/83.43 (E(x261,f3(a2,x261))),
% 83.18/83.43 inference(scs_inference,[],[13,2])).
% 83.18/83.43 cnf(27,plain,
% 83.18/83.43 (E(f3(a2,f4(f4(x271,x272),x272)),f4(x271,f4(x272,x272)))),
% 83.18/83.43 inference(scs_inference,[],[13,18,2,3])).
% 83.18/83.43 cnf(30,plain,
% 83.18/83.43 (E(f3(f4(x301,x302),f4(x301,x303)),f4(x301,f3(x303,x302)))),
% 83.18/83.43 inference(scs_inference,[],[27,16,20,2,3])).
% 83.18/83.43 cnf(32,plain,
% 83.18/83.43 (E(f4(x321,f3(x322,x323)),f3(f4(x321,x323),f4(x321,x322)))),
% 83.18/83.43 inference(scs_inference,[],[30,2])).
% 83.18/83.43 cnf(33,plain,
% 83.18/83.43 (E(f1(f1(f3(f4(x331,x332),f4(x331,x333)))),f4(x331,f3(x333,x332)))),
% 83.18/83.43 inference(scs_inference,[],[30,9,2,3])).
% 83.18/83.43 cnf(36,plain,
% 83.18/83.43 (E(f4(x361,f3(x362,x362)),f4(f3(x361,x361),x362))),
% 83.18/83.43 inference(scs_inference,[],[32,33,21,2,3])).
% 83.18/83.43 cnf(39,plain,
% 83.18/83.43 (E(f4(f3(x391,x391),x392),f4(x391,f3(x392,x392)))),
% 83.18/83.43 inference(scs_inference,[],[36,2])).
% 83.18/83.43 cnf(54,plain,
% 83.18/83.43 (E(f4(f3(f4(x541,x541),f4(x541,x541)),x542),f4(x541,f4(x541,f3(x542,x542))))),
% 83.18/83.43 inference(scs_inference,[],[39,19,2,3])).
% 83.18/83.43 cnf(58,plain,
% 83.18/83.43 (E(f3(x581,x582),f3(x581,f3(x582,a2)))),
% 83.18/83.43 inference(scs_inference,[],[23,54,17,2,3])).
% 83.18/83.43 cnf(61,plain,
% 83.18/83.43 (E(f3(x611,f3(x612,a2)),f3(x611,x612))),
% 83.18/83.43 inference(scs_inference,[],[58,2])).
% 83.18/83.43 cnf(62,plain,
% 83.18/83.43 (~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),f4(x621,a2))),
% 83.18/83.43 inference(scs_inference,[],[22,58,10,2,3])).
% 83.18/83.43 cnf(67,plain,
% 83.18/83.43 (E(a2,f3(x671,f1(x671)))),
% 83.18/83.43 inference(scs_inference,[],[14,2])).
% 83.18/83.43 cnf(70,plain,
% 83.18/83.43 (E(a2,f3(f1(x701),x701))),
% 83.18/83.43 inference(scs_inference,[],[15,2])).
% 83.18/83.43 cnf(71,plain,
% 83.18/83.43 (E(f3(f1(x711),x711),f3(x712,f1(x712)))),
% 83.18/83.43 inference(scs_inference,[],[67,15,2,3])).
% 83.18/83.43 cnf(72,plain,
% 83.18/83.43 (E(f3(x721,f1(x721)),f3(f1(x722),x722))),
% 83.18/83.43 inference(scs_inference,[],[71,2])).
% 83.18/83.43 cnf(73,plain,
% 83.18/83.43 (E(f1(f1(a2)),f3(f1(x731),x731))),
% 83.18/83.43 inference(scs_inference,[],[70,71,9,2,3])).
% 83.18/83.43 cnf(75,plain,
% 83.18/83.43 (E(f3(f1(x751),x751),f1(f1(a2)))),
% 83.18/83.43 inference(scs_inference,[],[73,2])).
% 83.18/83.43 cnf(76,plain,
% 83.18/83.43 (E(f1(a2),f3(f1(x761),x761))),
% 83.18/83.43 inference(scs_inference,[],[72,26,73,2,3])).
% 83.18/83.43 cnf(79,plain,
% 83.18/83.43 (E(f3(f1(x791),x791),f1(a2))),
% 83.18/83.43 inference(scs_inference,[],[76,2])).
% 83.18/83.43 cnf(80,plain,
% 83.18/83.43 (E(f3(x801,f1(x801)),f1(f1(a2)))),
% 83.18/83.43 inference(scs_inference,[],[75,72,76,2,3])).
% 83.18/83.43 cnf(82,plain,
% 83.18/83.43 (E(f1(f1(a2)),f3(x821,f1(x821)))),
% 83.18/83.43 inference(scs_inference,[],[80,2])).
% 83.18/83.43 cnf(83,plain,
% 83.18/83.43 (E(f3(f1(x831),f3(x831,a2)),f1(a2))),
% 83.18/83.43 inference(scs_inference,[],[79,61,80,2,3])).
% 83.18/83.43 cnf(86,plain,
% 83.18/83.43 (E(f1(a2),f3(f1(x861),f3(x861,a2)))),
% 83.18/83.43 inference(scs_inference,[],[83,2])).
% 83.18/83.43 cnf(87,plain,
% 83.18/83.43 (E(f1(a2),f1(f1(a2)))),
% 83.18/83.43 inference(scs_inference,[],[23,75,83,2,3])).
% 83.18/83.43 cnf(90,plain,
% 83.18/83.43 (E(f1(f1(a2)),f1(a2))),
% 83.18/83.43 inference(scs_inference,[],[87,2])).
% 83.18/83.43 cnf(91,plain,
% 83.18/83.43 (E(f3(f1(x911),x911),f3(f1(x912),f3(x912,a2)))),
% 83.18/83.43 inference(scs_inference,[],[86,79,87,2,3])).
% 83.18/83.43 cnf(92,plain,
% 83.18/83.43 (E(f3(f1(x921),f3(x921,a2)),f3(f1(x922),x922))),
% 83.18/83.43 inference(scs_inference,[],[91,2])).
% 83.18/83.43 cnf(93,plain,
% 83.18/83.43 (E(f1(f1(a2)),f3(f1(x931),f3(x931,a2)))),
% 83.18/83.43 inference(scs_inference,[],[90,86,91,2,3])).
% 83.18/83.43 cnf(94,plain,
% 83.18/83.43 (E(f3(f1(x941),f3(x941,a2)),f1(f1(a2)))),
% 83.18/83.43 inference(scs_inference,[],[93,2])).
% 83.18/83.43 cnf(95,plain,
% 83.18/83.43 (E(f3(f1(x951),f3(f3(x951,a2),a2)),f3(f1(x952),x952))),
% 83.18/83.43 inference(scs_inference,[],[92,61,93,2,3])).
% 83.28/83.43 cnf(97,plain,
% 83.28/83.43 (E(f3(f1(x971),x971),f3(f1(x972),f3(f3(x972,a2),a2)))),
% 83.28/83.43 inference(scs_inference,[],[95,2])).
% 83.28/83.43 cnf(98,plain,
% 83.28/83.43 (E(f3(f1(x981),f3(x981,a2)),f3(x982,f1(x982)))),
% 83.28/83.43 inference(scs_inference,[],[82,94,95,2,3])).
% 83.28/83.43 cnf(100,plain,
% 83.28/83.43 (E(f3(f1(x1001),f3(x1001,a2)),f3(f1(x1002),f3(f3(x1002,a2),a2)))),
% 83.28/83.43 inference(scs_inference,[],[97,92,98,2,3])).
% 83.28/83.43 cnf(102,plain,
% 83.28/83.43 (E(f3(f1(x1021),f3(f3(x1021,a2),a2)),f3(f1(x1022),f3(x1022,a2)))),
% 83.28/83.43 inference(scs_inference,[],[100,2])).
% 83.28/83.43 cnf(103,plain,
% 83.28/83.43 (E(a2,f3(f1(x1031),f3(f3(x1031,a2),a2)))),
% 83.28/83.43 inference(scs_inference,[],[97,70,100,2,3])).
% 83.28/83.43 cnf(106,plain,
% 83.28/83.43 (E(f4(x1061,a2),f3(x1062,f1(x1062)))),
% 83.28/83.43 inference(scs_inference,[],[67,103,10,2,3])).
% 83.28/83.43 cnf(107,plain,
% 83.28/83.43 (E(f3(x1071,f1(x1071)),f4(x1072,a2))),
% 83.28/83.43 inference(scs_inference,[],[106,2])).
% 83.28/83.43 cnf(108,plain,
% 83.28/83.43 (E(f3(x1081,f1(x1081)),f3(f1(x1082),f3(f3(x1082,a2),a2)))),
% 83.28/83.43 inference(scs_inference,[],[72,97,106,2,3])).
% 83.28/83.43 cnf(111,plain,
% 83.28/83.43 (E(f3(f1(x1111),f3(f3(f3(x1111,a2),a2),a2)),f3(f1(x1112),f3(x1112,a2)))),
% 83.28/83.43 inference(scs_inference,[],[102,61,108,2,3])).
% 83.28/83.43 cnf(114,plain,
% 83.28/83.43 (~E(f3(f4(f4(a5,a5),a6),f1(f4(a5,f4(a5,a6)))),f3(x1141,f1(x1141)))),
% 83.28/83.43 inference(scs_inference,[],[107,111,62,2,3])).
% 83.28/83.43 cnf(152,plain,
% 83.28/83.43 (E(f4(x1521,a2),f3(f1(x1522),f3(f3(x1522,a2),a2)))),
% 83.28/83.43 inference(scs_inference,[],[10,103,3])).
% 83.28/83.43 cnf(230,plain,
% 83.28/83.43 (E(f3(f1(x2301),f3(f3(x2301,a2),a2)),f3(a2,f4(x2302,a2)))),
% 83.28/83.43 inference(scs_inference,[],[13,152,3,2])).
% 83.28/83.43 cnf(233,plain,
% 83.28/83.43 (E(f3(a2,f4(x2331,a2)),f3(a2,f3(f1(x2332),f3(f3(x2332,a2),a2))))),
% 83.28/83.43 inference(scs_inference,[],[13,230,3,2])).
% 83.28/83.43 cnf(291,plain,
% 83.28/83.43 (E(f3(a2,f3(f1(x2911),f3(f3(x2911,a2),a2))),f4(x2912,a2))),
% 83.28/83.43 inference(scs_inference,[],[233,26,3,2])).
% 83.28/83.43 cnf(2263,plain,
% 83.28/83.43 (E(f4(f4(x22631,x22631),x22632),f4(x22631,f4(x22631,x22632)))),
% 83.28/83.43 inference(rename_variables,[],[19])).
% 83.28/83.43 cnf(2266,plain,
% 83.28/83.43 ($false),
% 83.28/83.43 inference(scs_inference,[],[19,2263,291,114,3,4,7,5]),
% 83.28/83.43 ['proof']).
% 83.28/83.43 % SZS output end Proof
% 83.28/83.43 % Total time :82.710000s
%------------------------------------------------------------------------------