%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LDA007-3 : 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 11:43:26 EDT 2024
% Result : Unsatisfiable 61.04s 61.21s
% Output : CNFRefutation 61.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LDA007-3 : 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.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 13:05:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.42/0.60 start to proof:theBenchmark
% 61.04/61.20 %-------------------------------------------
% 61.04/61.20 % File :CSE---1.7
% 61.04/61.20 % Problem :theBenchmark
% 61.04/61.20 % Transform :cnf
% 61.04/61.20 % Format :tptp:raw
% 61.04/61.20 % Command :java -jar mcs_scs.jar %d %s
% 61.04/61.20
% 61.04/61.20 % Result :Theorem 60.430000s
% 61.04/61.20 % Output :CNFRefutation 60.430000s
% 61.04/61.20 %-------------------------------------------
% 61.04/61.21 %--------------------------------------------------------------------------
% 61.04/61.21 % File : LDA007-3 : TPTP v8.2.0. Released v1.0.0.
% 61.04/61.21 % Domain : LD-Algebras (Embedding algebras)
% 61.04/61.21 % Problem : Let g = cr(t). Show that t(tsg) = tt(ts)(tg)
% 61.04/61.21 % Version : [Jec93] axioms : Incomplete > Reduced & Augmented > Incomplete.
% 61.04/61.21 % English :
% 61.04/61.21
% 61.04/61.21 % Refs : [Jec93] Jech (1993), LD-Algebras
% 61.04/61.21 % Source : [Jec93]
% 61.04/61.21 % Names : Problem 8 [Jec93]
% 61.04/61.21
% 61.04/61.21 % Status : Unsatisfiable
% 61.04/61.21 % Rating : 0.00 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.05 v5.4.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.13 v2.0.0
% 61.04/61.21 % Syntax : Number of clauses : 7 ( 7 unt; 0 nHn; 6 RR)
% 61.04/61.21 % Number of literals : 7 ( 7 equ; 1 neg)
% 61.04/61.21 % Maximal clause size : 1 ( 1 avg)
% 61.04/61.21 % Maximal term depth : 3 ( 1 avg)
% 61.04/61.21 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 61.04/61.21 % Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% 61.04/61.21 % Number of variables : 3 ( 0 sgn)
% 61.04/61.21 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 61.04/61.21
% 61.04/61.21 % Comments :
% 61.04/61.21 %--------------------------------------------------------------------------
% 61.04/61.21 %----Include Embedding algebra axioms
% 61.04/61.21 % include('Axioms/LDA001-0.ax').
% 61.04/61.21 %--------------------------------------------------------------------------
% 61.04/61.21 cnf(a1,axiom,
% 61.04/61.21 f(X,f(Y,Z)) = f(f(X,Y),f(X,Z)) ).
% 61.04/61.21
% 61.04/61.21 cnf(clause_1,axiom,
% 61.04/61.21 tt = f(t,t) ).
% 61.04/61.21
% 61.04/61.21 cnf(clause_2,axiom,
% 61.04/61.21 ts = f(t,s) ).
% 61.04/61.21
% 61.04/61.21 cnf(clause_3,axiom,
% 61.04/61.21 tt_ts = f(tt,ts) ).
% 61.04/61.21
% 61.04/61.21 cnf(clause_4,axiom,
% 61.04/61.21 tk = f(t,k) ).
% 61.04/61.21
% 61.04/61.21 cnf(clause_5,axiom,
% 61.04/61.21 tsk = f(ts,k) ).
% 61.04/61.21
% 61.04/61.21 %----t(tsk) = tt(ts)(tk), where k=crit(t)
% 61.04/61.21 cnf(prove_equation,negated_conjecture,
% 61.04/61.21 f(t,tsk) != f(tt_ts,tk) ).
% 61.04/61.21
% 61.04/61.21 %--------------------------------------------------------------------------
% 61.04/61.21 %-------------------------------------------
% 61.04/61.21 % Proof found
% 61.04/61.21 % SZS status Theorem for theBenchmark
% 61.04/61.21 % SZS output start Proof
% 61.04/61.22 %ClaNum:12(EqnAxiom:5)
% 61.04/61.22 %VarNum:7(SingletonVarNum:3)
% 61.04/61.22 %MaxLitNum:1
% 61.04/61.22 %MaxfuncDepth:2
% 61.04/61.22 %SharedTerms:21
% 61.04/61.22 %goalClause: 12
% 61.04/61.22 %singleGoalClaCount:1
% 61.04/61.22 [6]E(f2(a1,a1),a5)
% 61.04/61.22 [7]E(f2(a1,a3),a6)
% 61.04/61.22 [8]E(f2(a5,a6),a9)
% 61.04/61.22 [9]E(f2(a1,a4),a7)
% 61.04/61.22 [10]E(f2(a6,a4),a8)
% 61.04/61.22 [12]~E(f2(a9,a7),f2(a1,a8))
% 61.04/61.22 [11]E(f2(f2(x111,x112),f2(x111,x113)),f2(x111,f2(x112,x113)))
% 61.04/61.22 %EqnAxiom
% 61.04/61.22 [1]E(x11,x11)
% 61.04/61.22 [2]E(x22,x21)+~E(x21,x22)
% 61.04/61.22 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 61.04/61.22 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 61.04/61.22 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 61.04/61.22
% 61.04/61.22 %-------------------------------------------
% 61.04/61.23 cnf(13,plain,
% 61.04/61.23 (E(f2(x131,f2(x132,x133)),f2(f2(x131,x132),f2(x131,x133)))),
% 61.04/61.23 inference(scs_inference,[],[11,2])).
% 61.04/61.23 cnf(16,plain,
% 61.04/61.23 (E(a6,f2(a1,a3))),
% 61.04/61.23 inference(scs_inference,[],[7,2])).
% 61.04/61.23 cnf(17,plain,
% 61.04/61.23 (E(x171,a9)+~E(x171,f2(a5,a6))),
% 61.04/61.23 inference(scs_inference,[],[7,8,2,3])).
% 61.04/61.23 cnf(20,plain,
% 61.04/61.23 (E(x201,a8)+~E(x201,f2(a6,a4))),
% 61.04/61.23 inference(scs_inference,[],[9,10,2,3])).
% 61.04/61.23 cnf(23,plain,
% 61.04/61.23 (E(a9,f2(a5,a6))),
% 61.04/61.23 inference(scs_inference,[],[8,2])).
% 61.04/61.23 cnf(25,plain,
% 61.04/61.23 (E(f2(a5,x251),f2(f2(a1,a1),x251))),
% 61.04/61.23 inference(scs_inference,[],[6,4,2])).
% 61.04/61.23 cnf(26,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),x261),f2(a5,x261))),
% 61.04/61.23 inference(scs_inference,[],[25,2])).
% 61.04/61.23 cnf(27,plain,
% 61.04/61.23 (E(a9,f2(f2(a1,a1),a6))),
% 61.04/61.23 inference(scs_inference,[],[23,25,2,3])).
% 61.04/61.23 cnf(30,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),a6),a9)),
% 61.04/61.23 inference(scs_inference,[],[27,2])).
% 61.04/61.23 cnf(31,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),f2(x311,x312)),f2(f2(a5,x311),f2(a5,x312)))),
% 61.04/61.23 inference(scs_inference,[],[13,26,27,2,3])).
% 61.04/61.23 cnf(35,plain,
% 61.04/61.23 (E(f2(f2(a5,x351),f2(a5,x352)),f2(f2(a1,a1),f2(x351,x352)))),
% 61.04/61.23 inference(scs_inference,[],[31,2])).
% 61.04/61.23 cnf(36,plain,
% 61.04/61.23 (E(f2(a1,f2(a1,x361)),f2(a5,f2(a1,x361)))),
% 61.04/61.23 inference(scs_inference,[],[13,26,31,2,3])).
% 61.04/61.23 cnf(40,plain,
% 61.04/61.23 (E(f2(a5,f2(a1,x401)),f2(a1,f2(a1,x401)))),
% 61.04/61.23 inference(scs_inference,[],[36,2])).
% 61.04/61.23 cnf(41,plain,
% 61.04/61.23 (E(f2(f2(a5,a1),f2(a5,x411)),f2(a1,f2(a1,x411)))),
% 61.04/61.23 inference(scs_inference,[],[35,36,11,2,3])).
% 61.04/61.23 cnf(44,plain,
% 61.04/61.23 (E(f2(x441,a5),f2(x441,f2(a1,a1)))),
% 61.04/61.23 inference(scs_inference,[],[6,2,5])).
% 61.04/61.23 cnf(46,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),a5),f2(a5,f2(a1,a1)))),
% 61.04/61.23 inference(scs_inference,[],[26,41,44,2,3])).
% 61.04/61.23 cnf(49,plain,
% 61.04/61.23 (E(f2(a5,f2(a1,a1)),f2(f2(a1,a1),a5))),
% 61.04/61.23 inference(scs_inference,[],[46,2])).
% 61.04/61.23 cnf(50,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),f2(a1,a1)),f2(f2(a1,a1),a5))),
% 61.04/61.23 inference(scs_inference,[],[26,46,2,3])).
% 61.04/61.23 cnf(54,plain,
% 61.04/61.23 (E(f2(x541,f2(a1,a1)),f2(x541,a5))),
% 61.04/61.23 inference(scs_inference,[],[44,2])).
% 61.04/61.23 cnf(55,plain,
% 61.04/61.23 (E(f2(f2(a5,a1),f2(a5,a1)),f2(f2(a1,a1),a5))),
% 61.04/61.23 inference(scs_inference,[],[35,50,44,2,3])).
% 61.04/61.23 cnf(59,plain,
% 61.04/61.23 (E(f2(a5,f2(a1,a1)),f2(a1,a5))),
% 61.04/61.23 inference(scs_inference,[],[54,40,55,2,3])).
% 61.04/61.23 cnf(63,plain,
% 61.04/61.23 (E(f2(a1,a5),f2(a5,f2(a1,a1)))),
% 61.04/61.23 inference(scs_inference,[],[59,2])).
% 61.04/61.23 cnf(64,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),f2(a1,a1)),f2(a1,a5))),
% 61.04/61.23 inference(scs_inference,[],[26,59,2,3])).
% 61.04/61.23 cnf(68,plain,
% 61.04/61.23 (E(f2(a1,a5),f2(f2(a1,a1),a5))),
% 61.04/61.23 inference(scs_inference,[],[49,63,64,2,3])).
% 61.04/61.23 cnf(70,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),a5),f2(a1,a5))),
% 61.04/61.23 inference(scs_inference,[],[68,2])).
% 61.04/61.23 cnf(94,plain,
% 61.04/61.23 (E(f2(f2(a1,x941),a5),f2(a1,f2(x941,a1)))),
% 61.04/61.23 inference(scs_inference,[],[13,54,3,2])).
% 61.04/61.23 cnf(101,plain,
% 61.04/61.23 (E(f2(a5,a5),f2(a1,a5))),
% 61.04/61.23 inference(scs_inference,[],[25,70,3])).
% 61.04/61.23 cnf(104,plain,
% 61.04/61.23 (E(f2(a5,f2(a1,a3)),a9)),
% 61.04/61.23 inference(scs_inference,[],[7,17,5])).
% 61.04/61.23 cnf(105,plain,
% 61.04/61.23 (E(a9,f2(a5,f2(a1,a3)))),
% 61.04/61.23 inference(scs_inference,[],[104,2])).
% 61.04/61.23 cnf(106,plain,
% 61.04/61.23 (E(f2(a5,a5),f2(a1,f2(a1,a1)))),
% 61.04/61.23 inference(scs_inference,[],[25,94,104,2,3])).
% 61.04/61.23 cnf(111,plain,
% 61.04/61.23 (E(f2(f2(a1,a1),a6),f2(a5,f2(a1,a3)))),
% 61.04/61.23 inference(scs_inference,[],[30,105,106,2,3])).
% 61.04/61.23 cnf(114,plain,
% 61.04/61.23 (E(f2(a5,a6),f2(a5,f2(a1,a3)))),
% 61.04/61.23 inference(scs_inference,[],[25,111,2,3])).
% 61.04/61.23 cnf(117,plain,
% 61.04/61.23 (E(f2(a5,f2(a1,a3)),f2(a5,a6))),
% 61.04/61.23 inference(scs_inference,[],[114,2])).
% 61.04/61.23 cnf(162,plain,
% 61.04/61.23 (E(f2(a1,f2(a1,a3)),f2(a5,a6))),
% 61.04/61.23 inference(scs_inference,[],[36,117,3])).
% 61.04/61.23 cnf(287,plain,
% 61.04/61.23 (~E(x2871,a4)+E(f2(a6,x2871),a8)),
% 61.04/61.23 inference(scs_inference,[],[20,5])).
% 61.04/61.23 cnf(960,plain,
% 61.04/61.23 (E(f2(x9601,f2(a6,x9602)),f2(x9601,a8))+~E(x9602,a4)),
% 61.04/61.23 inference(scs_inference,[],[287,5])).
% 61.04/61.23 cnf(961,plain,
% 61.04/61.23 (E(f2(x9611,f2(a6,a4)),f2(x9611,a8))),
% 61.04/61.23 inference(equality_inference,[],[960])).
% 61.04/61.23 cnf(963,plain,
% 61.04/61.23 (~E(f2(a9,a7),f2(a1,f2(a6,a4)))),
% 61.04/61.23 inference(scs_inference,[],[12,961,2,3])).
% 61.04/61.23 cnf(993,plain,
% 61.04/61.23 (~E(f2(a9,a7),f2(f2(a1,a6),f2(a1,a4)))),
% 61.04/61.23 inference(scs_inference,[],[963,11,3])).
% 61.04/61.23 cnf(1290,plain,
% 61.04/61.23 (~E(f2(f2(a1,a6),f2(a1,a4)),f2(a9,a7))),
% 61.04/61.23 inference(scs_inference,[],[993,101,4,5,2])).
% 61.04/61.23 cnf(1295,plain,
% 61.04/61.23 (E(f2(x12951,f2(a1,a4)),f2(x12951,a7))),
% 61.04/61.23 inference(scs_inference,[],[9,4,5])).
% 61.04/61.23 cnf(1327,plain,
% 61.04/61.23 (E(f2(x13271,a6),f2(x13271,f2(a1,a3)))),
% 61.04/61.23 inference(scs_inference,[],[16,4,5])).
% 61.04/61.23 cnf(1349,plain,
% 61.04/61.23 (E(f2(a1,a6),a9)),
% 61.04/61.23 inference(scs_inference,[],[162,1327,3,17])).
% 61.04/61.23 cnf(1352,plain,
% 61.04/61.23 (E(f2(f2(a1,a6),x13521),f2(a9,x13521))),
% 61.04/61.23 inference(scs_inference,[],[1349,4])).
% 61.04/61.23 cnf(1360,plain,
% 61.04/61.23 ($false),
% 61.04/61.23 inference(scs_inference,[],[1290,1352,1295,3]),
% 61.04/61.23 ['proof']).
% 61.04/61.23 % SZS output end Proof
% 61.04/61.23 % Total time :60.430000s
%------------------------------------------------------------------------------