%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ROB013-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 : n015.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:10:24 EDT 2024
% Result : Unsatisfiable 115.53s 116.01s
% Output : CNFRefutation 115.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ROB013-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 18:31:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.48/0.58 start to proof:theBenchmark
% 115.46/115.99 %-------------------------------------------
% 115.46/115.99 % File :CSE---1.7
% 115.46/115.99 % Problem :theBenchmark
% 115.46/115.99 % Transform :cnf
% 115.46/115.99 % Format :tptp:raw
% 115.46/115.99 % Command :java -jar mcs_scs.jar %d %s
% 115.46/115.99
% 115.46/115.99 % Result :Theorem 114.900000s
% 115.46/115.99 % Output :CNFRefutation 114.900000s
% 115.46/115.99 %-------------------------------------------
% 115.53/116.01 %--------------------------------------------------------------------------
% 115.53/116.01 % File : ROB013-1 : TPTP v8.2.0. Released v1.0.0.
% 115.53/116.01 % Domain : Robbins Algebra
% 115.53/116.01 % Problem : If -(a + b) = c then -(c + -(-b + a)) = a
% 115.53/116.01 % Version : [Win90] (equality) axioms.
% 115.53/116.01 % English :
% 115.53/116.01
% 115.53/116.01 % Refs : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% 115.53/116.01 % Source : [Win90]
% 115.53/116.01 % Names : Lemma 3.5 [Win90]
% 115.53/116.01
% 115.53/116.01 % Status : Unsatisfiable
% 115.53/116.01 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.00 v6.0.0, 0.05 v5.5.0, 0.00 v2.0.0
% 115.53/116.01 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 2 RR)
% 115.53/116.01 % Number of literals : 5 ( 5 equ; 1 neg)
% 115.53/116.01 % Maximal clause size : 1 ( 1 avg)
% 115.53/116.01 % Maximal term depth : 6 ( 2 avg)
% 115.53/116.01 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 115.53/116.01 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 115.53/116.01 % Number of variables : 7 ( 0 sgn)
% 115.53/116.01 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 115.53/116.01
% 115.53/116.01 % Comments :
% 115.53/116.01 %--------------------------------------------------------------------------
% 115.53/116.01 %----Include axioms for Robbins algebra
% 115.53/116.01 include('Axioms/ROB001-0.ax').
% 115.53/116.01 %--------------------------------------------------------------------------
% 115.53/116.01 cnf(condition,hypothesis,
% 115.53/116.01 negate(add(a,b)) = c ).
% 115.53/116.01
% 115.53/116.01 cnf(prove_result,negated_conjecture,
% 115.53/116.01 negate(add(c,negate(add(negate(b),a)))) != a ).
% 115.53/116.01
% 115.53/116.01 %--------------------------------------------------------------------------
% 115.53/116.01 %-------------------------------------------
% 115.53/116.01 % Proof found
% 115.53/116.01 % SZS status Theorem for theBenchmark
% 115.53/116.01 % SZS output start Proof
% 115.53/116.02 %ClaNum:11(EqnAxiom:6)
% 115.53/116.02 %VarNum:15(SingletonVarNum:7)
% 115.53/116.02 %MaxLitNum:1
% 115.53/116.02 %MaxfuncDepth:5
% 115.53/116.02 %SharedTerms:12
% 115.53/116.02 %goalClause: 11
% 115.53/116.02 %singleGoalClaCount:1
% 115.53/116.02 [7]E(f4(f3(a1,a2)),a5)
% 115.53/116.02 [11]~E(f4(f3(a5,f4(f3(f4(a2),a1)))),a1)
% 115.53/116.02 [8]E(f3(x81,x82),f3(x82,x81))
% 115.53/116.02 [10]E(f4(f3(f4(f3(x101,x102)),f4(f3(x101,f4(x102))))),x101)
% 115.53/116.02 [9]E(f3(f3(x91,x92),x93),f3(x91,f3(x92,x93)))
% 115.53/116.02 %EqnAxiom
% 115.53/116.02 [1]E(x11,x11)
% 115.53/116.02 [2]E(x22,x21)+~E(x21,x22)
% 115.53/116.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 115.53/116.02 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 115.53/116.02 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 115.53/116.02 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 115.53/116.02
% 115.53/116.02 %-------------------------------------------
% 115.53/116.03 cnf(12,plain,
% 115.53/116.03 (E(f3(x121,f3(x122,x123)),f3(f3(x121,x122),x123))),
% 115.53/116.03 inference(scs_inference,[],[9,2])).
% 115.53/116.03 cnf(13,plain,
% 115.53/116.03 (E(f3(x131,f3(x132,x133)),f3(x132,f3(x133,x131)))),
% 115.53/116.03 inference(scs_inference,[],[8,9,2,3])).
% 115.53/116.03 cnf(16,plain,
% 115.53/116.03 (E(f3(x161,f3(x162,x163)),f3(x163,f3(x161,x162)))),
% 115.53/116.03 inference(scs_inference,[],[13,2])).
% 115.53/116.03 cnf(17,plain,
% 115.53/116.03 (E(a5,f4(f3(a1,a2)))),
% 115.53/116.03 inference(scs_inference,[],[7,2])).
% 115.53/116.03 cnf(18,plain,
% 115.53/116.03 (E(f3(x181,f3(x182,x183)),f3(f3(x183,x181),x182))),
% 115.53/116.03 inference(scs_inference,[],[12,16,7,2,3])).
% 115.53/116.03 cnf(20,plain,
% 115.53/116.03 (E(f3(f3(x201,x202),x203),f3(x202,f3(x203,x201)))),
% 115.53/116.03 inference(scs_inference,[],[18,2])).
% 115.53/116.03 cnf(21,plain,
% 115.53/116.03 (E(f4(f3(f4(f3(a5,x211)),f4(f3(a5,f4(x211))))),f4(f3(a1,a2)))),
% 115.53/116.03 inference(scs_inference,[],[17,18,10,2,3])).
% 115.53/116.03 cnf(24,plain,
% 115.53/116.03 (E(f3(f3(x241,x242),x243),f3(f3(x242,x243),x241))),
% 115.53/116.03 inference(scs_inference,[],[20,12,21,2,3])).
% 115.53/116.03 cnf(26,plain,
% 115.53/116.03 (E(f3(f3(x261,x262),x263),f3(f3(x263,x261),x262))),
% 115.53/116.03 inference(scs_inference,[],[24,2])).
% 115.53/116.03 cnf(29,plain,
% 115.53/116.03 (E(f3(f3(x291,f3(x292,x293)),x294),f3(f3(f3(x294,x291),x292),x293))),
% 115.53/116.03 inference(scs_inference,[],[26,12,10,2,3])).
% 115.53/116.03 cnf(32,plain,
% 115.53/116.03 (E(f3(f3(f3(x321,x322),x323),x324),f3(f3(x322,f3(x323,x324)),x321))),
% 115.53/116.03 inference(scs_inference,[],[29,2])).
% 115.53/116.03 cnf(121,plain,
% 115.53/116.03 (E(f3(x1211,f3(f3(x1212,x1213),x1214)),f3(f3(x1213,f3(x1214,x1211)),x1212))),
% 115.53/116.03 inference(scs_inference,[],[8,32,3])).
% 115.53/116.03 cnf(165,plain,
% 115.53/116.03 (E(f3(f3(x1651,f3(x1652,x1653)),x1654),f3(f3(x1653,f3(x1654,x1651)),x1652))),
% 115.53/116.03 inference(scs_inference,[],[9,121,3])).
% 115.53/116.03 cnf(223,plain,
% 115.53/116.03 (~E(f3(a5,f4(f3(f4(a2),a1))),f3(f4(f3(a1,x2231)),f4(f3(a1,f4(x2231)))))),
% 115.53/116.03 inference(scs_inference,[],[11,10,3,6])).
% 115.53/116.03 cnf(224,plain,
% 115.53/116.03 (~E(f3(a5,f4(f3(f4(a2),a1))),f3(f4(f3(a1,f4(x2241))),f4(f3(a1,x2241))))),
% 115.53/116.03 inference(scs_inference,[],[223,8,3])).
% 115.53/116.03 cnf(239,plain,
% 115.53/116.03 (~E(f3(f4(f3(a1,f4(x2391))),f4(f3(a1,x2391))),f3(a5,f4(f3(f4(a2),a1))))),
% 115.53/116.03 inference(scs_inference,[],[165,224,5,4,6,2])).
% 115.53/116.03 cnf(364,plain,
% 115.53/116.03 (E(f3(f4(f3(a1,a2)),x3641),f3(a5,x3641))),
% 115.53/116.03 inference(scs_inference,[],[7,4])).
% 115.53/116.03 cnf(366,plain,
% 115.53/116.03 (E(f3(x3661,f4(f3(a1,a2))),f3(x3661,a5))),
% 115.53/116.03 inference(scs_inference,[],[7,4,6,5])).
% 115.53/116.03 cnf(376,plain,
% 115.53/116.03 (~E(f3(a5,f4(f3(f4(a2),a1))),f3(f4(f3(a1,f4(a2))),a5))),
% 115.53/116.03 inference(scs_inference,[],[364,366,239,5,4,6,3,2])).
% 115.53/116.03 cnf(683,plain,
% 115.53/116.03 (E(f3(f3(x6831,x6832),x6833),f3(f3(x6832,x6831),x6833))),
% 115.53/116.03 inference(scs_inference,[],[8,4])).
% 115.53/116.03 cnf(685,plain,
% 115.53/116.03 (E(f4(f3(x6851,x6852)),f4(f3(x6852,x6851)))),
% 115.53/116.03 inference(scs_inference,[],[8,4,5,6])).
% 115.53/116.03 cnf(690,plain,
% 115.53/116.03 (E(f3(x6901,f3(f3(x6902,x6903),x6904)),f3(x6901,f3(f3(x6903,x6902),x6904)))),
% 115.53/116.03 inference(scs_inference,[],[683,4,5])).
% 115.53/116.03 cnf(710,plain,
% 115.53/116.03 (~E(f3(f4(f3(f4(a2),a1)),a5),f3(f4(f3(a1,f4(a2))),a5))),
% 115.53/116.03 inference(scs_inference,[],[8,690,376,4,5,6,3])).
% 115.53/116.03 cnf(1606,plain,
% 115.53/116.03 ($false),
% 115.53/116.04 inference(scs_inference,[],[710,685,4]),
% 115.53/116.04 ['proof']).
% 115.53/116.04 % SZS output end Proof
% 115.53/116.04 % Total time :114.900000s
%------------------------------------------------------------------------------