%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ROB002-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 : n005.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:22 EDT 2024
% Result : Unsatisfiable 102.90s 102.91s
% Output : CNFRefutation 102.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ROB002-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n005.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 : Wed Jun 19 18:42:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.55 start to proof:theBenchmark
% 102.83/102.88 %-------------------------------------------
% 102.83/102.88 % File :CSE---1.7
% 102.83/102.88 % Problem :theBenchmark
% 102.83/102.88 % Transform :cnf
% 102.83/102.88 % Format :tptp:raw
% 102.83/102.88 % Command :java -jar mcs_scs.jar %d %s
% 102.83/102.88
% 102.83/102.88 % Result :Theorem 102.310000s
% 102.83/102.88 % Output :CNFRefutation 102.310000s
% 102.83/102.88 %-------------------------------------------
% 102.90/102.90 %--------------------------------------------------------------------------
% 102.90/102.90 % File : ROB002-1 : TPTP v8.2.0. Released v1.0.0.
% 102.90/102.90 % Domain : Robbins Algebra
% 102.90/102.90 % Problem : --X = X => Boolean
% 102.90/102.90 % Version : [Win90] (equality) axioms.
% 102.90/102.90 % English : If --X = X then the algebra is Boolean.
% 102.90/102.90
% 102.90/102.90 % Refs : [HMT71] Henkin et al. (1971), Cylindrical Algebras
% 102.90/102.90 % : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% 102.90/102.90 % Source : [Win90]
% 102.90/102.90 % Names : Lemma 2.1 [Win90]
% 102.90/102.90
% 102.90/102.90 % Status : Unsatisfiable
% 102.90/102.90 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v6.1.0, 0.06 v6.0.0, 0.24 v5.5.0, 0.21 v5.4.0, 0.07 v5.3.0, 0.00 v5.2.0, 0.07 v5.1.0, 0.13 v5.0.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.13 v2.0.0
% 102.90/102.90 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR)
% 102.90/102.90 % Number of literals : 5 ( 5 equ; 1 neg)
% 102.90/102.90 % Maximal clause size : 1 ( 1 avg)
% 102.90/102.90 % Maximal term depth : 6 ( 2 avg)
% 102.90/102.90 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 102.90/102.90 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 102.90/102.90 % Number of variables : 8 ( 0 sgn)
% 102.90/102.90 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 102.90/102.91
% 102.90/102.91 % Comments : Commutativity, associativity, and Huntington's axiom
% 102.90/102.91 % axiomatize Boolean algebra.
% 102.90/102.91 %--------------------------------------------------------------------------
% 102.90/102.91 %----Include axioms for Robbins algebra
% 102.90/102.91 include('Axioms/ROB001-0.ax').
% 102.90/102.91 %--------------------------------------------------------------------------
% 102.90/102.91 cnf(double_negation,hypothesis,
% 102.90/102.91 negate(negate(X)) = X ).
% 102.90/102.91
% 102.90/102.91 cnf(prove_huntingtons_axiom,negated_conjecture,
% 102.90/102.91 add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b ).
% 102.90/102.91
% 102.90/102.91 %--------------------------------------------------------------------------
% 102.90/102.91 %-------------------------------------------
% 102.90/102.91 % Proof found
% 102.90/102.91 % SZS status Theorem for theBenchmark
% 102.90/102.91 % SZS output start Proof
% 102.90/102.92 %ClaNum:11(EqnAxiom:6)
% 102.90/102.92 %VarNum:17(SingletonVarNum:8)
% 102.90/102.92 %MaxLitNum:1
% 102.90/102.92 %MaxfuncDepth:5
% 102.90/102.92 %SharedTerms:10
% 102.90/102.92 %goalClause: 11
% 102.90/102.92 %singleGoalClaCount:1
% 102.90/102.92 [11]~E(f2(f1(f2(a3,f1(a4))),f1(f2(f1(a3),f1(a4)))),a4)
% 102.90/102.93 [7]E(f1(f1(x71)),x71)
% 102.90/102.93 [8]E(f2(x81,x82),f2(x82,x81))
% 102.90/102.93 [10]E(f1(f2(f1(f2(x101,x102)),f1(f2(x101,f1(x102))))),x101)
% 102.90/102.93 [9]E(f2(f2(x91,x92),x93),f2(x91,f2(x92,x93)))
% 102.90/102.93 %EqnAxiom
% 102.90/102.93 [1]E(x11,x11)
% 102.90/102.93 [2]E(x22,x21)+~E(x21,x22)
% 102.90/102.93 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 102.90/102.93 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 102.90/102.93 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 102.90/102.93 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 102.90/102.93
% 102.90/102.93 %-------------------------------------------
% 102.90/102.95 cnf(12,plain,
% 102.90/102.95 (E(x121,f1(f1(x121)))),
% 102.90/102.95 inference(scs_inference,[],[7,2])).
% 102.90/102.95 cnf(15,plain,
% 102.90/102.95 (E(f2(x151,f2(x152,x153)),f2(f2(x151,x152),x153))),
% 102.90/102.95 inference(scs_inference,[],[9,2])).
% 102.90/102.95 cnf(16,plain,
% 102.90/102.95 (E(f2(x161,f2(x162,x163)),f2(x162,f2(x163,x161)))),
% 102.90/102.95 inference(scs_inference,[],[8,9,2,3])).
% 102.90/102.95 cnf(19,plain,
% 102.90/102.95 (E(f2(x191,f2(x192,x193)),f2(x193,f2(x191,x192)))),
% 102.90/102.95 inference(scs_inference,[],[16,2])).
% 102.90/102.95 cnf(20,plain,
% 102.90/102.95 (E(x201,f1(f2(f1(f2(x201,x202)),f1(f2(x201,f1(x202))))))),
% 102.90/102.95 inference(scs_inference,[],[10,2])).
% 102.90/102.95 cnf(21,plain,
% 102.90/102.95 (E(f2(x211,f2(x212,x213)),f2(f2(x213,x211),x212))),
% 102.90/102.95 inference(scs_inference,[],[15,19,10,2,3])).
% 102.90/102.95 cnf(23,plain,
% 102.90/102.95 (E(f2(f2(x231,x232),x233),f2(x232,f2(x233,x231)))),
% 102.90/102.95 inference(scs_inference,[],[21,2])).
% 102.90/102.95 cnf(24,plain,
% 102.90/102.95 (E(f2(x241,f2(x242,f2(x243,x244))),f2(f2(x244,f2(x241,x242)),x243))),
% 102.90/102.95 inference(scs_inference,[],[15,21,2,3])).
% 102.90/102.95 cnf(27,plain,
% 102.90/102.95 (E(f2(f2(x271,f2(x272,x273)),x274),f2(x272,f2(x273,f2(x274,x271))))),
% 102.90/102.95 inference(scs_inference,[],[24,2])).
% 102.90/102.95 cnf(28,plain,
% 102.90/102.95 (E(f2(x281,f2(x282,f2(x283,x284))),f2(x284,f2(f2(x281,x282),x283)))),
% 102.90/102.95 inference(scs_inference,[],[23,19,24,2,3])).
% 102.90/102.95 cnf(31,plain,
% 102.90/102.95 (E(f2(x311,f2(f2(x312,x313),x314)),f2(x312,f2(x313,f2(x314,x311))))),
% 102.90/102.95 inference(scs_inference,[],[28,2])).
% 102.90/102.95 cnf(32,plain,
% 102.90/102.95 (E(f2(f2(x321,f2(x322,f2(x323,x324))),x325),f2(x323,f2(x324,f2(f2(x325,x321),x322))))),
% 102.90/102.95 inference(scs_inference,[],[27,23,28,2,3])).
% 102.90/102.95 cnf(35,plain,
% 102.90/102.95 (E(f2(x351,f2(x352,f2(f2(x353,x354),x355))),f2(f2(x354,f2(x355,f2(x351,x352))),x353))),
% 102.90/102.95 inference(scs_inference,[],[32,2])).
% 102.90/102.95 cnf(36,plain,
% 102.90/102.95 (E(f2(x361,f2(f2(f2(x362,x363),x364),x365)),f2(x363,f2(f2(x364,f2(x365,x361)),x362)))),
% 102.90/102.95 inference(scs_inference,[],[31,23,32,2,3])).
% 102.90/102.95 cnf(39,plain,
% 102.90/102.95 (E(f2(x391,f2(f2(x392,f2(x393,x394)),x395)),f2(x394,f2(f2(f2(x395,x391),x392),x393)))),
% 102.90/102.95 inference(scs_inference,[],[36,2])).
% 102.90/102.95 cnf(40,plain,
% 102.90/102.95 (E(f2(x401,f2(x402,f2(f2(x403,x404),x405))),f2(x404,f2(f2(x405,f2(x401,x402)),x403)))),
% 102.90/102.95 inference(scs_inference,[],[35,36,9,2,3])).
% 102.90/102.95 cnf(43,plain,
% 102.90/102.95 (E(f2(x431,f2(f2(x432,f2(x433,x434)),x435)),f2(f2(x434,f2(f2(x435,x431),x432)),x433))),
% 102.90/102.95 inference(scs_inference,[],[39,15,40,2,3])).
% 102.90/102.95 cnf(45,plain,
% 102.90/102.95 (E(f2(f2(x451,f2(f2(x452,x453),x454)),x455),f2(x453,f2(f2(x454,f2(x455,x451)),x452)))),
% 102.90/102.95 inference(scs_inference,[],[43,2])).
% 102.90/102.95 cnf(151,plain,
% 102.90/102.95 (E(f2(f2(x1511,x1512),x1513),f2(f2(x1513,x1511),x1512))),
% 102.90/102.95 inference(scs_inference,[],[8,15,3])).
% 102.90/102.95 cnf(251,plain,
% 102.90/102.95 (E(f2(x2511,x2512),f2(f1(f1(x2511)),x2512))),
% 102.90/102.95 inference(scs_inference,[],[12,151,4,5])).
% 102.90/102.95 cnf(257,plain,
% 102.90/102.95 (E(f1(f2(x2571,x2572)),f1(f2(f1(f1(x2571)),x2572)))),
% 102.90/102.95 inference(scs_inference,[],[251,6,4])).
% 102.90/102.95 cnf(258,plain,
% 102.90/102.95 (E(f2(f2(x2581,x2582),x2583),f2(f2(f1(f1(x2581)),x2582),x2583))),
% 102.90/102.95 inference(scs_inference,[],[251,6,4,5])).
% 102.90/102.95 cnf(314,plain,
% 102.90/102.95 (E(f2(f1(f2(x3141,x3142)),x3143),f2(f1(f2(f1(f1(x3141)),x3142)),x3143))),
% 102.90/102.95 inference(scs_inference,[],[257,5])).
% 102.90/102.95 cnf(320,plain,
% 102.90/102.95 (~E(f2(f1(f2(f1(f1(a3)),f1(a4))),f1(f2(f1(a3),f1(a4)))),a4)),
% 102.90/102.95 inference(scs_inference,[],[11,258,314,6,5,4,3])).
% 102.90/102.95 cnf(676,plain,
% 102.90/102.95 (E(f2(f1(f1(x6761)),x6762),f2(x6761,x6762))),
% 102.90/102.95 inference(scs_inference,[],[7,45,6,4,5])).
% 102.90/102.95 cnf(684,plain,
% 102.90/102.95 (E(f1(f2(f1(f1(x6841)),x6842)),f1(f2(x6841,x6842)))),
% 102.90/102.95 inference(scs_inference,[],[676,6,4])).
% 102.90/102.95 cnf(698,plain,
% 102.90/102.95 (E(f2(x6981,f1(f2(f1(f1(x6982)),x6983))),f2(x6981,f1(f2(x6982,x6983))))),
% 102.90/102.95 inference(scs_inference,[],[684,6])).
% 102.90/102.95 cnf(715,plain,
% 102.90/102.95 (E(f2(x7151,f2(x7152,x7153)),f2(x7151,f2(x7153,x7152)))),
% 102.90/102.95 inference(scs_inference,[],[8,6])).
% 102.90/102.95 cnf(717,plain,
% 102.90/102.95 (E(f1(f2(x7171,x7172)),f1(f2(x7172,x7171)))),
% 102.90/102.95 inference(scs_inference,[],[8,6,5,4])).
% 102.90/102.95 cnf(718,plain,
% 102.90/102.95 (~E(f2(f1(f2(f1(a3),f1(a4))),f1(f2(f1(f1(a3)),f1(a4)))),a4)),
% 102.90/102.95 inference(scs_inference,[],[8,320,6,5,4,3])).
% 102.90/102.95 cnf(723,plain,
% 102.90/102.95 (E(f1(f2(x7231,f2(x7232,x7233))),f1(f2(x7231,f2(x7233,x7232))))),
% 102.90/102.95 inference(scs_inference,[],[715,6,5,4])).
% 102.90/102.95 cnf(779,plain,
% 102.90/102.95 (E(f2(x7791,f2(f2(x7792,x7793),x7794)),f2(x7791,f2(x7792,f2(x7793,x7794))))),
% 102.90/102.95 inference(scs_inference,[],[9,6])).
% 102.90/102.95 cnf(788,plain,
% 102.90/102.95 (~E(f2(f1(f2(f1(a3),f1(a4))),f1(f2(a3,f1(a4)))),a4)),
% 102.90/102.95 inference(scs_inference,[],[779,718,698,6,5,4,3])).
% 102.90/102.95 cnf(864,plain,
% 102.90/102.95 (E(f1(f1(f2(x8641,x8642))),f1(f1(f2(x8642,x8641))))),
% 102.90/102.95 inference(scs_inference,[],[717,4])).
% 102.90/102.95 cnf(865,plain,
% 102.90/102.95 (E(f2(x8651,f1(f2(x8652,x8653))),f2(x8651,f1(f2(x8653,x8652))))),
% 102.90/102.95 inference(scs_inference,[],[717,4,6])).
% 102.90/102.95 cnf(866,plain,
% 102.90/102.95 (E(f2(f1(f2(x8661,x8662)),x8663),f2(f1(f2(x8662,x8661)),x8663))),
% 102.90/102.95 inference(scs_inference,[],[717,4,6,5])).
% 102.90/102.95 cnf(869,plain,
% 102.90/102.95 (E(f2(f1(f1(f2(x8691,x8692))),x8693),f2(f1(f1(f2(x8692,x8691))),x8693))),
% 102.90/102.95 inference(scs_inference,[],[864,4,6,5])).
% 102.90/102.95 cnf(870,plain,
% 102.90/102.95 (~E(f2(f1(f2(f1(a3),f1(a4))),f1(f2(f1(a4),a3))),a4)),
% 102.90/102.95 inference(scs_inference,[],[864,865,788,4,6,5,3])).
% 102.90/102.95 cnf(878,plain,
% 102.90/102.95 (~E(a4,f2(f1(f2(f1(a4),f1(a3))),f1(f2(f1(a4),a3))))),
% 102.90/102.95 inference(scs_inference,[],[866,870,6,5,4,3,2])).
% 102.90/102.95 cnf(896,plain,
% 102.90/102.95 (~E(f2(f1(f2(f1(a4),f1(a3))),f1(f2(f1(a4),a3))),f1(f1(a4)))),
% 102.90/102.95 inference(scs_inference,[],[12,878,869,6,5,4,3,2])).
% 102.90/102.95 cnf(910,plain,
% 102.90/102.95 (E(f1(f1(f2(x9101,f2(x9102,x9103)))),f1(f1(f2(x9101,f2(x9103,x9102)))))),
% 102.90/102.95 inference(scs_inference,[],[723,6,5,4])).
% 102.90/102.95 cnf(929,plain,
% 102.90/102.95 (~E(f1(f1(a4)),f1(f1(f2(f1(f2(f1(a4),f1(a3))),f1(f2(f1(a4),a3))))))),
% 102.90/102.95 inference(scs_inference,[],[12,896,910,6,5,4,3,2])).
% 102.90/102.95 cnf(1515,plain,
% 102.90/102.95 (E(f1(x15151),f1(f1(f2(f1(f2(x15151,x15152)),f1(f2(x15151,f1(x15152)))))))),
% 102.90/102.95 inference(scs_inference,[],[20,4])).
% 102.90/102.95 cnf(1527,plain,
% 102.90/102.95 ($false),
% 102.90/102.95 inference(scs_inference,[],[1515,929,864,3]),
% 102.90/102.95 ['proof']).
% 102.90/102.95 % SZS output end Proof
% 102.90/102.95 % Total time :102.310000s
%------------------------------------------------------------------------------