%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM020-1 : TPTP v8.2.0. Bugfixed v4.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 12:22:59 EDT 2024
% Result : Unsatisfiable 58.86s 58.92s
% Output : CNFRefutation 58.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NUM020-1 : TPTP v8.2.0. Bugfixed v4.0.0.
% 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.36 % Computer : n022.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Sun Jun 23 03:30:24 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.55/0.60 start to proof:theBenchmark
% 58.82/58.91 %-------------------------------------------
% 58.82/58.91 % File :CSE---1.7
% 58.82/58.91 % Problem :theBenchmark
% 58.82/58.91 % Transform :cnf
% 58.82/58.91 % Format :tptp:raw
% 58.82/58.91 % Command :java -jar mcs_scs.jar %d %s
% 58.82/58.91
% 58.82/58.91 % Result :Theorem 58.260000s
% 58.82/58.91 % Output :CNFRefutation 58.260000s
% 58.82/58.91 %-------------------------------------------
% 58.82/58.92 %--------------------------------------------------------------------------
% 58.82/58.92 % File : NUM020-1 : TPTP v8.2.0. Bugfixed v4.0.0.
% 58.82/58.92 % Domain : Number Theory
% 58.82/58.92 % Problem : a + 1 = successor(a)
% 58.82/58.92 % Version : [LS74] axioms :
% 58.86/58.92 % Incomplete > Reduced > Incomplete.
% 58.86/58.92 % English :
% 58.86/58.92
% 58.86/58.92 % Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% 58.86/58.92 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 58.86/58.92 % Source : [SPRFN]
% 58.86/58.92 % Names : ls55 [LS74]
% 58.86/58.92 % : ls55 [WM76]
% 58.86/58.92
% 58.86/58.92 % Status : Unsatisfiable
% 58.86/58.92 % Rating : 0.00 v7.2.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.07 v4.1.0, 0.13 v4.0.1, 0.14 v4.0.0
% 58.86/58.92 % Syntax : Number of clauses : 12 ( 8 unt; 0 nHn; 7 RR)
% 58.86/58.92 % Number of literals : 17 ( 0 equ; 7 neg)
% 58.86/58.92 % Maximal clause size : 3 ( 1 avg)
% 58.86/58.92 % Maximal term depth : 3 ( 1 avg)
% 58.86/58.92 % Number of predicates : 1 ( 1 usr; 0 prp; 2-2 aty)
% 58.86/58.92 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% 58.86/58.92 % Number of variables : 17 ( 2 sgn)
% 58.86/58.92 % SPC : CNF_UNS_RFO_NEQ_HRN
% 58.86/58.92
% 58.86/58.92 % Comments : Surplus transitivity axiom removed.
% 58.86/58.92 % : This is dumb, because there is no need for the clause
% 58.86/58.92 % prove_a_contradiction.
% 58.86/58.92 % Bugfixes : v4.0.0 - Bugfix in NUM001-0.ax
% 58.86/58.92 %--------------------------------------------------------------------------
% 58.86/58.92 %----Include recursive function + and * axioms
% 58.86/58.92 include('Axioms/NUM001-0.ax').
% 58.86/58.92 %--------------------------------------------------------------------------
% 58.86/58.92 cnf(reflexivity,axiom,
% 58.86/58.92 equalish(X,X) ).
% 58.86/58.92
% 58.86/58.92 cnf(symmetry,axiom,
% 58.86/58.92 ( ~ equalish(X,Y)
% 58.86/58.92 | equalish(Y,X) ) ).
% 58.86/58.92
% 58.86/58.92 cnf(transitivity,axiom,
% 58.86/58.92 ( ~ equalish(X,Y)
% 58.86/58.92 | ~ equalish(Y,Z)
% 58.86/58.92 | equalish(X,Z) ) ).
% 58.86/58.92
% 58.86/58.92 cnf(one_succeeds_zero,axiom,
% 58.86/58.92 equalish(n1,successor(n0)) ).
% 58.86/58.92
% 58.86/58.92 cnf(deny_addition_lemma,negated_conjecture,
% 58.86/58.92 ~ equalish(add(a,successor(n0)),successor(a)) ).
% 58.86/58.92
% 58.86/58.92 cnf(prove_a_contradiction,negated_conjecture,
% 58.86/58.92 ~ equalish(successor(A),n0) ).
% 58.86/58.92
% 58.86/58.92 %--------------------------------------------------------------------------
% 58.86/58.92 %-------------------------------------------
% 58.86/58.92 % Proof found
% 58.86/58.92 % SZS status Theorem for theBenchmark
% 58.86/58.92 % SZS output start Proof
% 58.86/58.92 %ClaNum:12(EqnAxiom:0)
% 58.86/58.92 %VarNum:33(SingletonVarNum:17)
% 58.86/58.92 %MaxLitNum:3
% 58.86/58.92 %MaxfuncDepth:2
% 58.86/58.92 %SharedTerms:8
% 58.86/58.92 %goalClause: 7 8
% 58.86/58.92 %singleGoalClaCount:2
% 58.86/58.92 [2]P1(a1,f6(a2))
% 58.86/58.92 [8]~P1(f4(a5,f6(a2)),f6(a5))
% 58.86/58.92 [1]P1(x11,x11)
% 58.86/58.92 [3]P1(f3(x31,a2),a2)
% 58.86/58.92 [4]P1(f4(x41,a2),x41)
% 58.86/58.92 [7]~P1(f6(x71),a2)
% 58.86/58.92 [5]P1(f4(x51,f6(x52)),f6(f4(x51,x52)))
% 58.86/58.92 [6]P1(f3(x61,f6(x62)),f4(f3(x61,x62),x61))
% 58.86/58.92 [9]~P1(x92,x91)+P1(x91,x92)
% 58.86/58.92 [10]~P1(x101,x102)+P1(f6(x101),f6(x102))
% 58.86/58.92 [11]P1(x111,x112)+~P1(f6(x111),f6(x112))
% 58.86/58.92 [12]~P1(x121,x123)+P1(x121,x122)+~P1(x123,x122)
% 58.86/58.92 %EqnAxiom
% 58.86/58.92
% 58.86/58.92 %-------------------------------------------
% 58.86/58.93 cnf(13,plain,
% 58.86/58.93 (~P1(a2,f6(x131))),
% 58.86/58.93 inference(scs_inference,[],[7,9])).
% 58.86/58.93 cnf(18,plain,
% 58.86/58.93 (~P1(a1,a2)),
% 58.86/58.93 inference(scs_inference,[],[2,13,12,9])).
% 58.86/58.93 cnf(19,plain,
% 58.86/58.93 (~P1(a2,a1)),
% 58.86/58.93 inference(scs_inference,[],[18,9])).
% 58.86/58.93 cnf(21,plain,
% 58.86/58.93 (P1(f6(f6(a2)),f6(a1))),
% 58.86/58.93 inference(scs_inference,[],[2,9,10])).
% 58.86/58.93 cnf(24,plain,
% 58.86/58.93 (~P1(f6(a1),f6(a2))),
% 58.86/58.93 inference(scs_inference,[],[19,9,11])).
% 58.86/58.93 cnf(25,plain,
% 58.86/58.93 (~P1(f6(a2),f6(a1))),
% 58.86/58.93 inference(scs_inference,[],[24,9])).
% 58.86/58.93 cnf(36,plain,
% 58.86/58.93 (~P1(f6(a1),f4(f6(a2),a2))),
% 58.86/58.93 inference(scs_inference,[],[18,4,11,12])).
% 58.86/58.93 cnf(39,plain,
% 58.86/58.93 (~P1(a2,f4(a1,a2))),
% 58.86/58.93 inference(scs_inference,[],[4,19,36,9,12])).
% 58.86/58.93 cnf(43,plain,
% 58.86/58.93 (~P1(f4(a1,a2),a2)),
% 58.86/58.93 inference(scs_inference,[],[39,9])).
% 58.86/58.93 cnf(48,plain,
% 58.86/58.93 (~P1(f6(a2),f6(f4(a1,a2)))),
% 58.86/58.93 inference(scs_inference,[],[43,11,9])).
% 58.86/58.93 cnf(49,plain,
% 58.86/58.93 (~P1(f6(f4(a1,a2)),f6(a2))),
% 58.86/58.93 inference(scs_inference,[],[48,9])).
% 58.86/58.93 cnf(51,plain,
% 58.86/58.93 (~P1(f6(a2),f4(f6(f4(a1,a2)),a2))),
% 58.86/58.93 inference(scs_inference,[],[4,48,9,12])).
% 58.86/58.93 cnf(57,plain,
% 58.86/58.93 (~P1(f6(a2),f4(f6(a1),a2))),
% 58.86/58.93 inference(scs_inference,[],[4,25,51,9,12])).
% 58.86/58.93 cnf(75,plain,
% 58.86/58.93 (~P1(f4(a1,a2),f4(a2,a2))),
% 58.86/58.93 inference(scs_inference,[],[4,43,57,9,12])).
% 58.86/58.93 cnf(79,plain,
% 58.86/58.93 (~P1(f4(a2,a2),f4(a1,a2))),
% 58.86/58.93 inference(scs_inference,[],[75,9])).
% 58.86/58.93 cnf(84,plain,
% 58.86/58.93 (~P1(f6(f4(a1,a2)),f6(f4(a2,a2)))),
% 58.86/58.93 inference(scs_inference,[],[79,11,9])).
% 58.86/58.93 cnf(85,plain,
% 58.86/58.93 (~P1(f6(f4(a2,a2)),f6(f4(a1,a2)))),
% 58.86/58.93 inference(scs_inference,[],[84,9])).
% 58.86/58.93 cnf(94,plain,
% 58.86/58.93 (~P1(f4(a1,f6(a2)),f6(f4(a2,a2)))),
% 58.86/58.93 inference(scs_inference,[],[85,5,12,9])).
% 58.86/58.93 cnf(110,plain,
% 58.86/58.93 (~P1(a1,f6(f4(a1,a2)))),
% 58.86/58.93 inference(scs_inference,[],[49,2,12,9])).
% 58.86/58.93 cnf(112,plain,
% 58.86/58.93 (~P1(f6(f6(f4(a1,a2))),f6(a1))),
% 58.86/58.93 inference(scs_inference,[],[110,11,9])).
% 58.86/58.93 cnf(115,plain,
% 58.86/58.93 (~P1(f4(a1,f6(a2)),f4(a2,f6(a2)))),
% 58.86/58.93 inference(scs_inference,[],[112,94,5,9,12])).
% 58.86/58.93 cnf(121,plain,
% 58.86/58.93 (~P1(f4(a2,a2),f4(f4(a1,a2),a2))),
% 58.86/58.93 inference(scs_inference,[],[4,79,115,9,12])).
% 58.86/58.93 cnf(127,plain,
% 58.86/58.93 (~P1(f6(x1271),f3(x1272,a2))),
% 58.86/58.93 inference(scs_inference,[],[7,121,3,9,12])).
% 58.86/58.93 cnf(246,plain,
% 58.86/58.93 (P1(f4(f3(x2461,x2462),x2461),f3(x2461,f6(x2462)))),
% 58.86/58.93 inference(scs_inference,[],[6,1,12,9])).
% 58.86/58.93 cnf(416,plain,
% 58.86/58.93 (~P1(f6(x4161),f4(f3(x4162,a2),a2))),
% 58.86/58.93 inference(scs_inference,[],[127,4,12])).
% 58.86/58.93 cnf(720,plain,
% 58.86/58.93 (~P1(f3(a2,f6(a2)),f6(x7201))),
% 58.86/58.93 inference(scs_inference,[],[416,6,12,9])).
% 58.86/58.93 cnf(722,plain,
% 58.86/58.93 (~P1(f3(a2,f6(a2)),a1)),
% 58.86/58.93 inference(scs_inference,[],[720,2,12])).
% 58.86/58.93 cnf(1331,plain,
% 58.86/58.93 (P1(f6(x13311),f6(f4(x13311,a2)))),
% 58.86/58.93 inference(scs_inference,[],[4,10,9])).
% 58.86/58.93 cnf(1334,plain,
% 58.86/58.93 (P1(f3(a2,x13341),f3(a2,f6(x13341)))),
% 58.86/58.93 inference(scs_inference,[],[1331,246,11,12])).
% 58.86/58.93 cnf(1339,plain,
% 58.86/58.93 (P1(f6(a1),f6(f6(a2)))),
% 58.86/58.93 inference(scs_inference,[],[21,1,12,9])).
% 58.86/58.93 cnf(1360,plain,
% 58.86/58.93 (P1(a1,f4(f6(a2),a2))),
% 58.86/58.93 inference(scs_inference,[],[1339,1331,12,11])).
% 58.86/58.93 cnf(1394,plain,
% 58.86/58.93 (~P1(f6(f4(a5,a2)),f6(a5))),
% 58.86/58.93 inference(scs_inference,[],[8,722,1334,1360,5,10,11,9,12])).
% 58.86/58.93 cnf(1421,plain,
% 58.86/58.93 ($false),
% 58.86/58.93 inference(scs_inference,[],[1394,4,10]),
% 58.86/58.93 ['proof']).
% 58.86/58.93 % SZS output end Proof
% 58.86/58.93 % Total time :58.260000s
%------------------------------------------------------------------------------