%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWV578-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n010.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 : Wed Jul 20 21:35:20 EDT 2022
% Result : Unsatisfiable 2.77s 2.99s
% Output : Refutation 2.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 5
% Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 5 RR)
% Number of literals : 9 ( 4 equ; 4 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-4 aty)
% Number of variables : 6 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_setsum__head__upt__Suc_0,axiom,
( ~ class_OrderedGroup_Ocomm__monoid__add(X)
| c_Finite__Set_Osetsum(Y,c_SetInterval_Oord__class_OatLeastLessThan(Z,U,tc_nat),tc_nat,X) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X),hAPP(Y,Z)),c_Finite__Set_Osetsum(Y,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,Z),U,tc_nat),tc_nat,X))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(Z,tc_nat),U)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__head__upt__Suc_0) ).
cnf(cls_less_0,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_m,tc_nat),v_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less_0) ).
cnf(cls_atLeastSucLessThan__greaterThanLessThan_0,axiom,
c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X),Y,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(X,Y,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastSucLessThan__greaterThanLessThan_0) ).
cnf(tfree_tcs,negated_conjecture,
class_OrderedGroup_Ocomm__monoid__add(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
cnf(cls_conjecture_0,negated_conjecture,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(676,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,v_m),v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference('REWRITE',[status(thm)],[cls_conjecture_0,cls_atLeastSucLessThan__greaterThanLessThan_0,theory(equality)]) ).
cnf(2265,plain,
$false,
inference('UR-RESOLVE',[status(thm)],[cls_setsum__head__upt__Suc_0,tfree_tcs,676,cls_less_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV578-1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n010.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 : Thu Jun 16 06:25:39 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.20/0.48 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.50 *
% 0.20/0.50 *
% 0.20/0.51 #<PACKAGE "SNARK-USER">
% 0.20/0.51 *
% 0.20/0.51 SNARK-TPTP-OPTIONS
% 0.20/0.51 *
% 0.20/0.51 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.51 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.51 (USE-FACTORING :POS)
% 0.20/0.51 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.51 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.51 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.51 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.51 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.51 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.51 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.51 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.51 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.51 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.51 *
% 0.20/0.51 "."
% 0.20/0.51 *
% 0.20/0.51 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-16T06:25:39
% 0.20/0.51 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n010.cluster.edu at 2022-06-16T06:25:39
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_RealVector_Ovector__space| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |class_Divides_Oring__div| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_Ring__and__Field_Oring| is a 6-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_Ring__and__Field_Ofield| is a 9-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_RealVector_Obounded__bilinear| is a 4-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |class_OrderedGroup_Oab__semigroup__idem__mult| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_OrderedGroup_Opordered__ab__group__add| is a 7-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_Ring__and__Field_Opordered__ring| is a 8-ary relation that occurs only negatively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |c_OrderedGroup_Ocancel__ab__semigroup__add__axioms| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.84/1.02 WARNING:
% 0.84/1.02 |class_OrderedGroup_Osemigroup__mult| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 2.77/2.99
% 2.77/2.99
% 2.77/2.99 #||
% 2.77/2.99 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.77/2.99 % SZS output start Refutation
% See solution above
% 2.77/2.99 ||#
% 2.77/2.99
% 2.77/2.99 ; Summary of computation:
% 2.77/2.99 ; 4993 formulas have been input or derived (from 715 formulas).
% 2.77/2.99 ; 2265 (45%) were retained. Of these,
% 2.77/2.99 ; 39 ( 2%) were simplified or subsumed later,
% 2.77/2.99 ; 2226 (98%) are still being kept.
% 2.77/2.99 ;
% 2.77/2.99 ; Run time in seconds excluding printing time:
% 2.77/2.99 ; 0.438 18% Read assertion file (1 call)
% 2.77/2.99 ; 0.046 2% Assert (1,225 calls)
% 2.77/2.99 ; 0.395 16% Process new row (4,478 calls)
% 2.77/2.99 ; 0.365 15% Resolution (1,428 calls)
% 2.77/2.99 ; 0.073 3% Paramodulation (714 calls)
% 2.77/2.99 ; 0.000 0% Factoring (4 calls)
% 2.77/2.99 ; 0.067 3% Condensing (2,653 calls)
% 2.77/3.00 ; 0.389 16% Forward subsumption (2,653 calls)
% 2.77/3.00 ; 0.110 4% Backward subsumption (1,678 calls)
% 2.77/3.00 ; 0.068 3% Clause clause subsumption (4,672 calls)
% 2.77/3.00 ; 0.270 11% Forward simplification (4,174 calls)
% 2.77/3.00 ; 0.025 1% Backward simplification (2,263 calls)
% 2.77/3.00 ; 0.154 6% Ordering (8,903 calls)
% 2.77/3.00 ; 0.000 0% Sortal reasoning (32 calls)
% 2.77/3.00 ; 0.008 0% Purity testing (1 call)
% 2.77/3.00 ; 0.072 3% Other
% 2.77/3.00 ; 2.480 Total
% 2.77/3.00 ; 2.487 Real time
% 2.77/3.00 ;
% 2.77/3.00 ; Term-hash-array has 5,754 terms in all.
% 2.77/3.00 ; Feature-vector-row-index has 1,663 entries (1,663 at peak, 1,678 added, 15 deleted).
% 2.77/3.00 ; Feature-vector-row-index has 13,476 nodes (13,476 at peak, 13,623 added, 147 deleted).
% 2.77/3.00 ; Retrieved 9,658 possibly forward subsuming rows in 2,653 calls.
% 2.77/3.00 ; Retrieved 1,482 possibly backward subsumed rows in 1,678 calls.
% 2.77/3.00 ; Path-index has 5,698 entries (5,698 at peak, 5,790 added, 92 deleted).
% 2.77/3.00 ; Path-index has 8,128 nodes (8,128 at peak, 8,167 added, 39 deleted).
% 2.77/3.00 ; Trie-index has 5,698 entries (5,698 at peak, 5,790 added, 92 deleted).
% 2.77/3.00 ; Trie-index has 21,708 nodes (21,708 at peak, 21,984 added, 276 deleted).
% 2.77/3.00 ; Retrieved 11,053 generalization terms in 26,801 calls.
% 2.77/3.00 ; Retrieved 1,172 instance terms in 736 calls.
% 2.77/3.00 ; Retrieved 251,237 unifiable terms in 6,939 calls.
% 2.77/3.00 ;
% 2.77/3.00 ; The agenda of rows to process has 24 entries:
% 2.77/3.00 ; 1 with value 4 6 with value 32 9 with value 45
% 2.77/3.00 ; 1 with value 10 6 with value 36 1 with value 54
% 2.77/3.00 ; The agenda of input rows to give has 76 entries:
% 2.77/3.00 ; 1 with value 43 4 with value 51 2 with value 58
% 2.77/3.00 ; 7 with value 44 9 with value 53 6 with value 59
% 2.77/3.00 ; 2 with value 46 5 with value 54 6 with value 62
% 2.77/3.00 ; 1 with value 47 8 with value 55 4 with value 63
% 2.77/3.00 ; 4 with value 48 3 with value 56 4 with value 64
% 2.77/3.00 ; 5 with value 49 4 with value 57 1 with value 71
% 2.77/3.00 ; The agenda of rows to give has 1435 entries:
% 2.77/3.00 ; 3 with value (4 4) 26 with value (4 24) 41 with value (4 43)
% 2.77/3.00 ; 1 with value (4 5) 29 with value (4 25) 32 with value (4 44)
% 2.77/3.00 ; 3 with value (4 6) 31 with value (4 26) 23 with value (4 45)
% 2.77/3.00 ; 28 with value (4 7) 30 with value (4 27) 24 with value (4 46)
% 2.77/3.00 ; 4 with value (4 8) 37 with value (4 28) 29 with value (4 47)
% 2.77/3.00 ; 6 with value (4 9) 43 with value (4 29) 31 with value (4 48)
% 2.77/3.00 ; 9 with value (4 10) 62 with value (4 30) 28 with value (4 49)
% 2.77/3.00 ; 1 with value (4 11) 48 with value (4 31) 28 with value (4 50)
% 2.77/3.00 ; 19 with value (4 12) 32 with value (4 32) 42 with value (4 51)
% 2.77/3.00 ; 16 with value (4 13) 43 with value (4 33) 23 with value (4 52)
% 2.77/3.00 ; 26 with value (4 14) 45 with value (4 34) 23 with value (4 53)
% 2.77/3.00 ; 16 with value (4 15) 36 with value (4 35) 12 with value (4 54)
% 2.77/3.00 ; 22 with value (4 16) 58 with value (4 36) 4 with value (4 55)
% 2.77/3.00 ; 14 with value (4 17) 46 with value (4 37) 2 with value (4 56)
% 2.77/3.00 ; 19 with value (4 18) 48 with value (4 38) 5 with value (4 57)
% 2.77/3.00 ; 16 with value (4 19) 73 with value (4 39) 1 with value (4 58)
% 2.77/3.00 ; 25 with value (4 20) 41 with value (4 40) 1 with value (4 59)
% 2.77/3.00 ; 21 with value (4 21) 30 with value (4 41) 2 with value (4 64)
% 2.77/3.00 ; 22 with value (4 22) 27 with value (4 42) 5 with value (4 69)
% 2.77/3.00 ; 23 with value (4 23)
% 2.77/3.00 Evaluation took:
% 2.77/3.00 2.49 seconds of real time
% 2.77/3.00 2.340686 seconds of user run time
% 2.77/3.00 0.144134 seconds of system run time
% 2.77/3.00 [Run times include 0.267 seconds GC run time.]
% 2.77/3.00 0 calls to %EVAL
% 2.77/3.00 0 page faults and
% 2.77/3.00 101,925,048 bytes consed.
% 2.77/3.00 :PROOF-FOUND
% 2.77/3.00 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-16T06:25:41
% 2.77/3.00 :PROOF-FOUND
% 2.77/3.00 *
%------------------------------------------------------------------------------