%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : RNG090+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n026.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 : 600s
% DateTime : Mon Jul 18 20:40:45 EDT 2022
% Result : Theorem 3.27s 3.48s
% Output : Refutation 3.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 17
% Syntax : Number of clauses : 32 ( 28 unt; 0 nHn; 32 RR)
% Number of literals : 41 ( 12 equ; 10 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 9 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
( ~ aElement0(X)
| ~ aElement0(Y)
| aElement0(sdtpldt0(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
cnf(6,axiom,
( ~ aElement0(X)
| ~ aElement0(Y)
| sdtpldt0(X,Y) = sdtpldt0(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddComm) ).
cnf(7,axiom,
( ~ aElement0(X)
| ~ aElement0(Y)
| ~ aElement0(Z)
| sdtpldt0(sdtpldt0(X,Y),Z) = sdtpldt0(X,sdtpldt0(Y,Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddAsso) ).
cnf(24,axiom,
( ~ aSet0(X)
| ~ aElementOf0(Y,X)
| aElement0(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
cnf(53,hypothesis,
aSet0(xI),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__870) ).
cnf(57,hypothesis,
aSet0(xJ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__870) ).
cnf(65,hypothesis,
aElementOf0('SKOLEMAAAV14',xI),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__901) ).
cnf(66,hypothesis,
aElementOf0('SKOLEMAAAV15',xJ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__901) ).
cnf(67,hypothesis,
sdtpldt0('SKOLEMAAAV14','SKOLEMAAAV15') = xy,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__901) ).
cnf(70,hypothesis,
aElementOf0(xk,xI),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__934) ).
cnf(71,hypothesis,
aElementOf0(xl,xJ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__934) ).
cnf(72,hypothesis,
xx = sdtpldt0(xk,xl),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__934) ).
cnf(73,hypothesis,
aElementOf0(xm,xI),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__967) ).
cnf(74,hypothesis,
aElementOf0(xn,xJ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__967) ).
cnf(75,hypothesis,
xy = sdtpldt0(xm,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__967) ).
cnf(77,hypothesis,
aElementOf0(sdtpldt0(xl,xn),xJ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__994) ).
cnf(80,negated_conjecture,
sdtpldt0(xx,xy) != sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
cnf(98,plain,
aElement0('SKOLEMAAAV15'),
inference('HYPERRESOLVE',[status(thm)],[24,57,66]) ).
cnf(99,plain,
aElement0(xl),
inference('HYPERRESOLVE',[status(thm)],[24,57,71]) ).
cnf(100,plain,
aElement0(xn),
inference('HYPERRESOLVE',[status(thm)],[24,57,74]) ).
cnf(102,plain,
aElement0('SKOLEMAAAV14'),
inference('HYPERRESOLVE',[status(thm)],[24,53,65]) ).
cnf(103,plain,
aElement0(xk),
inference('HYPERRESOLVE',[status(thm)],[24,53,70]) ).
cnf(104,plain,
aElement0(xm),
inference('HYPERRESOLVE',[status(thm)],[24,53,73]) ).
cnf(105,plain,
aElement0(sdtpldt0(xl,xn)),
inference('HYPERRESOLVE',[status(thm)],[24,57,77]) ).
cnf(2476,plain,
aElement0(xy),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[4,102,98]),67,theory(equality)]) ).
cnf(4478,plain,
xy = sdtpldt0(xn,xm),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[6,104,100]),75,theory(equality)]) ).
cnf(4613,plain,
sdtpldt0(sdtpldt0(xm,xl),xn) = sdtpldt0(xm,sdtpldt0(xl,xn)),
inference('HYPERRESOLVE',[status(thm)],[7,104,99,100]) ).
cnf(5005,plain,
sdtpldt0(sdtpldt0(xl,xn),xm) = sdtpldt0(xl,xy),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[7,104,99,100]),4478,theory(equality)]) ).
cnf(8192,plain,
sdtpldt0(xx,xy) = sdtpldt0(xk,sdtpldt0(xl,xy)),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[7,2476,103,99]),72,theory(equality)]) ).
cnf(14803,plain,
sdtpldt0(xl,xy) = sdtpldt0(sdtpldt0(xm,xl),xn),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[6,105,104]),4613,5005,theory(equality)]) ).
cnf(14804,plain,
sdtpldt0(xl,xy) = sdtpldt0(xm,sdtpldt0(xl,xn)),
inference('REWRITE',[status(thm)],[4613,14803,theory(equality)]) ).
cnf(15402,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[7,105,103,104]),80,8192,14804,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG090+2 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon May 30 13:49:40 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.20/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.47 *
% 0.20/0.47 *
% 0.20/0.47 #<PACKAGE "SNARK-USER">
% 0.20/0.47 *
% 0.20/0.47 SNARK-TPTP-OPTIONS
% 0.20/0.47 *
% 0.20/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.47 (USE-FACTORING :POS)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.47 *
% 0.20/0.47 "."
% 0.20/0.47 *
% 0.20/0.48 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-05-30T13:49:40
% 0.20/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n026.cluster.edu at 2022-05-30T13:49:40
% 3.27/3.48
% 3.27/3.48
% 3.27/3.48 #||
% 3.27/3.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.27/3.48 % SZS output start Refutation
% See solution above
% 3.27/3.48 ||#
% 3.27/3.48
% 3.27/3.48 ; Summary of computation:
% 3.27/3.48 ; 41847 formulas have been input or derived (from 96 formulas).
% 3.27/3.48 ; 15402 (37%) were retained. Of these,
% 3.27/3.48 ; 1624 (11%) were simplified or subsumed later,
% 3.27/3.48 ; 13778 (89%) are still being kept.
% 3.27/3.48 ;
% 3.27/3.48 ; Run time in seconds excluding printing time:
% 3.27/3.48 ; 0.008 0% Read assertion file (1 call)
% 3.27/3.48 ; 0.002 0% Assert (31 calls)
% 3.27/3.48 ; 1.095 36% Process new row (36,319 calls)
% 3.27/3.48 ; 0.764 25% Resolution (190 calls)
% 3.27/3.48 ; 0.000 0% Paramodulation (95 calls)
% 3.27/3.48 ; 0.002 0% Condensing (103 calls)
% 3.27/3.48 ; 0.001 0% Forward subsumption (103 calls)
% 3.27/3.48 ; 0.001 0% Backward subsumption (97 calls)
% 3.27/3.48 ; 0.001 0% Clause clause subsumption (70 calls)
% 3.27/3.48 ; 0.748 25% Forward simplification (36,319 calls)
% 3.27/3.48 ; 0.187 6% Backward simplification (15,402 calls)
% 3.27/3.48 ; 0.058 2% Ordering (14,433 calls)
% 3.27/3.48 ; 0.001 0% Sortal reasoning (32 calls)
% 3.27/3.48 ; 0.001 0% Purity testing (1 call)
% 3.27/3.48 ; 0.137 5% Other
% 3.27/3.48 ; 3.006 Total
% 3.27/3.48 ; 3.008 Real time
% 3.27/3.48 ;
% 3.27/3.48 ; Term-hash-array has 38,509 terms in all.
% 3.27/3.48 ; Feature-vector-row-index has 95 entries (95 at peak, 97 added, 2 deleted).
% 3.27/3.48 ; Feature-vector-row-index has 409 nodes (409 at peak, 409 added, 0 deleted).
% 3.27/3.48 ; Retrieved 54 possibly forward subsuming rows in 103 calls.
% 3.27/3.48 ; Retrieved 23 possibly backward subsumed rows in 97 calls.
% 3.27/3.48 ; Path-index has 35,675 entries (35,675 at peak, 39,726 added, 4,051 deleted).
% 3.27/3.49 ; Path-index has 1,872 nodes (1,872 at peak, 1,952 added, 80 deleted).
% 3.27/3.49 ; Trie-index has 35,675 entries (35,675 at peak, 39,726 added, 4,051 deleted).
% 3.27/3.49 ; Trie-index has 113,714 nodes (113,714 at peak, 128,875 added, 15,161 deleted).
% 3.27/3.49 ; Retrieved 49,262 generalization terms in 226,674 calls.
% 3.27/3.49 ; Retrieved 15,306 instance terms in 15,304 calls.
% 3.27/3.49 ; Retrieved 957,877 unifiable terms in 31,467 calls.
% 3.27/3.49 ;
% 3.27/3.49 ; The agenda of rows to process has 5504 entries:
% 3.27/3.49 ; 812 with value 21 972 with value 25 204 with value 29
% 3.27/3.49 ; 576 with value 22 448 with value 26 48 with value 30
% 3.27/3.49 ; 1496 with value 23 344 with value 27 32 with value 31
% 3.27/3.49 ; 480 with value 24 80 with value 28 12 with value 33
% 3.27/3.49 ; The agenda of rows to give has 13682 entries:
% 3.27/3.49 ; 23 with value (4 7) 509 with value (4 15) 142 with value (4 23)
% 3.27/3.49 ; 218 with value (4 8) 2153 with value (4 16) 106 with value (4 24)
% 3.27/3.49 ; 248 with value (4 9) 1889 with value (4 17) 25 with value (4 25)
% 3.27/3.49 ; 136 with value (4 10) 1390 with value (4 18) 4 with value (4 26)
% 3.27/3.49 ; 235 with value (4 11) 2531 with value (4 19) 1 with value (4 27)
% 3.27/3.49 ; 473 with value (4 12) 698 with value (4 20) 4 with value (4 30)
% 3.27/3.49 ; 324 with value (4 13) 995 with value (4 21) 8 with value (4 33)
% 3.27/3.49 ; 1052 with value (4 14) 514 with value (4 22) 4 with value (4 41)
% 3.27/3.49 Evaluation took:
% 3.27/3.49 3.01 seconds of real time
% 3.27/3.49 2.739576 seconds of user run time
% 3.27/3.49 0.270681 seconds of system run time
% 3.27/3.49 [Run times include 0.572 seconds GC run time.]
% 3.27/3.49 0 calls to %EVAL
% 3.27/3.49 0 page faults and
% 3.27/3.49 249,327,920 bytes consed.
% 3.27/3.49 :PROOF-FOUND
% 3.27/3.49 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-05-30T13:49:43
% 3.27/3.49 :PROOF-FOUND
% 3.27/3.49 *
%------------------------------------------------------------------------------