%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWW625_2 : TPTP v8.1.0. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n017.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 : Thu Jul 21 01:25:30 EDT 2022
% Result : Theorem 0.61s 0.79s
% Output : Refutation 0.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 11
% Syntax : Number of formulae : 21 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 206 ( 6 equ)
% Maximal formula atoms : 4 ( 9 avg)
% Number of connectives : 38 ( 18 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 165 ( 165 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 8 prp; 0-3 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 32 ( 0 sgn 32 !; 0 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
tff(41,axiom,
! [X: ty,Y: uni] : ( infix_plpl(X,Y,nil(X)) = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',append_l_nil) ).
tff(64,axiom,
! [X: ty,Y: uni] : ( reverse(X,reverse(X,Y)) = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reverse_reverse) ).
tff(113,axiom,
! [X: ty,Y: uni,Z: uni,U: uni] : ( rev_append(X,Y,infix_plpl(X,Z,U)) = rev_append(X,rev_append(X,Z,Y),U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rev_append_append_r) ).
tff(115,axiom,
! [X: ty,Y: uni,Z: uni] : ( rev_append(X,Y,Z) = infix_plpl(X,reverse(X,Y),Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rev_append_def1) ).
tff(118,axiom,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| mem(elt1,t2tb1('SKOLEMAAAV12.elt'(X,Y)),t2tb(X))
| sorted(tb2t(reverse(elt1,rev_append(elt1,t2tb(Y),t2tb(X))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_rev_append) ).
tff(119,plain,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| mem(elt1,t2tb1('SKOLEMAAAV12.elt'(X,Y)),t2tb(X))
| sorted(tb2t(reverse(elt1,infix_plpl(elt1,reverse(elt1,t2tb(Y)),t2tb(X))))) ),
inference('REWRITE',[status(thm)],[118,115,theory(equality)]) ).
tff(120,axiom,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| mem(elt1,t2tb1('SKOLEMAAAV13.elt'(X,Y)),t2tb(Y))
| sorted(tb2t(reverse(elt1,rev_append(elt1,t2tb(Y),t2tb(X))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_rev_append) ).
tff(121,plain,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| mem(elt1,t2tb1('SKOLEMAAAV13.elt'(X,Y)),t2tb(Y))
| sorted(tb2t(reverse(elt1,infix_plpl(elt1,reverse(elt1,t2tb(Y)),t2tb(X))))) ),
inference('REWRITE',[status(thm)],[120,115,theory(equality)]) ).
tff(122,axiom,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| ~ le('SKOLEMAAAV12.elt'(X,Y),'SKOLEMAAAV13.elt'(X,Y))
| sorted(tb2t(reverse(elt1,rev_append(elt1,t2tb(Y),t2tb(X))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_rev_append) ).
tff(123,plain,
! [X: list_elt,Y: list_elt] :
( ~ sorted(tb2t(reverse(elt1,t2tb(X))))
| ~ sorted(Y)
| ~ le('SKOLEMAAAV12.elt'(X,Y),'SKOLEMAAAV13.elt'(X,Y))
| sorted(tb2t(reverse(elt1,infix_plpl(elt1,reverse(elt1,t2tb(Y)),t2tb(X))))) ),
inference('REWRITE',[status(thm)],[122,115,theory(equality)]) ).
tff(126,negated_conjecture,
sorted('SKOLEMAAAV16.list_elt'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_rev_merge_rev) ).
tff(128,negated_conjecture,
sorted(tb2t(reverse(elt1,t2tb('SKOLEMAAAV15.list_elt')))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_rev_merge_rev) ).
tff(130,negated_conjecture,
! [X: elt,Y: elt] :
( ~ mem(elt1,t2tb1(X),t2tb('SKOLEMAAAV16.list_elt'))
| ~ mem(elt1,t2tb1(Y),t2tb('SKOLEMAAAV15.list_elt'))
| le(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_rev_merge_rev) ).
tff(133,negated_conjecture,
~ sorted(tb2t(rev_append(elt1,t2tb('SKOLEMAAAV15.list_elt'),t2tb('SKOLEMAAAV16.list_elt')))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_rev_merge_rev) ).
tff(134,plain,
~ sorted(tb2t(infix_plpl(elt1,reverse(elt1,t2tb('SKOLEMAAAV15.list_elt')),t2tb('SKOLEMAAAV16.list_elt')))),
inference('REWRITE',[status(thm)],[133,115,theory(equality)]) ).
tff(139,plain,
! [X: ty,Y: uni,Z: uni,U: uni] : ( infix_plpl(X,reverse(X,Y),infix_plpl(X,Z,U)) = infix_plpl(X,reverse(X,infix_plpl(X,reverse(X,Z),Y)),U) ),
inference('REWRITE',[status(thm)],[113,115,theory(equality)]) ).
tff(377,plain,
! [X: ty,Y: uni,Z: uni] : ( infix_plpl(X,reverse(X,Y),Z) = reverse(X,infix_plpl(X,reverse(X,Z),Y)) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[41,139,theory(equality)]),41,theory(equality)]) ).
tff(485,plain,
mem(elt1,t2tb1('SKOLEMAAAV12.elt'('SKOLEMAAAV15.list_elt','SKOLEMAAAV16.list_elt')),t2tb('SKOLEMAAAV15.list_elt')),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[119,128,126]),134,64,377,theory(equality)]) ).
tff(489,plain,
mem(elt1,t2tb1('SKOLEMAAAV13.elt'('SKOLEMAAAV15.list_elt','SKOLEMAAAV16.list_elt')),t2tb('SKOLEMAAAV16.list_elt')),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[121,128,126]),134,64,377,theory(equality)]) ).
tff(610,plain,
le('SKOLEMAAAV12.elt'('SKOLEMAAAV15.list_elt','SKOLEMAAAV16.list_elt'),'SKOLEMAAAV13.elt'('SKOLEMAAAV15.list_elt','SKOLEMAAAV16.list_elt')),
inference('HYPERRESOLVE',[status(thm)],[130,489,485]) ).
cnf(627,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[123,610,128,126]),134,64,377,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWW625_2 : TPTP v8.1.0. Released v6.1.0.
% 0.03/0.14 % Command : run-snark %s %d
% 0.13/0.35 % Computer : n017.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 : 600
% 0.13/0.35 % DateTime : Mon Jun 6 03:18:16 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.21/0.47 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.48 *
% 0.21/0.48 *
% 0.21/0.49 #<PACKAGE "SNARK-USER">
% 0.21/0.49 *
% 0.21/0.49 SNARK-TPTP-OPTIONS
% 0.21/0.49 *
% 0.21/0.49 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.49 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.49 (USE-FACTORING :POS)
% 0.21/0.49 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.49 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.49 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.49 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.49 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.49 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.49 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.49 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.49 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.49 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.49 *
% 0.21/0.49 "."
% 0.21/0.49 *
% 0.21/0.49 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-06T03:18:16
% 0.21/0.49 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n017.cluster.edu at 2022-06-06T03:18:16
% 0.21/0.53 WARNING: Cannot use equality or equivalence (= ?X.tuple0 tuple02) as rewrite.
% 0.61/0.79
% 0.61/0.79
% 0.61/0.79 #||
% 0.61/0.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.61/0.79 % SZS output start Refutation
% See solution above
% 0.61/0.79 ||#
% 0.61/0.79
% 0.61/0.79 ; Summary of computation:
% 0.61/0.79 ; 1690 formulas have been input or derived (from 147 formulas).
% 0.61/0.79 ; 627 (37%) were retained. Of these,
% 0.61/0.79 ; 42 ( 7%) were simplified or subsumed later,
% 0.61/0.79 ; 585 (93%) are still being kept.
% 0.61/0.79 ;
% 0.61/0.79 ; Run time in seconds excluding printing time:
% 0.61/0.79 ; 0.028 9% Read assertion file (1 call)
% 0.61/0.79 ; 0.005 2% Assert (79 calls)
% 0.61/0.79 ; 0.069 23% Process new row (1,528 calls)
% 0.61/0.79 ; 0.037 12% Resolution (292 calls)
% 0.61/0.79 ; 0.009 3% Paramodulation (146 calls)
% 0.61/0.79 ; 0.000 0% Factoring (8 calls)
% 0.61/0.79 ; 0.005 2% Condensing (284 calls)
% 0.61/0.79 ; 0.010 3% Forward subsumption (284 calls)
% 0.61/0.79 ; 0.006 2% Backward subsumption (239 calls)
% 0.61/0.79 ; 0.001 0% Clause clause subsumption (301 calls)
% 0.61/0.79 ; 0.064 21% Forward simplification (1,513 calls)
% 0.61/0.79 ; 0.005 2% Backward simplification (621 calls)
% 0.61/0.79 ; 0.024 8% Ordering (3,332 calls)
% 0.61/0.79 ; 0.000 0% Ordering ac (8 calls)
% 0.61/0.79 ; 0.005 2% Sortal reasoning (3,928 calls)
% 0.61/0.79 ; 0.001 0% Purity testing (1 call)
% 0.61/0.79 ; 0.034 11% Other
% 0.61/0.79 ; 0.303 Total
% 0.61/0.79 ; 0.306 Real time
% 0.61/0.79 ;
% 0.61/0.80 ; Term-hash-array has 1,782 terms in all.
% 0.61/0.80 ; Feature-vector-row-index has 222 entries (222 at peak, 239 added, 17 deleted).
% 0.61/0.80 ; Feature-vector-row-index has 1,944 nodes (1,944 at peak, 2,136 added, 192 deleted).
% 0.61/0.80 ; Retrieved 281 possibly forward subsuming rows in 284 calls.
% 0.61/0.80 ; Retrieved 53 possibly backward subsumed rows in 239 calls.
% 0.61/0.80 ; Path-index has 1,727 entries (1,727 at peak, 1,823 added, 96 deleted).
% 0.61/0.80 ; Path-index has 6,159 nodes (6,159 at peak, 6,304 added, 145 deleted).
% 0.61/0.80 ; Trie-index has 1,727 entries (1,727 at peak, 1,823 added, 96 deleted).
% 0.61/0.80 ; Trie-index has 8,009 nodes (8,009 at peak, 8,315 added, 306 deleted).
% 0.61/0.80 ; Retrieved 6,255 generalization terms in 9,367 calls.
% 0.61/0.80 ; Retrieved 866 instance terms in 501 calls.
% 0.61/0.80 ; Retrieved 23,525 unifiable terms in 2,555 calls.
% 0.61/0.80 ;
% 0.61/0.80 ; The agenda of rows to give has 454 entries:
% 0.61/0.80 ; 1 with value (4 11) 34 with value (4 27) 2 with value (4 43)
% 0.61/0.80 ; 3 with value (4 12) 18 with value (4 28) 5 with value (4 44)
% 0.61/0.80 ; 15 with value (4 13) 4 with value (4 29) 1 with value (4 45)
% 0.61/0.80 ; 10 with value (4 14) 21 with value (4 30) 3 with value (4 47)
% 0.61/0.80 ; 18 with value (4 15) 13 with value (4 31) 4 with value (4 48)
% 0.61/0.80 ; 12 with value (4 16) 11 with value (4 32) 2 with value (4 49)
% 0.61/0.80 ; 23 with value (4 17) 24 with value (4 33) 1 with value (4 51)
% 0.61/0.80 ; 9 with value (4 18) 29 with value (4 34) 1 with value (4 52)
% 0.61/0.80 ; 13 with value (4 19) 22 with value (4 35) 1 with value (4 53)
% 0.61/0.80 ; 18 with value (4 20) 17 with value (4 36) 2 with value (4 54)
% 0.61/0.80 ; 14 with value (4 21) 6 with value (4 37) 1 with value (4 56)
% 0.61/0.80 ; 11 with value (4 22) 2 with value (4 38) 1 with value (4 64)
% 0.61/0.80 ; 11 with value (4 23) 6 with value (4 39) 1 with value (4 66)
% 0.61/0.80 ; 10 with value (4 24) 7 with value (4 40) 1 with value (4 74)
% 0.61/0.80 ; 15 with value (4 25) 8 with value (4 41) 1 with value (4 79)
% 0.61/0.80 ; 13 with value (4 26) 8 with value (4 42) 1 with value (4 93)
% 0.61/0.80 Evaluation took:
% 0.61/0.80 0.307 seconds of real time
% 0.61/0.80 0.271752 seconds of user run time
% 0.61/0.80 0.035249 seconds of system run time
% 0.61/0.80 [Run times include 0.01 seconds GC run time.]
% 0.61/0.80 0 calls to %EVAL
% 0.61/0.80 0 page faults and
% 0.61/0.80 20,458,920 bytes consed.
% 0.61/0.80 :PROOF-FOUND
% 0.61/0.80 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-06T03:18:16
% 0.61/0.80 :PROOF-FOUND
% 0.61/0.80 *
%------------------------------------------------------------------------------