%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG007-4 : 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 : n009.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:36 EDT 2024
% Result : Unsatisfiable 68.75s 68.98s
% Output : CNFRefutation 68.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : RNG007-4 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n009.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Jun 18 13:13:24 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 68.75/68.97 %-------------------------------------------
% 68.75/68.97 % File :CSE---1.7
% 68.75/68.97 % Problem :theBenchmark
% 68.75/68.97 % Transform :cnf
% 68.75/68.97 % Format :tptp:raw
% 68.75/68.97 % Command :java -jar mcs_scs.jar %d %s
% 68.75/68.97
% 68.75/68.97 % Result :Theorem 68.200000s
% 68.75/68.97 % Output :CNFRefutation 68.200000s
% 68.75/68.97 %-------------------------------------------
% 68.75/68.98 %--------------------------------------------------------------------------
% 68.75/68.98 % File : RNG007-4 : TPTP v8.2.0. Released v1.0.0.
% 68.75/68.98 % Domain : Ring Theory
% 68.75/68.98 % Problem : In Boolean rings, X is its own inverse
% 68.75/68.98 % Version : [Peterson & Stickel, 1981] (equality) axioms.
% 68.75/68.98 % Theorem formulation : Equality.
% 68.75/68.98 % English : Given a ring in which for all x, x * x = x, prove that for
% 68.75/68.98 % all x, x + x = additive_identity
% 68.75/68.98
% 68.75/68.98 % Refs : [PS81] Peterson & Stickel (1981), Complete Sets of Reductions
% 68.75/68.98 % Source : [ANL]
% 68.75/68.98 % Names : lemma.ver2.in [ANL]
% 68.75/68.98
% 68.75/68.98 % Status : Unsatisfiable
% 68.75/68.98 % Rating : 0.00 v7.4.0, 0.04 v7.3.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.14 v5.5.0, 0.11 v5.4.0, 0.00 v5.1.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
% 68.75/68.98 % Syntax : Number of clauses : 16 ( 16 unt; 0 nHn; 2 RR)
% 68.75/68.98 % Number of literals : 16 ( 16 equ; 1 neg)
% 68.75/68.98 % Maximal clause size : 1 ( 1 avg)
% 68.75/68.98 % Maximal term depth : 3 ( 2 avg)
% 68.75/68.98 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 68.75/68.98 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 68.75/68.98 % Number of variables : 26 ( 2 sgn)
% 68.75/68.98 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 68.75/68.98
% 68.75/68.98 % Comments :
% 68.75/68.98 %--------------------------------------------------------------------------
% 68.75/68.98 %----Include ring theory axioms
% 68.75/68.98 include('Axioms/RNG002-0.ax').
% 68.75/68.98 %--------------------------------------------------------------------------
% 68.75/68.98 cnf(boolean_ring,hypothesis,
% 68.75/68.98 multiply(X,X) = X ).
% 68.75/68.98
% 68.75/68.98 cnf(prove_inverse,negated_conjecture,
% 68.75/68.98 add(a,a) != additive_identity ).
% 68.75/68.98
% 68.75/68.98 %--------------------------------------------------------------------------
% 68.75/68.98 %-------------------------------------------
% 68.75/68.98 % Proof found
% 68.75/68.98 % SZS status Theorem for theBenchmark
% 68.75/68.98 % SZS output start Proof
% 68.75/68.98 %ClaNum:24(EqnAxiom:8)
% 68.75/68.98 %VarNum:53(SingletonVarNum:26)
% 68.75/68.98 %MaxLitNum:1
% 68.75/68.98 %MaxfuncDepth:2
% 68.75/68.98 %SharedTerms:6
% 68.75/68.98 %goalClause: 24
% 68.75/68.98 %singleGoalClaCount:1
% 68.75/68.98 [9]E(f4(a1),a1)
% 68.75/68.98 [24]~E(f2(a3,a3),a1)
% 68.75/68.98 [11]E(f5(x111,a1),a1)
% 68.75/68.98 [12]E(f5(a1,x121),a1)
% 68.75/68.98 [13]E(f2(a1,x131),x131)
% 68.75/68.98 [14]E(f5(x141,x141),x141)
% 68.75/68.98 [10]E(f4(f4(x101)),x101)
% 68.75/68.98 [15]E(f2(f4(x151),x151),a1)
% 68.75/68.98 [16]E(f2(x161,x162),f2(x162,x161))
% 68.75/68.98 [17]E(f4(f5(x171,x172)),f5(x171,f4(x172)))
% 68.75/68.98 [18]E(f4(f5(x181,x182)),f5(f4(x181),x182))
% 68.75/68.98 [19]E(f4(f2(x191,x192)),f2(f4(x191),f4(x192)))
% 68.75/68.98 [20]E(f2(f2(x201,x202),x203),f2(x201,f2(x202,x203)))
% 68.75/68.98 [21]E(f5(f5(x211,x212),x213),f5(x211,f5(x212,x213)))
% 68.75/68.98 [22]E(f2(f5(x221,x222),f5(x221,x223)),f5(x221,f2(x222,x223)))
% 68.75/68.98 [23]E(f2(f5(x231,x232),f5(x233,x232)),f5(f2(x231,x233),x232))
% 68.75/68.98 %EqnAxiom
% 68.75/68.98 [1]E(x11,x11)
% 68.75/68.98 [2]E(x22,x21)+~E(x21,x22)
% 68.75/68.98 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 68.75/68.99 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 68.75/68.99 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 68.75/68.99 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 68.75/68.99 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73))
% 68.75/68.99 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82))
% 68.75/68.99
% 68.75/68.99 %-------------------------------------------
% 68.84/68.99 cnf(25,plain,
% 68.84/68.99 (E(x251,f5(x251,x251))),
% 68.84/68.99 inference(scs_inference,[],[14,2])).
% 68.84/68.99 cnf(28,plain,
% 68.84/68.99 (E(x281,f2(a1,x281))),
% 68.84/68.99 inference(scs_inference,[],[13,2])).
% 68.84/68.99 cnf(31,plain,
% 68.84/68.99 (E(f5(x311,f2(x312,x313)),f2(f5(x311,x312),f5(x311,x313)))),
% 68.84/68.99 inference(scs_inference,[],[22,2])).
% 68.84/68.99 cnf(37,plain,
% 68.84/68.99 (E(f5(f2(x371,x372),x373),f2(f5(x371,x373),f5(x372,x373)))),
% 68.84/68.99 inference(scs_inference,[],[23,2])).
% 68.84/68.99 cnf(55,plain,
% 68.84/68.99 (E(f5(x551,f4(x552)),f4(f5(x551,x552)))),
% 68.84/68.99 inference(scs_inference,[],[17,2])).
% 68.84/68.99 cnf(58,plain,
% 68.84/68.99 (E(f5(f4(x581),x582),f4(f5(x581,x582)))),
% 68.84/68.99 inference(scs_inference,[],[18,2])).
% 68.84/68.99 cnf(59,plain,
% 68.84/68.99 (E(f4(x591),f4(f5(f4(x591),x591)))),
% 68.84/68.99 inference(scs_inference,[],[55,25,18,2,3])).
% 68.84/68.99 cnf(62,plain,
% 68.84/68.99 (E(f4(f5(f4(x621),x621)),f4(x621))),
% 68.84/68.99 inference(scs_inference,[],[59,2])).
% 68.84/68.99 cnf(63,plain,
% 68.84/68.99 (~E(f2(a3,a3),f5(x631,a1))),
% 68.84/68.99 inference(scs_inference,[],[24,59,11,2,3])).
% 68.84/68.99 cnf(64,plain,
% 68.84/68.99 (E(f2(f4(x641),f4(x642)),f4(f2(x641,x642)))),
% 68.84/68.99 inference(scs_inference,[],[19,2])).
% 68.84/68.99 cnf(65,plain,
% 68.84/68.99 (E(f5(f4(f4(x651)),x651),f4(x651))),
% 68.84/68.99 inference(scs_inference,[],[62,58,19,2,3])).
% 68.84/68.99 cnf(68,plain,
% 68.84/68.99 (E(f4(x681),f5(f4(f4(x681)),x681))),
% 68.84/68.99 inference(scs_inference,[],[65,2])).
% 68.84/68.99 cnf(70,plain,
% 68.84/68.99 (E(f2(x701,f2(x702,x703)),f2(f2(x701,x702),x703))),
% 68.84/68.99 inference(scs_inference,[],[20,2])).
% 68.84/68.99 cnf(71,plain,
% 68.84/68.99 (~E(f2(a3,a3),f4(a1))),
% 68.84/68.99 inference(scs_inference,[],[68,63,20,2,3])).
% 68.84/68.99 cnf(74,plain,
% 68.84/68.99 (E(f5(x741,f5(x742,x743)),f5(f5(x741,x742),x743))),
% 68.84/68.99 inference(scs_inference,[],[21,2])).
% 68.84/68.99 cnf(75,plain,
% 68.84/68.99 (E(f2(x751,x752),f2(f2(a1,x751),x752))),
% 68.84/68.99 inference(scs_inference,[],[70,28,21,2,3])).
% 68.84/68.99 cnf(78,plain,
% 68.84/68.99 (E(f2(f2(a1,x781),x782),f2(x781,x782))),
% 68.84/68.99 inference(scs_inference,[],[75,2])).
% 68.84/68.99 cnf(83,plain,
% 68.84/68.99 (E(f2(f2(a1,f4(x831)),f4(x832)),f4(f2(x831,x832)))),
% 68.84/68.99 inference(scs_inference,[],[64,78,9,2,3])).
% 68.84/68.99 cnf(88,plain,
% 68.84/68.99 (E(a1,f2(f4(x881),x881))),
% 68.84/68.99 inference(scs_inference,[],[15,2])).
% 68.84/68.99 cnf(91,plain,
% 68.84/68.99 (E(a1,f5(x911,a1))),
% 68.84/68.99 inference(scs_inference,[],[11,2])).
% 68.84/68.99 cnf(92,plain,
% 68.84/68.99 (E(f4(a1),f2(f4(x921),x921))),
% 68.84/68.99 inference(scs_inference,[],[88,9,11,2,3])).
% 68.84/68.99 cnf(93,plain,
% 68.84/68.99 (E(f2(f4(x931),x931),f4(a1))),
% 68.84/68.99 inference(scs_inference,[],[92,2])).
% 68.84/68.99 cnf(94,plain,
% 68.84/68.99 (E(a1,f2(f5(x941,a1),f5(x942,a1)))),
% 68.84/68.99 inference(scs_inference,[],[37,91,92,2,3])).
% 68.84/68.99 cnf(97,plain,
% 68.84/68.99 (E(f2(f5(x971,a1),f5(x972,a1)),a1)),
% 68.84/68.99 inference(scs_inference,[],[94,2])).
% 68.84/68.99 cnf(98,plain,
% 68.84/68.99 (~E(f2(a3,a3),f2(f4(x981),x981))),
% 68.84/68.99 inference(scs_inference,[],[93,94,71,2,3])).
% 68.84/68.99 cnf(99,plain,
% 68.84/68.99 (~E(a3,f4(a3))),
% 68.84/68.99 inference(scs_inference,[],[93,94,71,2,3,5])).
% 68.84/68.99 cnf(101,plain,
% 68.84/68.99 (~E(f2(a3,a3),f2(f5(x1011,a1),f5(x1012,a1)))),
% 68.84/68.99 inference(scs_inference,[],[24,97,12,2,3])).
% 68.84/68.99 cnf(102,plain,
% 68.84/68.99 (~E(f2(a3,a3),f5(x1021,f2(a1,a1)))),
% 68.84/68.99 inference(scs_inference,[],[31,101,3])).
% 68.84/68.99 cnf(105,plain,
% 68.84/68.99 (~E(f2(a3,a3),f5(x1051,f5(x1052,f2(a1,a1))))),
% 68.84/68.99 inference(scs_inference,[],[74,102,3])).
% 68.84/68.99 cnf(112,plain,
% 68.84/68.99 (~E(f2(a3,a3),f4(f5(x1121,f2(a1,a1))))),
% 68.84/69.00 inference(scs_inference,[],[68,105,3])).
% 68.84/69.00 cnf(123,plain,
% 68.84/69.00 (~E(a3,f4(f5(f4(a3),a3)))),
% 68.84/69.00 inference(scs_inference,[],[62,99,3])).
% 68.84/69.00 cnf(214,plain,
% 68.84/69.00 (~E(a3,f5(f4(a3),f4(a3)))),
% 68.84/69.00 inference(scs_inference,[],[55,123,3])).
% 68.84/69.00 cnf(219,plain,
% 68.84/69.00 (~E(f2(a3,a3),f4(f2(a1,a1)))),
% 68.84/69.00 inference(scs_inference,[],[59,112,3])).
% 68.84/69.00 cnf(222,plain,
% 68.84/69.00 (~E(f2(a3,a3),f2(f2(a1,f4(a1)),f4(a1)))),
% 68.84/69.00 inference(scs_inference,[],[83,219,3])).
% 68.84/69.00 cnf(226,plain,
% 68.84/69.00 (~E(f2(a3,a3),f2(a1,f2(f4(a1),f4(a1))))),
% 68.84/69.00 inference(scs_inference,[],[70,222,3])).
% 68.84/69.00 cnf(242,plain,
% 68.84/69.00 (~E(f2(a3,a3),f2(x2421,f4(x2421)))),
% 68.84/69.00 inference(scs_inference,[],[98,16,3])).
% 68.84/69.00 cnf(247,plain,
% 68.84/69.00 (~E(a3,f4(f2(a1,a3)))),
% 68.84/69.00 inference(scs_inference,[],[75,242,3,6])).
% 68.84/69.00 cnf(248,plain,
% 68.84/69.00 (~E(a3,f2(f4(a1),f4(a3)))),
% 68.84/69.00 inference(scs_inference,[],[64,247,3])).
% 68.84/69.00 cnf(337,plain,
% 68.84/69.00 (~E(a3,f4(f5(a3,f4(a3))))),
% 68.84/69.00 inference(scs_inference,[],[214,18,3])).
% 68.84/69.00 cnf(339,plain,
% 68.84/69.00 (~E(a3,f5(a3,f4(f4(a3))))),
% 68.84/69.00 inference(scs_inference,[],[55,337,3])).
% 68.84/69.00 cnf(347,plain,
% 68.84/69.00 (~E(f2(a3,a3),f2(f2(f4(a1),f4(a1)),a1))),
% 68.84/69.00 inference(scs_inference,[],[226,16,3])).
% 68.84/69.00 cnf(390,plain,
% 68.84/69.00 (~E(a3,f2(a1,f2(f4(a1),f4(a3))))),
% 68.84/69.00 inference(scs_inference,[],[248,13,3])).
% 68.84/69.00 cnf(481,plain,
% 68.84/69.00 (~E(f2(a3,a3),f2(f4(a1),f2(f4(a1),a1)))),
% 68.84/69.00 inference(scs_inference,[],[347,70,3])).
% 68.84/69.00 cnf(523,plain,
% 68.84/69.00 (~E(a3,f2(f2(a1,a1),f2(f4(a1),f4(a3))))),
% 68.84/69.00 inference(scs_inference,[],[390,78,3])).
% 68.84/69.00 cnf(647,plain,
% 68.84/69.00 (~E(a3,f2(f2(f2(a1,a1),f4(a1)),f4(a3)))),
% 68.84/69.00 inference(scs_inference,[],[523,20,3])).
% 68.84/69.00 cnf(733,plain,
% 68.84/69.00 (~E(a3,f2(f4(a3),f2(f2(a1,a1),f4(a1))))),
% 68.84/69.00 inference(scs_inference,[],[647,16,3])).
% 68.84/69.00 cnf(783,plain,
% 68.84/69.00 (~E(a3,f2(f2(f4(a3),f2(a1,a1)),f4(a1)))),
% 68.84/69.00 inference(scs_inference,[],[733,20,3])).
% 68.84/69.00 cnf(895,plain,
% 68.84/69.00 (E(f5(x8951,f4(f4(x8952))),f5(x8951,x8952))),
% 68.84/69.00 inference(scs_inference,[],[10,783,2,8])).
% 68.84/69.00 cnf(1081,plain,
% 68.84/69.00 (~E(f5(a3,f4(f4(a3))),a3)),
% 68.84/69.00 inference(scs_inference,[],[339,2])).
% 68.84/69.00 cnf(1103,plain,
% 68.84/69.00 ($false),
% 68.84/69.00 inference(scs_inference,[],[14,895,481,1081,2,3]),
% 68.84/69.00 ['proof']).
% 68.84/69.00 % SZS output end Proof
% 68.84/69.00 % Total time :68.200000s
%------------------------------------------------------------------------------