%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n016.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 : Tue May 5 07:07:17 PM UTC 2026
% Result : Unsatisfiable 41.43s 41.64s
% Output : Refutation 41.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 23
% Syntax : Number of clauses : 36 ( 36 unt; 0 nHn; 7 RR)
% Number of literals : 36 ( 35 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-4 aty)
% Number of variables : 62 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(X,Y,btrue) = eps,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom) ).
cnf(axiom_005,axiom,
aux3(X,Y,Z,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
cnf(axiom_067,axiom,
orb(btrue,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_067) ).
cnf(axiom_068,axiom,
orb(bfalse,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_068) ).
cnf(axiom_071,axiom,
notb(btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_073,axiom,
andb(btrue,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_073) ).
cnf(axiom_075,axiom,
eps2(eps) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_075) ).
cnf(axiom_076,axiom,
eps2(x(X,Y)) = orb(eps2(X),eps2(Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_076) ).
cnf(axiom_077,axiom,
eps2(y(X,Y)) = andb(eps2(X),eps2(Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_077) ).
cnf(axiom_078,axiom,
eps2(star(X)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_078) ).
cnf(axiom_079,axiom,
eps2(nil4) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_079) ).
cnf(axiom_081,axiom,
step(atom(X),Y) = aux(Y,X,eq(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_081) ).
cnf(axiom_082,axiom,
step(x(X,Y),Z) = x(step(X,Z),step(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_082) ).
cnf(axiom_084,axiom,
step(star(X),Y) = y(step(X,Y),star(X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_084) ).
cnf(axiom_086,axiom,
step(eps,X) = nil4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_086) ).
cnf(axiom_087,axiom,
rec(X,nil2) = eps2(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_087) ).
cnf(axiom_088,axiom,
rec(X,cons2(Y,Z)) = rec(step(X,Y),Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_088) ).
cnf(axiom_100,axiom,
reck2(star(X),cons2(Y,Z)) = aux3(X,Y,Z,notb(eps2(X))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_100) ).
cnf(axiom_101,axiom,
prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_101) ).
cnf(axiom_109,axiom,
eq2(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_109) ).
cnf(axiom_110,axiom,
eq(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
cnf(axiom_111,axiom,
eq2(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_111) ).
cnf(goal,negated_conjecture,
eq2(prop_same(X,Y),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
cnf(123,plain,
step(atom(X),X) = eps,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[axiom_081,axiom_110,theory(equality)]),axiom,theory(equality)]) ).
cnf(131,plain,
eps2(step(star(X),Y)) = andb(eps2(step(X,Y)),btrue),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[axiom_077,axiom_084,theory(equality)]),axiom_078,theory(equality)]) ).
cnf(133,plain,
rec(eps,cons2(X,Y)) = rec(nil4,Y),
inference('PARAMODULATE',[status(thm)],[axiom_088,axiom_086,theory(equality)]) ).
cnf(134,plain,
rec(X,cons2(Y,nil2)) = eps2(step(X,Y)),
inference('PARAMODULATE',[status(thm)],[axiom_087,axiom_088,theory(equality)]) ).
cnf(135,plain,
rec(star(X),cons2(Y,nil2)) = andb(rec(X,cons2(Y,nil2)),btrue),
inference('REWRITE',[status(thm)],[131,134,theory(equality)]) ).
cnf(172,plain,
rec(x(X,Y),cons2(Z,nil2)) = orb(rec(X,cons2(Z,nil2)),rec(Y,cons2(Z,nil2))),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[axiom_076,axiom_082,theory(equality)]),134,theory(equality)]) ).
cnf(205,plain,
reck2(star(x(X,Y)),cons2(Z,U)) = aux3(x(X,Y),Z,U,notb(orb(eps2(X),eps2(Y)))),
inference('PARAMODULATE',[status(thm)],[axiom_100,axiom_076,theory(equality)]) ).
cnf(239,plain,
rec(atom(X),cons2(X,Y)) = rec(eps,Y),
inference('PARAMODULATE',[status(thm)],[axiom_088,123,theory(equality)]) ).
cnf(30263,plain,
reck2(star(x(eps,X)),cons2(Y,Z)) = bfalse,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[205,axiom_075,theory(equality)]),axiom_005,axiom_071,axiom_067,theory(equality)]) ).
cnf(30491,plain,
prop_same(star(x(eps,X)),cons2(Y,Z)) = eq2(rec(star(x(eps,X)),cons2(Y,Z)),bfalse),
inference('PARAMODULATE',[status(thm)],[axiom_101,30263,theory(equality)]) ).
cnf(57919,plain,
prop_same(star(x(eps,X)),cons2(Y,nil2)) = eq2(andb(rec(X,cons2(Y,nil2)),btrue),bfalse),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[30491,135,theory(equality)]),axiom_068,axiom_079,axiom_087,133,172,theory(equality)]) ).
cnf(58849,plain,
eq2(eq2(andb(rec(X,cons2(Y,nil2)),btrue),bfalse),bfalse) != btrue,
inference('PARAMODULATE',[status(thm)],[goal,57919,theory(equality)]) ).
cnf(59007,plain,
$false,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[58849,239,theory(equality)]),axiom_111,axiom_109,axiom_073,axiom_075,axiom_087,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.16/0.34 % Computer : n016.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 13:20:06 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.29/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.46 *
% 0.29/0.46 *
% 0.29/0.47 #<PACKAGE "SNARK-USER">
% 0.29/0.47 *
% 0.29/0.47 SNARK-TPTP-OPTIONS
% 0.29/0.47 *
% 0.29/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.29/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.29/0.47 (USE-FACTORING :POS)
% 0.29/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.29/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.29/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.29/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.29/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.29/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.29/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.29/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.29/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.29/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.29/0.47 *
% 0.29/0.47 "."
% 0.29/0.47 *
% 0.29/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2026-05-05T13:20:06
% 0.29/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n016.cluster.edu at 2026-05-05T13:20:06
% 0.29/0.49
% 0.29/0.50 ; Recognized left identity assertion (= (|z| |eps| ?X) ?X).
% 0.29/0.50 ; Recognized left identity assertion (= (|x2| |nil4| ?X) ?X).
% 0.29/0.50 ; Recognized left identity assertion (= (|orb| |bfalse| ?X) ?X).
% 41.43/41.64 ; Recognized left identity assertion (= (|andb| |btrue| ?X) ?X).
% 41.43/41.64
% 41.43/41.64 #||
% 41.43/41.64 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.43/41.64 % SZS output start Refutation
% See solution above
% 41.43/41.65 ||#
% 41.43/41.65
% 41.43/41.65 ; Summary of computation:
% 41.43/41.65 ; 198093 formulas have been input or derived (from 2502 formulas).
% 41.43/41.65 ; 59007 (30%) were retained. Of these,
% 41.43/41.65 ; 3932 ( 7%) were simplified or subsumed later,
% 41.43/41.65 ; 55075 (93%) are still being kept.
% 41.43/41.65 ;
% 41.43/41.65 ; Run time in seconds excluding printing time:
% 41.43/41.65 ; 0.016 0% Read assertion file (1 call)
% 41.43/41.65 ; 0.003 0% Assert (113 calls)
% 41.43/41.65 ; 14.601 35% Process new row (197,352 calls)
% 41.43/41.65 ; 0.145 0% Resolution (5,002 calls)
% 41.43/41.65 ; 3.583 9% Paramodulation (2,501 calls)
% 41.43/41.65 ; 15.552 38% Forward simplification (192,129 calls)
% 41.43/41.65 ; 2.433 6% Backward simplification (59,007 calls)
% 41.43/41.65 ; 3.902 9% Ordering (765,751 calls)
% 41.43/41.65 ; 0.000 0% Sortal reasoning (32 calls)
% 41.43/41.65 ; 0.001 0% Purity testing (1 call)
% 41.43/41.65 ; 0.943 2% Other
% 41.43/41.65 ; 41.179 Total
% 41.43/41.65 ; 41.177 Real time
% 41.43/41.65 ;
% 41.43/41.65 ; Term-hash-array has 221,954 terms in all.
% 41.43/41.65 ; Feature-vector-row-index has 0 entries (0 at peak, 0 added, 0 deleted).
% 41.43/41.65 ; Feature-vector-row-index has 1 node (1 at peak, 1 added, 0 deleted).
% 41.43/41.65 ; Path-index has 212,839 entries (212,839 at peak, 225,386 added, 12,547 deleted).
% 41.43/41.65 ; Path-index has 86,804 nodes (86,804 at peak, 88,552 added, 1,748 deleted).
% 41.43/41.65 ; Trie-index has 212,839 entries (212,839 at peak, 225,386 added, 12,547 deleted).
% 41.43/41.65 ; Trie-index has 1,345,525 nodes (1,345,525 at peak, 1,416,113 added, 70,588 deleted).
% 41.43/41.65 ; Retrieved 853,713 generalization terms in 2,222,695 calls.
% 41.43/41.65 ; Retrieved 87,298 instance terms in 73,421 calls.
% 41.43/41.65 ; Retrieved 223,472 unifiable terms in 25,099 calls.
% 41.43/41.65 ;
% 41.43/41.65 ; The agenda of rows to process has 349 entries:
% 41.43/41.65 ; 1 with value 23 42 with value 28 61 with value 32
% 41.43/41.65 ; 6 with value 25 50 with value 29 4 with value 33
% 41.43/41.65 ; 6 with value 26 115 with value 30 1 with value 34
% 41.43/41.65 ; 21 with value 27 42 with value 31
% 41.43/41.65 ; The agenda of rows to give has 52726 entries:
% 41.43/41.65 ; 5 with value (4 24) 6023 with value (4 37) 258 with value (4 50)
% 41.43/41.65 ; 19 with value (4 25) 4540 with value (4 38) 163 with value (4 51)
% 41.43/41.65 ; 8 with value (4 26) 4046 with value (4 39) 80 with value (4 52)
% 41.43/41.65 ; 11 with value (4 27) 2170 with value (4 40) 67 with value (4 53)
% 41.43/41.65 ; 859 with value (4 28) 2114 with value (4 41) 69 with value (4 54)
% 41.43/41.65 ; 984 with value (4 29) 1252 with value (4 42) 15 with value (4 55)
% 41.43/41.65 ; 1510 with value (4 30) 1515 with value (4 43) 47 with value (4 56)
% 41.43/41.65 ; 2207 with value (4 31) 1085 with value (4 44) 5 with value (4 57)
% 41.43/41.65 ; 2667 with value (4 32) 1162 with value (4 45) 13 with value (4 58)
% 41.43/41.65 ; 3971 with value (4 33) 687 with value (4 46) 4 with value (4 60)
% 41.43/41.65 ; 3969 with value (4 34) 599 with value (4 47) 1 with value (4 61)
% 41.43/41.65 ; 4976 with value (4 35) 482 with value (4 48) 1 with value (4 62)
% 41.43/41.65 ; 4722 with value (4 36) 420 with value (4 49)
% 41.43/41.65 Evaluation took:
% 41.43/41.65 41.185 seconds of real time
% 41.43/41.65 38.10136 seconds of user run time
% 41.43/41.65 3.088472 seconds of system run time
% 41.43/41.65 [Run times include 15.616 seconds GC run time.]
% 41.43/41.65 0 calls to %EVAL
% 41.43/41.65 0 page faults and
% 41.43/41.65 1,951,072,336 bytes consed.
% 41.43/41.65 :PROOF-FOUND
% 41.43/41.65 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2026-05-05T13:20:47
% 41.43/41.65 :PROOF-FOUND
% 41.43/41.65 *
%------------------------------------------------------------------------------