%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KRS292_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n029.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 06:43:34 PM UTC 2026
% Result : Theorem 1.32s 1.60s
% Output : Refutation 1.43s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 'CODE-FOR-$$SUM')
% Comments :
%------------------------------------------------------------------------------
tff(1,axiom,
! [X: binary_relation,Y: thing,Z: thing,U: $int,V: binary_relation,W: thing,X1: $int] :
( ~ binary_relation_with_confidence(X,Y,Z,U)
| ~ binary_relation_with_confidence(V,Z,W,X1)
| binary_relation_with_confidence(compose_binary_binary(X,V),Y,W,$sum(U,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
tff(4,axiom,
! [X: binary_relation,Y: thing,Z: thing,U: $int] :
( ~ binary_relation_with_confidence(X,Y,Z,U)
| binary_relation_with_confidence(inverse(X),Z,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(18,axiom,
! [X: binary_relation,Y: thing,Z: thing,U: $int,V: $int] :
( ~ binary_relation_with_confidence(X,Y,Z,U)
| ~ $greatereq(V,U)
| binary_relation_with_confidence(X,Y,Z,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(20,axiom,
! [X: thing,Y: thing,Z: $int,U: thing,V: $int] :
( ~ binary_relation_with_confidence(livesin,X,Y,Z)
| ~ binary_relation_with_confidence(partof,Y,U,V)
| binary_relation_with_confidence(livesin,X,U,$sum(Z,V)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
tff(22,axiom,
binary_relation_with_confidence(livesin,john,newyork,1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
tff(23,axiom,
binary_relation_with_confidence(livesin,mary,chicago,2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
tff(28,axiom,
binary_relation_with_confidence(partof,newyork,usa,0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
tff(29,axiom,
binary_relation_with_confidence(partof,chicago,usa,0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
tff(40,negated_conjecture,
! [X: binary_relation] : ~ binary_relation_with_confidence(X,john,mary,4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(41,plain,
! [X: binary_relation] : ~ binary_relation_with_confidence(X,mary,john,4),
inference('UR-RESOLVE',[status(thm)],[4,40]) ).
tff(83,plain,
binary_relation_with_confidence(livesin,john,usa,1),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[20,22,28]),'CODE-FOR-$$SUM']) ).
tff(84,plain,
binary_relation_with_confidence(livesin,mary,usa,2),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[20,23,29]),'CODE-FOR-$$SUM']) ).
tff(95,plain,
binary_relation_with_confidence(inverse(livesin),usa,john,1),
inference('HYPERRESOLVE',[status(thm)],[4,83]) ).
tff(415,plain,
binary_relation_with_confidence(compose_binary_binary(livesin,inverse(livesin)),mary,john,3),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[1,95,84]),'CODE-FOR-$$SUM']) ).
cnf(5577,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[18,415,41]),'CODE-FOR-$$GREATEREQ']) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : KRS292_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run-snark %s %d
% 0.16/0.33 % Computer : n029.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 03:35:59 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.18/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.46 *
% 0.29/0.46 *
% 0.29/0.46 #<PACKAGE "SNARK-USER">
% 0.29/0.46 *
% 0.29/0.46 SNARK-TPTP-OPTIONS
% 0.29/0.46 *
% 0.29/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.29/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.29/0.46 (USE-FACTORING :POS)
% 0.29/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.29/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.29/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.29/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.29/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.29/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.29/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.29/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.29/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.29/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.29/0.46 *
% 0.29/0.46 "."
% 0.29/0.46 *
% 0.29/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2026-05-05T03:35:59
% 0.29/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n029.cluster.edu at 2026-05-05T03:35:59
% 1.32/1.60
% 1.32/1.60
% 1.32/1.60 #||
% 1.32/1.60 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.32/1.60 % SZS output start Refutation
% See solution above
% 1.43/1.60 ||#
% 1.43/1.60
% 1.43/1.60 ; Summary of computation:
% 1.43/1.60 ; 12195 formulas have been input or derived (from 338 formulas).
% 1.43/1.60 ; 5577 (46%) were retained. Of these,
% 1.43/1.60 ; 5577 (100%) are still being kept.
% 1.43/1.60 ;
% 1.43/1.60 ; Run time in seconds excluding printing time:
% 1.43/1.60 ; 0.008 1% Read assertion file (1 call)
% 1.43/1.60 ; 0.001 0% Assert (28 calls)
% 1.43/1.60 ; 0.349 31% Process new row (11,661 calls)
% 1.43/1.60 ; 0.215 19% Resolution (674 calls)
% 1.43/1.60 ; 0.002 0% Paramodulation (337 calls)
% 1.43/1.60 ; 0.000 0% Factoring (61 calls)
% 1.43/1.60 ; 0.025 2% Condensing (2,614 calls)
% 1.43/1.60 ; 0.128 11% Forward subsumption (2,614 calls)
% 1.43/1.60 ; 0.074 7% Backward subsumption (1,874 calls)
% 1.43/1.60 ; 0.008 1% Clause clause subsumption (1,752 calls)
% 1.43/1.60 ; 0.205 18% Forward simplification (11,661 calls)
% 1.43/1.60 ; 0.020 2% Backward simplification (5,577 calls)
% 1.43/1.60 ; 0.000 0% Ordering (7 calls)
% 1.43/1.60 ; 0.041 4% Sortal reasoning (42,375 calls)
% 1.43/1.60 ; 0.000 0% Purity testing (1 call)
% 1.43/1.60 ; 0.056 5% Other
% 1.43/1.60 ; 1.132 Total
% 1.43/1.60 ; 1.133 Real time
% 1.43/1.60 ;
% 1.43/1.60 ; Term-hash-array has 6,401 terms in all.
% 1.43/1.60 ; Feature-vector-row-index has 1,874 entries (1,874 at peak, 1,874 added, 0 deleted).
% 1.43/1.60 ; Feature-vector-row-index has 13,356 nodes (13,356 at peak, 13,356 added, 0 deleted).
% 1.43/1.60 ; Retrieved 2,008 possibly forward subsuming rows in 2,614 calls.
% 1.43/1.60 ; Retrieved 228 possibly backward subsumed rows in 1,874 calls.
% 1.43/1.60 ; Path-index has 6,425 entries (6,425 at peak, 6,425 added, 0 deleted).
% 1.43/1.60 ; Path-index has 788 nodes (788 at peak, 788 added, 0 deleted).
% 1.43/1.60 ; Trie-index has 6,425 entries (6,425 at peak, 6,425 added, 0 deleted).
% 1.43/1.60 ; Trie-index has 13,327 nodes (13,327 at peak, 13,327 added, 0 deleted).
% 1.43/1.60 ; Retrieved 5,377 generalization terms in 30,979 calls.
% 1.43/1.60 ; Retrieved 3,702 instance terms in 3,702 calls.
% 1.43/1.60 ; Retrieved 151,177 unifiable terms in 10,594 calls.
% 1.43/1.60 ;
% 1.43/1.60 ; The agenda of rows to process has 101 entries:
% 1.43/1.60 ; 1 with value 15 6 with value 20 38 with value 23
% 1.43/1.60 ; 1 with value 17 18 with value 21 17 with value 24
% 1.43/1.60 ; 5 with value 19 12 with value 22 3 with value 25
% 1.43/1.60 ; The agenda of rows to give has 5239 entries:
% 1.43/1.60 ; 50 with value (4 14) 675 with value (4 18) 545 with value (4 22)
% 1.43/1.60 ; 126 with value (4 15) 714 with value (4 19) 238 with value (4 23)
% 1.43/1.60 ; 244 with value (4 16) 901 with value (4 20) 263 with value (4 24)
% 1.43/1.60 ; 470 with value (4 17) 860 with value (4 21) 153 with value (4 25)
% 1.43/1.60 Evaluation took:
% 1.43/1.60 1.135 seconds of real time
% 1.43/1.60 0.988632 seconds of user run time
% 1.43/1.60 0.146211 seconds of system run time
% 1.43/1.60 [Run times include 0.101 seconds GC run time.]
% 1.43/1.60 0 calls to %EVAL
% 1.43/1.60 0 page faults and
% 1.43/1.60 83,928,464 bytes consed.
% 1.43/1.60 :PROOF-FOUND
% 1.43/1.60 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2026-05-05T03:36:00
% 1.43/1.60 :PROOF-FOUND
% 1.43/1.60 *
%------------------------------------------------------------------------------