%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : GEO528+1 : TPTP v8.1.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n013.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 : Sat Jul 16 06:16:34 EDT 2022
% Result : Theorem 131.25s 131.61s
% Output : Refutation 131.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 11
% Syntax : Number of clauses : 17 ( 11 unt; 5 nHn; 13 RR)
% Number of literals : 29 ( 12 equ; 9 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-3 aty)
% Number of variables : 24 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(163,axiom,
s_m(X,midpoint(X,Y),Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz8_22) ).
cnf(202,axiom,
( X = Y
| s_col(X,Y,midpoint(Z,reflect(X,Y,Z))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_2a) ).
cnf(207,axiom,
( X = Y
| reflect(X,Y,reflect(X,Y,Z)) = Z ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_5) ).
cnf(209,axiom,
( X = Y
| Z != reflect(X,Y,Z)
| s_col(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_8a) ).
cnf(210,axiom,
( X = Y
| ~ s_col(X,Y,Z)
| Z = reflect(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_8b) ).
cnf(217,negated_conjecture,
'SKOLEMAAAV1' != 'SKOLEMAAAV2',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_14) ).
cnf(218,negated_conjecture,
reflect('SKOLEMAAAV1','SKOLEMAAAV2','SKOLEMAAAV3') = 'SKOLEMAAAV4',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_14) ).
cnf(219,negated_conjecture,
~ s_col('SKOLEMAAAV1','SKOLEMAAAV2','SKOLEMAAAV3'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_14) ).
cnf(220,negated_conjecture,
~ opposite('SKOLEMAAAV3','SKOLEMAAAV1','SKOLEMAAAV2','SKOLEMAAAV4'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz10_14) ).
cnf(257,axiom,
( ~ s_m(X,Y,Z)
| s_t(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn7_1) ).
cnf(275,axiom,
( X = Y
| s_col(X,Y,Z)
| s_col(X,Y,U)
| ~ s_t(Z,V,U)
| ~ s_col(X,Y,V)
| opposite(Z,X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn9_1) ).
cnf(374,plain,
s_t(X,midpoint(X,Y),Y),
inference('HYPERRESOLVE',[status(thm)],[257,163]) ).
cnf(583,plain,
s_col('SKOLEMAAAV1','SKOLEMAAAV2',midpoint('SKOLEMAAAV3','SKOLEMAAAV4')),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[202,218,theory(equality)]),217]) ).
cnf(598,plain,
reflect('SKOLEMAAAV1','SKOLEMAAAV2','SKOLEMAAAV4') = 'SKOLEMAAAV3',
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[207,218,theory(equality)]),217]) ).
cnf(627,plain,
'SKOLEMAAAV3' != 'SKOLEMAAAV4',
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[209,217,219]),218,theory(equality)]) ).
cnf(10003,plain,
s_col('SKOLEMAAAV1','SKOLEMAAAV2','SKOLEMAAAV4'),
inference('UR-RESOLVE',[status(thm)],[275,583,217,219,374,220]) ).
cnf(10844,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[210,10003,217]),627,598,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO528+1 : TPTP v8.1.0. Released v7.0.0.
% 0.03/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n013.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 : Sat Jun 18 08:52:14 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.47 *
% 0.19/0.47 *
% 0.19/0.47 #<PACKAGE "SNARK-USER">
% 0.19/0.47 *
% 0.19/0.47 SNARK-TPTP-OPTIONS
% 0.19/0.47 *
% 0.19/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.47 (USE-FACTORING :POS)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.47 *
% 0.19/0.47 "."
% 0.19/0.47 *
% 0.19/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-18T08:52:14
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n013.cluster.edu at 2022-06-18T08:52:14
% 0.39/0.57
% 0.39/0.57 ; Recognized commutativity assertion (OR (NOT (|s_col| ?X ?Y ?Z)) (|s_col| ?Y ?X ?Z)).
% 0.39/0.58 ; Recognized relation functionality assertion (OR (NOT (|s_m| ?X ?Y ?Z)) (NOT (|s_m| ?X ?Y ?U)) (= ?Z ?U)).
% 131.25/131.61 ; Declaring s_col to be commutative.
% 131.25/131.61
% 131.25/131.61 #||
% 131.25/131.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 131.25/131.61 % SZS output start Refutation
% See solution above
% 131.25/131.61 ||#
% 131.25/131.61
% 131.25/131.61 ; Summary of computation:
% 131.25/131.61 ; 114040 formulas have been input or derived (from 504 formulas).
% 131.25/131.61 ; 10844 (10%) were retained. Of these,
% 131.25/131.61 ; 301 ( 3%) were simplified or subsumed later,
% 131.25/131.61 ; 10543 (97%) are still being kept.
% 131.25/131.61 ;
% 131.25/131.61 ; Run time in seconds excluding printing time:
% 131.25/131.61 ; 0.081 0% Read assertion file (1 call)
% 131.25/131.61 ; 0.011 0% Assert (213 calls)
% 131.25/131.61 ; 0.900 1% Process new row (78,509 calls)
% 131.25/131.61 ; 125.232 96% Resolution (1,006 calls)
% 131.25/131.61 ; 0.008 0% Paramodulation (503 calls)
% 131.25/131.61 ; 0.001 0% Factoring (19 calls)
% 131.25/131.61 ; 0.279 0% Condensing (14,420 calls)
% 131.25/131.61 ; 1.400 1% Forward subsumption (14,420 calls)
% 131.25/131.61 ; 0.156 0% Backward subsumption (3,708 calls)
% 131.25/131.61 ; 0.811 1% Clause clause subsumption (149,573 calls)
% 131.25/131.61 ; 1.729 1% Forward simplification (78,509 calls)
% 131.25/131.61 ; 0.100 0% Backward simplification (10,842 calls)
% 131.25/131.61 ; 0.025 0% Ordering (17,419 calls)
% 131.25/131.61 ; 0.000 0% Sortal reasoning (32 calls)
% 131.25/131.61 ; 0.000 0% Purity testing (1 call)
% 131.25/131.61 ; 0.264 0% Other
% 131.25/131.61 ; 130.997 Total
% 131.25/131.61 ; 131.135 Real time
% 131.25/131.61 ;
% 131.25/131.61 ; Term-hash-array has 16,912 terms in all.
% 131.25/131.61 ; Feature-vector-row-index has 3,633 entries (3,633 at peak, 3,708 added, 75 deleted).
% 131.25/131.61 ; Feature-vector-row-index has 7,344 nodes (7,344 at peak, 7,543 added, 199 deleted).
% 131.25/131.61 ; Retrieved 382,117 possibly forward subsuming rows in 14,420 calls.
% 131.25/131.61 ; Retrieved 20,261 possibly backward subsumed rows in 3,708 calls.
% 131.25/131.61 ; Path-index has 16,628 entries (16,628 at peak, 17,024 added, 396 deleted).
% 131.25/131.61 ; Path-index has 20,380 nodes (20,382 at peak, 20,628 added, 248 deleted).
% 131.25/131.61 ; Trie-index has 16,628 entries (16,628 at peak, 17,024 added, 396 deleted).
% 131.25/131.61 ; Trie-index has 75,308 nodes (75,308 at peak, 76,385 added, 1,077 deleted).
% 131.25/131.61 ; Retrieved 376,335 generalization terms in 329,011 calls.
% 131.25/131.61 ; Retrieved 12,819 instance terms in 7,133 calls.
% 131.25/131.61 ; Retrieved 202,016,089 unifiable terms in 1,908,861 calls.
% 131.25/131.61 ;
% 131.25/131.61 ; The agenda of rows to process has 14135 entries:
% 131.25/131.61 ; 117 with value 11 612 with value 32 12 with value 52
% 131.25/131.61 ; 268 with value 12 631 with value 33 54 with value 53
% 131.25/131.61 ; 36 with value 13 454 with value 34 94 with value 54
% 131.25/131.61 ; 50 with value 14 438 with value 35 10 with value 55
% 131.25/131.61 ; 30 with value 15 440 with value 36 50 with value 56
% 131.25/131.61 ; 487 with value 16 412 with value 37 46 with value 58
% 131.25/131.61 ; 30 with value 17 464 with value 38 160 with value 59
% 131.25/131.61 ; 40 with value 18 71 with value 39 20 with value 60
% 131.25/131.61 ; 177 with value 19 192 with value 40 4 with value 62
% 131.25/131.61 ; 702 with value 20 232 with value 41 40 with value 63
% 131.25/131.61 ; 41 with value 21 262 with value 42 24 with value 64
% 131.25/131.61 ; 271 with value 22 184 with value 43 24 with value 65
% 131.25/131.61 ; 630 with value 23 46 with value 44 8 with value 67
% 131.25/131.61 ; 573 with value 24 62 with value 45 16 with value 68
% 131.25/131.61 ; 956 with value 25 346 with value 46 16 with value 69
% 131.25/131.61 ; 360 with value 26 48 with value 47 8 with value 71
% 131.25/131.61 ; 557 with value 27 68 with value 48 56 with value 72
% 131.25/131.61 ; 365 with value 28 112 with value 49 8 with value 75
% 131.25/131.61 ; 1390 with value 29 36 with value 50 8 with value 77
% 131.25/131.61 ; 505 with value 30 264 with value 51 8 with value 81
% 131.25/131.61 ; 510 with value 31
% 131.25/131.61 ; The agenda of rows to give has 10041 entries:
% 131.25/131.61 ; 6 with value (4 8) 102 with value (4 34) 31 with value (4 59)
% 131.25/131.61 ; 191 with value (4 9) 92 with value (4 35) 10 with value (4 60)
% 131.25/131.61 ; 454 with value (4 10) 153 with value (4 36) 7 with value (4 61)
% 131.25/131.61 ; 408 with value (4 11) 207 with value (4 37) 26 with value (4 62)
% 131.25/131.61 ; 772 with value (4 12) 149 with value (4 38) 18 with value (4 63)
% 131.25/131.61 ; 777 with value (4 13) 117 with value (4 39) 15 with value (4 64)
% 131.25/131.61 ; 366 with value (4 14) 83 with value (4 40) 9 with value (4 65)
% 131.25/131.61 ; 428 with value (4 15) 115 with value (4 41) 5 with value (4 68)
% 131.25/131.61 ; 447 with value (4 16) 123 with value (4 42) 8 with value (4 69)
% 131.25/131.61 ; 318 with value (4 17) 76 with value (4 43) 4 with value (4 70)
% 131.25/131.61 ; 392 with value (4 18) 108 with value (4 44) 1 with value (4 72)
% 131.25/131.61 ; 491 with value (4 19) 68 with value (4 45) 2 with value (4 73)
% 131.25/131.61 ; 349 with value (4 20) 77 with value (4 46) 3 with value (4 74)
% 131.25/131.61 ; 246 with value (4 21) 115 with value (4 47) 5 with value (4 79)
% 131.25/131.61 ; 231 with value (4 22) 87 with value (4 48) 1 with value (4 91)
% 131.25/131.61 ; 167 with value (4 23) 32 with value (4 49) 4 with value (4 95)
% 131.25/131.61 ; 347 with value (4 24) 72 with value (4 50) 1 with value (4 97)
% 131.25/131.61 ; 171 with value (4 25) 40 with value (4 51) 3 with value (4 98)
% 131.25/131.61 ; 330 with value (4 26) 16 with value (4 52) 2 with value (4 99)
% 131.25/131.61 ; 147 with value (4 27) 72 with value (4 53) 1 with value (4 102)
% 131.25/131.61 ; 99 with value (4 28) 33 with value (4 54) 3 with value (4 103)
% 131.25/131.61 ; 123 with value (4 29) 30 with value (4 55) 1 with value (4 109)
% 131.25/131.61 ; 106 with value (4 30) 7 with value (4 56) 4 with value (4 110)
% 131.25/131.61 ; 149 with value (4 31) 15 with value (4 57) 4 with value (4 115)
% 131.25/131.61 ; 197 with value (4 32) 74 with value (4 58) 2 with value (4 123)
% 131.25/131.61 ; 96 with value (4 33)
% 131.25/131.61 Evaluation took:
% 131.25/131.61 131.137 seconds of real time
% 131.25/131.61 130.09184 seconds of user run time
% 131.25/131.61 0.909178 seconds of system run time
% 131.25/131.61 [Run times include 3.94 seconds GC run time.]
% 131.25/131.61 0 calls to %EVAL
% 131.25/131.61 0 page faults and
% 131.25/131.61 3,469,480,664 bytes consed.
% 131.25/131.61 :PROOF-FOUND
% 131.25/131.61 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-18T08:54:25
% 131.25/131.61 :PROOF-FOUND
% 131.25/131.61 *
%------------------------------------------------------------------------------