%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : HWV016-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n032.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 19:10:38 EDT 2022
% Result : Unsatisfiable 0.39s 0.56s
% Output : Refutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 23
% Syntax : Number of clauses : 47 ( 21 unt; 20 nHn; 42 RR)
% Number of literals : 98 ( 27 equ; 31 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 35 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_1,axiom,
plus(X,n1) != n0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
cnf(axiom_2,axiom,
gt(plus(X,n1),n0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
cnf(axiom_3,axiom,
( ~ gt(X,n0)
| gt(X,minus(X,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_3) ).
cnf(axiom_4,axiom,
( minus(X,Y) != Z
| plus(Z,Y) = X
| def_10(Y,X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_4) ).
cnf(axiom_6,axiom,
( ~ def_10(X,Y)
| ~ gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_6) ).
cnf(axiom_9,axiom,
( gt(X,Y)
| ~ gt(plus(X,n1),plus(Y,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_9) ).
cnf(axiom_12,axiom,
( gt(X,Y)
| Y = X
| gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
cnf(axiom_13,axiom,
( ~ gt(X,Y)
| gt(X,Z)
| ~ gt(Y,Z) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_13) ).
cnf(axiom_14,axiom,
( ~ gt(X,Y)
| plus(Y,n1) = X
| gt(X,plus(Y,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
cnf(axiom_15,axiom,
( X = n0
| gt(X,n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
cnf(axiom_17,axiom,
~ gt(X,X),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
cnf(axiom_19,axiom,
plus(n0,X) = X,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
cnf(axiom_25,axiom,
( int_level(X) = n0
| ~ p_Empty(X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_25) ).
cnf(axiom_34,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| p_Rd(X)
| ~ gt(fifo_length,int_level(X))
| ~ p_Wr_error(plus(X,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_34) ).
cnf(axiom_35,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| p_Rd(X)
| ~ gt(fifo_length,int_level(X))
| int_level(plus(X,n1)) = plus(int_level(X),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_35) ).
cnf(axiom_42,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| p_Rd(X)
| gt(fifo_length,int_level(X))
| p_Wr_error(plus(X,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_42) ).
cnf(axiom_44,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| p_Rd(X)
| gt(fifo_length,int_level(X))
| int_level(plus(X,n1)) = int_level(X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_44) ).
cnf(axiom_53,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| ~ p_Rd(X)
| ~ gt(int_level(X),n0)
| int_level(plus(X,n1)) = int_level(X) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_53) ).
cnf(axiom_59,axiom,
( p_Reset(X)
| ~ p_Wr(X)
| ~ p_Rd(X)
| gt(int_level(X),n0)
| int_level(plus(X,n1)) = plus(int_level(X),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_59) ).
cnf(quest_2,negated_conjecture,
p_Wr(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
cnf(quest_3,negated_conjecture,
~ p_Reset(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
cnf(quest_4,negated_conjecture,
p_Empty(plus(t_139,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_4) ).
cnf(quest_5,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
cnf(96,plain,
n1 != n0,
inference('PARAMODULATE',[status(thm)],[axiom_1,axiom_19,theory(equality)]) ).
cnf(100,plain,
int_level(plus(t_139,n1)) = n0,
inference('HYPERRESOLVE',[status(thm)],[axiom_25,quest_4]) ).
cnf(104,plain,
gt(fifo_length,minus(fifo_length,n1)),
inference('HYPERRESOLVE',[status(thm)],[axiom_3,quest_5]) ).
cnf(109,plain,
~ gt(n0,plus(X,n1)),
inference('UR-RESOLVE',[status(thm)],[axiom_13,axiom_17,axiom_2]) ).
cnf(119,plain,
( gt(n0,X)
| ~ gt(n1,plus(X,n1)) ),
inference('PARAMODULATE',[status(thm)],[axiom_9,axiom_19,theory(equality)]) ).
cnf(141,plain,
( plus(minus(X,Y),Y) = X
| def_10(Y,X) ),
inference('HYPERRESOLVE',[status(thm)],[axiom_4,theory(equality)]) ).
cnf(149,plain,
( n1 = fifo_length
| gt(fifo_length,n1) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_14,quest_5]),axiom_19,theory(equality)]) ).
cnf(167,plain,
( p_Rd(t_139)
| gt(fifo_length,int_level(t_139))
| p_Wr_error(plus(t_139,n1)) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_42,quest_2]),quest_3]) ).
cnf(178,plain,
( p_Rd(t_139)
| gt(fifo_length,int_level(t_139))
| n0 = int_level(t_139) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_44,quest_2]),100,quest_3,theory(equality)]) ).
cnf(184,plain,
( gt(int_level(t_139),fifo_length)
| fifo_length = int_level(t_139)
| p_Rd(t_139) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_35,quest_2,axiom_12]),axiom_1,100,quest_3,theory(equality)]) ).
cnf(220,plain,
( plus(minus(fifo_length,n1),n1) = fifo_length
| gt(fifo_length,plus(minus(fifo_length,n1),n1)) ),
inference('HYPERRESOLVE',[status(thm)],[axiom_14,104]) ).
cnf(221,plain,
~ gt(n0,X),
inference('UR-RESOLVE',[status(thm)],[axiom_14,109,axiom_1]) ).
cnf(222,plain,
~ gt(n1,plus(X,n1)),
inference('REWRITE',[status(thm)],[119,221]) ).
cnf(355,plain,
( plus(minus(fifo_length,n1),n1) = fifo_length
| n1 = fifo_length ),
inference('HYPERRESOLVE',[status(thm)],[axiom_6,141,149]) ).
cnf(392,plain,
( p_Rd(t_139)
| p_Wr_error(plus(t_139,n1)) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_35,167,quest_2]),axiom_1,100,quest_3,theory(equality)]) ).
cnf(394,plain,
( p_Rd(t_139)
| n0 = int_level(t_139) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_34,178,quest_2,392]),quest_3]) ).
cnf(395,plain,
n0 = int_level(t_139),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_53,394,quest_2,axiom_15]),100,quest_3,theory(equality)]) ).
cnf(396,plain,
( n0 = fifo_length
| p_Rd(t_139) ),
inference('REWRITE',[status(thm)],[184,221,395,theory(equality)]) ).
cnf(400,plain,
n0 = fifo_length,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[axiom_59,396,quest_2]),96,axiom_19,100,221,395,quest_3,theory(equality)]) ).
cnf(401,plain,
plus(X,n1) != fifo_length,
inference('REWRITE',[status(thm)],[axiom_1,400,theory(equality)]) ).
cnf(403,plain,
gt(fifo_length,plus(minus(fifo_length,n1),n1)),
inference('REWRITE',[status(thm)],[220,401]) ).
cnf(404,plain,
n1 = fifo_length,
inference('REWRITE',[status(thm)],[355,401]) ).
cnf(468,plain,
~ gt(fifo_length,plus(X,fifo_length)),
inference('REWRITE',[status(thm)],[222,404,theory(equality)]) ).
cnf(547,plain,
$false,
inference('REWRITE',[status(thm)],[403,468,404,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : HWV016-1 : TPTP v8.1.0. Released v2.5.0.
% 0.05/0.09 % Command : run-snark %s %d
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 600
% 0.08/0.28 % DateTime : Fri Jun 17 00:56:45 EDT 2022
% 0.08/0.28 % CPUTime :
% 0.12/0.37 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 *
% 0.12/0.38 *
% 0.12/0.38 #<PACKAGE "SNARK-USER">
% 0.12/0.38 *
% 0.12/0.38 SNARK-TPTP-OPTIONS
% 0.12/0.38 *
% 0.12/0.38 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.12/0.38 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.12/0.38 (USE-FACTORING :POS)
% 0.12/0.38 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.12/0.38 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.12/0.38 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.12/0.38 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.12/0.38 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.12/0.38 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.12/0.38 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.12/0.38 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.12/0.38 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.12/0.38 (DECLARE-TPTP-SYMBOLS2))
% 0.12/0.38 *
% 0.12/0.38 "."
% 0.12/0.38 *
% 0.12/0.38 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-17T00:56:45
% 0.12/0.38 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n032.cluster.edu at 2022-06-17T00:56:45
% 0.12/0.40
% 0.39/0.56 ; Recognized left identity assertion (= (|plus| |n0| ?X) ?X).
% 0.39/0.56
% 0.39/0.56 #||
% 0.39/0.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.56 % SZS output start Refutation
% See solution above
% 0.39/0.57 ||#
% 0.39/0.57
% 0.39/0.57 ; Summary of computation:
% 0.39/0.57 ; 1901 formulas have been input or derived (from 180 formulas).
% 0.39/0.57 ; 547 (29%) were retained. Of these,
% 0.39/0.57 ; 417 (76%) were simplified or subsumed later,
% 0.39/0.57 ; 130 (24%) are still being kept.
% 0.39/0.57 ;
% 0.39/0.57 ; Run time in seconds excluding printing time:
% 0.39/0.57 ; 0.013 7% Read assertion file (1 call)
% 0.39/0.57 ; 0.002 1% Assert (95 calls)
% 0.39/0.57 ; 0.028 15% Process new row (1,440 calls)
% 0.39/0.57 ; 0.030 17% Resolution (358 calls)
% 0.39/0.57 ; 0.007 4% Paramodulation (179 calls)
% 0.39/0.57 ; 0.001 1% Factoring (22 calls)
% 0.39/0.57 ; 0.006 3% Condensing (587 calls)
% 0.39/0.57 ; 0.024 13% Forward subsumption (587 calls)
% 0.39/0.57 ; 0.008 4% Backward subsumption (397 calls)
% 0.39/0.57 ; 0.012 7% Clause clause subsumption (936 calls)
% 0.39/0.57 ; 0.019 10% Forward simplification (1,326 calls)
% 0.39/0.57 ; 0.009 5% Backward simplification (546 calls)
% 0.39/0.57 ; 0.000 0% Ordering (2,262 calls)
% 0.39/0.57 ; 0.001 1% Sortal reasoning (32 calls)
% 0.39/0.57 ; 0.000 0% Purity testing (1 call)
% 0.39/0.57 ; 0.021 12% Other
% 0.39/0.57 ; 0.181 Total
% 0.39/0.57 ; 0.184 Real time
% 0.39/0.57 ;
% 0.39/0.57 ; Term-hash-array has 586 terms in all.
% 0.39/0.57 ; Feature-vector-row-index has 81 entries (292 at peak, 397 added, 316 deleted).
% 0.39/0.57 ; Feature-vector-row-index has 570 nodes (1,898 at peak, 2,649 added, 2,079 deleted).
% 0.39/0.57 ; Retrieved 2,073 possibly forward subsuming rows in 587 calls.
% 0.39/0.57 ; Retrieved 333 possibly backward subsumed rows in 397 calls.
% 0.39/0.57 ; Path-index has 181 entries (426 at peak, 618 added, 437 deleted).
% 0.39/0.57 ; Path-index has 673 nodes (854 at peak, 1,104 added, 431 deleted).
% 0.39/0.57 ; Trie-index has 181 entries (426 at peak, 618 added, 437 deleted).
% 0.39/0.57 ; Trie-index has 658 nodes (1,322 at peak, 2,045 added, 1,387 deleted).
% 0.39/0.57 ; Retrieved 2,193 generalization terms in 5,567 calls.
% 0.39/0.57 ; Retrieved 197 instance terms in 148 calls.
% 0.39/0.57 ; Retrieved 14,599 unifiable terms in 2,492 calls.
% 0.39/0.57 ;
% 0.39/0.57 ; The agenda of backward simplifiable rows to process has 176 entries:
% 0.39/0.57 ; 176 with value 0
% 0.39/0.57 ; The agenda of rows to process has 60 entries:
% 0.39/0.57 ; 3 with value 28 3 with value 39 2 with value 50
% 0.39/0.57 ; 1 with value 29 1 with value 40 2 with value 51
% 0.39/0.57 ; 1 with value 30 4 with value 41 2 with value 52
% 0.39/0.57 ; 3 with value 31 1 with value 42 1 with value 53
% 0.39/0.57 ; 2 with value 32 1 with value 43 1 with value 56
% 0.39/0.57 ; 4 with value 34 1 with value 45 1 with value 57
% 0.39/0.57 ; 3 with value 35 2 with value 46 2 with value 59
% 0.39/0.57 ; 4 with value 36 2 with value 47 1 with value 60
% 0.39/0.57 ; 2 with value 37 2 with value 48 2 with value 62
% 0.39/0.57 ; 3 with value 38 3 with value 49
% 0.39/0.57 ; The agenda of input rows to give has 41 entries:
% 0.39/0.57 ; 1 with value 6 4 with value 15 2 with value 22
% 0.39/0.57 ; 1 with value 7 1 with value 16 1 with value 27
% 0.39/0.57 ; 2 with value 9 5 with value 18 6 with value 28
% 0.39/0.57 ; 1 with value 10 3 with value 19 1 with value 29
% 0.39/0.57 ; 1 with value 11 4 with value 20 2 with value 34
% 0.39/0.57 ; 3 with value 13 2 with value 21 1 with value 35
% 0.39/0.57 ; The agenda of rows to give has 74 entries:
% 0.39/0.57 ; 2 with value (4 6) 6 with value (4 15) 1 with value (4 26)
% 0.39/0.57 ; 2 with value (4 8) 5 with value (4 17) 8 with value (4 27)
% 0.39/0.57 ; 3 with value (4 9) 7 with value (4 18) 2 with value (4 29)
% 0.39/0.57 ; 3 with value (4 10) 7 with value (4 20) 2 with value (4 30)
% 0.39/0.57 ; 1 with value (4 11) 2 with value (4 21) 1 with value (4 32)
% 0.39/0.57 ; 2 with value (4 12) 1 with value (4 22) 2 with value (4 41)
% 0.39/0.57 ; 1 with value (4 13) 4 with value (4 23) 3 with value (4 48)
% 0.39/0.57 ; 8 with value (4 14) 1 with value (4 25)
% 0.39/0.57 Evaluation took:
% 0.39/0.57 0.185 seconds of real time
% 0.39/0.57 0.16212 seconds of user run time
% 0.39/0.57 0.022103 seconds of system run time
% 0.39/0.57 [Run times include 0.006 seconds GC run time.]
% 0.39/0.57 0 calls to %EVAL
% 0.39/0.57 0 page faults and
% 0.39/0.57 19,030,048 bytes consed.
% 0.39/0.57 :PROOF-FOUND
% 0.39/0.57 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-17T00:56:45
% 0.39/0.57 :PROOF-FOUND
% 0.39/0.57 *
%------------------------------------------------------------------------------