%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWC539_1 : TPTP v9.0.0. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n012.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 Apr 1 02:08:20 AM UTC 2025
% Result : Theorem 0.85s 1.05s
% Output : Refutation 0.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of formulae : 25 ( 4 unt; 0 typ; 0 def)
% Number of atoms : 156 ( 11 equ)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 37 ( 12 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 106 ( 106 fml; 0 var)
% Number arithmetic : 5 ( 0 atm; 0 fun; 0 num; 5 var)
% Number of types : 1 ( 0 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-3 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 5 ( 0 sgn 5 !; 0 ?; 5 :)
% Comments :
%------------------------------------------------------------------------------
tff(525,axiom,
! [X: $int,Y: $int] :
( mem2(X,Y,'SKOLEMAAAW181.set_2')
| ~ mem2(X,Y,g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:imprp:14') ).
tff(526,axiom,
! [X: $int,Y: $int,Z: $int] :
( ~ mem2(X,Y,'SKOLEMAAAW181.set_2')
| ~ mem2(X,Z,'SKOLEMAAAW181.set_2')
| ( Y = Z ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:imprp:14') ).
tff(604,negated_conjecture,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(607,negated_conjecture,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(609,negated_conjecture,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| ( 'SKOLEMAAAW209.$int' != 'SKOLEMAAAW210.$int' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(610,negated_conjecture,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(613,negated_conjecture,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(615,negated_conjecture,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| ( 'SKOLEMAAAW209.$int' != 'SKOLEMAAAW210.$int' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(616,negated_conjecture,
( ~ mem0('SKOLEMAAAW207.$int',g_s66_66)
| ~ mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(619,negated_conjecture,
( ~ mem0('SKOLEMAAAW207.$int',g_s66_66)
| ~ mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int',g_s104_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(621,negated_conjecture,
( ~ mem0('SKOLEMAAAW207.$int',g_s66_66)
| ~ mem0('SKOLEMAAAW206.$int',g_s37_37)
| ( 'SKOLEMAAAW209.$int' != 'SKOLEMAAAW210.$int' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(658,plain,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,610]) ).
tff(659,plain,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,604]) ).
tff(660,plain,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,613]) ).
tff(661,plain,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,607]) ).
tff(2102,plain,
( mem0('SKOLEMAAAW206.$int',g_s37_37)
| ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' ) ),
inference('HYPERRESOLVE',[status(thm)],[526,660,658]) ).
tff(2103,plain,
( mem0('SKOLEMAAAW207.$int',g_s66_66)
| ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' ) ),
inference('HYPERRESOLVE',[status(thm)],[526,661,659]) ).
tff(2133,plain,
( ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' )
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int',g_s104_89) ),
inference('HYPERRESOLVE',[status(thm)],[619,2103,2102]) ).
tff(2134,plain,
( ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' )
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int',g_s104_89) ),
inference('HYPERRESOLVE',[status(thm)],[616,2103,2102]) ).
tff(2337,plain,
( ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' )
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW210.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,2133]) ).
tff(2338,plain,
( ( 'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int' )
| mem2('SKOLEMAAAW208.$int','SKOLEMAAAW209.$int','SKOLEMAAAW181.set_2') ),
inference('HYPERRESOLVE',[status(thm)],[525,2134]) ).
tff(2720,plain,
'SKOLEMAAAW209.$int' = 'SKOLEMAAAW210.$int',
inference('HYPERRESOLVE',[status(thm)],[526,2338,2337]) ).
tff(2722,plain,
mem0('SKOLEMAAAW207.$int',g_s66_66),
inference('REWRITE',[status(thm)],[609,2720,theory(equality)]) ).
tff(2726,plain,
mem0('SKOLEMAAAW206.$int',g_s37_37),
inference('REWRITE',[status(thm)],[615,2720,theory(equality)]) ).
cnf(2730,plain,
$false,
inference('REWRITE',[status(thm)],[621,2726,2722,2720,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWC539_1 : TPTP v9.0.0. Bugfixed v9.1.0.
% 0.12/0.13 % Command : run-snark %s %d
% 0.14/0.34 % Computer : n012.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Mar 31 13:41:19 EDT 2025
% 0.14/0.34 % CPUTime :
% 0.21/0.46 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.47 *
% 0.21/0.47 *
% 0.21/0.48 #<PACKAGE "SNARK-USER">
% 0.21/0.48 *
% 0.21/0.48 SNARK-TPTP-OPTIONS
% 0.21/0.48 *
% 0.21/0.48 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.48 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.48 (USE-FACTORING :POS)
% 0.21/0.48 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.48 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.48 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.48 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.48 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.48 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.48 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.48 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.48 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.48 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.48 *
% 0.21/0.48 "."
% 0.21/0.48 *
% 0.21/0.48 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2025-03-31T13:41:19
% 0.21/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n012.cluster.edu at 2025-03-31T13:41:19
% 0.85/1.05
% 0.85/1.05
% 0.85/1.05 #||
% 0.85/1.05 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.85/1.05 % SZS output start Refutation
% See solution above
% 0.85/1.05 ||#
% 0.85/1.05
% 0.85/1.05 ; Summary of computation:
% 0.85/1.05 ; 5227 formulas have been input or derived (from 1320 formulas).
% 0.85/1.05 ; 2730 (52%) were retained. Of these,
% 0.85/1.05 ; 311 (11%) were simplified or subsumed later,
% 0.85/1.05 ; 2419 (89%) are still being kept.
% 0.85/1.05 ;
% 0.85/1.05 ; Run time in seconds excluding printing time:
% 0.85/1.05 ; 0.088 15% Read assertion file (1 call)
% 0.85/1.05 ; 0.016 3% Assert (140 calls)
% 0.85/1.05 ; 0.155 27% Process new row (4,561 calls)
% 0.85/1.05 ; 0.074 13% Resolution (2,638 calls)
% 0.85/1.05 ; 0.005 1% Paramodulation (1,319 calls)
% 0.85/1.05 ; 0.000 0% Factoring (363 calls)
% 0.85/1.05 ; 0.010 2% Condensing (2,755 calls)
% 0.85/1.05 ; 0.062 11% Forward subsumption (2,755 calls)
% 0.85/1.05 ; 0.044 8% Backward subsumption (2,248 calls)
% 0.85/1.05 ; 0.003 1% Clause clause subsumption (719 calls)
% 0.85/1.05 ; 0.048 8% Forward simplification (4,561 calls)
% 0.85/1.05 ; 0.012 2% Backward simplification (2,712 calls)
% 0.85/1.05 ; 0.000 0% Ordering (921 calls)
% 0.85/1.06 ; 0.004 1% Sortal reasoning (3,317 calls)
% 0.85/1.06 ; 0.001 0% Purity testing (1 call)
% 0.85/1.06 ; 0.052 9% Other
% 0.85/1.06 ; 0.574 Total
% 0.85/1.06 ; 0.576 Real time
% 0.85/1.06 ;
% 0.85/1.06 ; Term-hash-array has 4,620 terms in all.
% 0.85/1.06 ; Feature-vector-row-index has 1,955 entries (2,215 at peak, 2,248 added, 293 deleted).
% 0.85/1.06 ; Feature-vector-row-index has 2,394 nodes (3,187 at peak, 3,426 added, 1,032 deleted).
% 0.85/1.06 ; Retrieved 8,771 possibly forward subsuming rows in 2,755 calls.
% 0.85/1.06 ; Retrieved 6,765 possibly backward subsumed rows in 2,248 calls.
% 0.85/1.06 ; Path-index has 4,772 entries (4,839 at peak, 4,929 added, 157 deleted).
% 0.85/1.06 ; Path-index has 4,935 nodes (4,978 at peak, 5,068 added, 133 deleted).
% 0.85/1.06 ; Trie-index has 4,772 entries (4,839 at peak, 4,929 added, 157 deleted).
% 0.85/1.06 ; Trie-index has 10,085 nodes (10,196 at peak, 10,391 added, 306 deleted).
% 0.85/1.06 ; Retrieved 1,322 generalization terms in 6,669 calls.
% 0.85/1.06 ; Retrieved 463 instance terms in 463 calls.
% 0.85/1.06 ; Retrieved 21,578 unifiable terms in 11,193 calls.
% 0.85/1.06 ;
% 0.85/1.06 ; The agenda of backward simplifiable rows to process has 113 entries:
% 0.85/1.06 ; 113 with value 0
% 0.85/1.06 ; The agenda of rows to process has 20 entries:
% 0.85/1.06 ; 8 with value 13 4 with value 17 4 with value 19
% 0.85/1.06 ; 3 with value 14 1 with value 18
% 0.85/1.06 ; The agenda of input rows to give has 6 entries:
% 0.85/1.06 ; 4 with value 4 2 with value 5
% 0.85/1.06 ; The agenda of rows to give has 1224 entries:
% 0.85/1.06 ; 1 with value (4 9) 24 with value (4 15) 102 with value (4 17)
% 0.85/1.06 ; 58 with value (4 13) 44 with value (4 16) 930 with value (4 20)
% 0.85/1.06 ; 65 with value (4 14)
% 0.85/1.06 Evaluation took:
% 0.85/1.06 0.576 seconds of real time
% 0.85/1.06 0.514872 seconds of user run time
% 0.85/1.06 0.061811 seconds of system run time
% 0.85/1.06 [Run times include 0.037 seconds GC run time.]
% 0.85/1.06 0 calls to %EVAL
% 0.85/1.06 0 page faults and
% 0.85/1.06 43,297,040 bytes consed.
% 0.85/1.06 :PROOF-FOUND
% 0.85/1.06 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2025-03-31T13:41:20
% 0.85/1.06 :PROOF-FOUND
% 0.85/1.06 *
%------------------------------------------------------------------------------