%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWV908-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n008.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:36:25 EDT 2022
% Result : Unsatisfiable 3.45s 3.65s
% Output : Refutation 3.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 6
% Syntax : Number of clauses : 9 ( 7 unt; 0 nHn; 7 RR)
% Number of literals : 13 ( 1 equ; 6 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-5 aty)
% Number of variables : 10 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_equalityE_0,axiom,
c_lessequals(X,X,tc_fun(Y,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_equalityE_0) ).
cnf(cls_MGF__lemma2__simult_0,axiom,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X,tc_Com_Ostate)
| ~ c_lessequals(X,c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool))
| ~ c_Com_OWT__bodies
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_MGF__lemma2__simult_0) ).
cnf(cls_image__image_0,axiom,
c_Set_Oimage(X,c_Set_Oimage(Y,Z,U,V),V,W) = c_Set_Oimage(c_COMBB(X,Y,V,W,U),Z,U,W),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__image_0) ).
cnf(cls_conjecture_0,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_conjecture_1,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_4,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
cnf(374,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference('REWRITE',[status(thm)],[cls_conjecture_4,cls_image__image_0,theory(equality)]) ).
cnf(409,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Com_Ocom_OBODY,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X,tc_Com_Ostate)
| ~ c_lessequals(X,c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)) ),
inference('REWRITE',[status(thm)],[cls_MGF__lemma2__simult_0,cls_conjecture_0,cls_conjecture_1,cls_image__image_0,theory(equality)]) ).
cnf(4502,plain,
$false,
inference('UR-RESOLVE',[status(thm)],[409,374,cls_equalityE_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV908-1 : TPTP v8.1.0. Released v4.1.0.
% 0.03/0.13 % Command : run-snark %s %d
% 0.13/0.33 % Computer : n008.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Tue Jun 14 16:01:37 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-14T16:01:37
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n008.cluster.edu at 2022-06-14T16:01:37
% 3.45/3.65
% 3.45/3.65
% 3.45/3.65 #||
% 3.45/3.65 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.45/3.65 % SZS output start Refutation
% See solution above
% 3.45/3.65 ||#
% 3.45/3.65
% 3.45/3.65 ; Summary of computation:
% 3.45/3.65 ; 10296 formulas have been input or derived (from 374 formulas).
% 3.45/3.65 ; 4502 (44%) were retained. Of these,
% 3.45/3.65 ; 65 ( 1%) were simplified or subsumed later,
% 3.45/3.65 ; 4437 (99%) are still being kept.
% 3.45/3.65 ;
% 3.45/3.65 ; Run time in seconds excluding printing time:
% 3.45/3.66 ; 0.106 3% Read assertion file (1 call)
% 3.45/3.66 ; 0.004 0% Assert (481 calls)
% 3.45/3.66 ; 0.455 14% Process new row (9,419 calls)
% 3.45/3.66 ; 0.257 8% Resolution (746 calls)
% 3.45/3.66 ; 0.041 1% Paramodulation (373 calls)
% 3.45/3.66 ; 0.000 0% Factoring (12 calls)
% 3.45/3.66 ; 0.021 1% Condensing (1,460 calls)
% 3.45/3.66 ; 0.075 2% Forward subsumption (1,460 calls)
% 3.45/3.66 ; 0.027 1% Backward subsumption (1,141 calls)
% 3.45/3.66 ; 0.015 0% Clause clause subsumption (2,188 calls)
% 3.45/3.66 ; 0.642 20% Forward simplification (9,410 calls)
% 3.45/3.66 ; 0.070 2% Backward simplification (4,493 calls)
% 3.45/3.66 ; 1.412 44% Ordering (136,992 calls)
% 3.45/3.66 ; 0.000 0% Sortal reasoning (32 calls)
% 3.45/3.66 ; 0.001 0% Purity testing (1 call)
% 3.45/3.66 ; 0.064 2% Other
% 3.45/3.66 ; 3.190 Total
% 3.45/3.66 ; 3.192 Real time
% 3.45/3.66 ;
% 3.49/3.66 ; Term-hash-array has 11,425 terms in all.
% 3.49/3.66 ; Feature-vector-row-index has 1,111 entries (1,111 at peak, 1,141 added, 30 deleted).
% 3.49/3.66 ; Feature-vector-row-index has 9,312 nodes (9,312 at peak, 9,736 added, 424 deleted).
% 3.49/3.66 ; Retrieved 4,394 possibly forward subsuming rows in 1,460 calls.
% 3.49/3.66 ; Retrieved 483 possibly backward subsumed rows in 1,141 calls.
% 3.49/3.66 ; Path-index has 11,342 entries (11,342 at peak, 11,487 added, 145 deleted).
% 3.49/3.66 ; Path-index has 20,284 nodes (20,284 at peak, 20,462 added, 178 deleted).
% 3.49/3.66 ; Trie-index has 11,342 entries (11,342 at peak, 11,487 added, 145 deleted).
% 3.49/3.66 ; Trie-index has 67,477 nodes (67,477 at peak, 68,293 added, 816 deleted).
% 3.49/3.66 ; Retrieved 140,140 generalization terms in 44,521 calls.
% 3.49/3.66 ; Retrieved 5,422 instance terms in 3,619 calls.
% 3.49/3.66 ; Retrieved 298,633 unifiable terms in 5,598 calls.
% 3.49/3.66 ;
% 3.49/3.66 ; The agenda of rows to process has 5 entries:
% 3.49/3.66 ; 1 with value 25 1 with value 51 1 with value 54
% 3.49/3.66 ; 1 with value 41 1 with value 52
% 3.49/3.66 ; The agenda of input rows to give has 12 entries:
% 3.49/3.66 ; 1 with value 52 1 with value 70 1 with value 155
% 3.49/3.66 ; 1 with value 53 1 with value 77 2 with value 172
% 3.49/3.66 ; 1 with value 57 1 with value 81 2 with value 178
% 3.49/3.66 ; 1 with value 67
% 3.49/3.66 ; The agenda of rows to give has 4056 entries:
% 3.49/3.66 ; 1 with value (4 4) 73 with value (4 29) 40 with value (4 54)
% 3.49/3.66 ; 1 with value (4 5) 60 with value (4 30) 5 with value (4 55)
% 3.49/3.66 ; 4 with value (4 6) 50 with value (4 31) 6 with value (4 56)
% 3.49/3.66 ; 21 with value (4 7) 55 with value (4 32) 3 with value (4 57)
% 3.49/3.66 ; 10 with value (4 8) 43 with value (4 33) 3 with value (4 58)
% 3.49/3.66 ; 9 with value (4 9) 58 with value (4 34) 4 with value (4 59)
% 3.49/3.66 ; 21 with value (4 10) 40 with value (4 35) 3 with value (4 60)
% 3.49/3.66 ; 24 with value (4 11) 44 with value (4 36) 6 with value (4 61)
% 3.49/3.66 ; 37 with value (4 12) 37 with value (4 37) 4 with value (4 62)
% 3.49/3.66 ; 75 with value (4 13) 45 with value (4 38) 3 with value (4 63)
% 3.49/3.66 ; 90 with value (4 14) 41 with value (4 39) 9 with value (4 64)
% 3.49/3.66 ; 118 with value (4 15) 31 with value (4 40) 2 with value (4 66)
% 3.49/3.66 ; 191 with value (4 16) 28 with value (4 41) 3 with value (4 67)
% 3.49/3.66 ; 163 with value (4 17) 34 with value (4 42) 8 with value (4 69)
% 3.49/3.66 ; 222 with value (4 18) 26 with value (4 43) 3 with value (4 70)
% 3.49/3.66 ; 102 with value (4 19) 33 with value (4 44) 1 with value (4 71)
% 3.49/3.66 ; 119 with value (4 20) 34 with value (4 45) 2 with value (4 73)
% 3.49/3.66 ; 94 with value (4 21) 75 with value (4 46) 2 with value (4 74)
% 3.49/3.66 ; 55 with value (4 22) 133 with value (4 47) 1 with value (4 76)
% 3.49/3.66 ; 57 with value (4 23) 200 with value (4 48) 1 with value (4 78)
% 3.49/3.66 ; 82 with value (4 24) 138 with value (4 49) 1 with value (4 79)
% 3.49/3.66 ; 95 with value (4 25) 382 with value (4 50) 1 with value (4 80)
% 3.49/3.66 ; 69 with value (4 26) 278 with value (4 51) 1 with value (4 82)
% 3.49/3.66 ; 57 with value (4 27) 145 with value (4 52) 1 with value (4 86)
% 3.49/3.66 ; 76 with value (4 28) 67 with value (4 53)
% 3.49/3.66 Evaluation took:
% 3.49/3.66 3.193 seconds of real time
% 3.49/3.66 2.93929 seconds of user run time
% 3.49/3.66 0.253237 seconds of system run time
% 3.49/3.66 [Run times include 0.26 seconds GC run time.]
% 3.49/3.66 0 calls to %EVAL
% 3.49/3.66 0 page faults and
% 3.49/3.66 220,774,488 bytes consed.
% 3.49/3.66 :PROOF-FOUND
% 3.49/3.66 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-14T16:01:41
% 3.49/3.66 :PROOF-FOUND
% 3.49/3.66 *
%------------------------------------------------------------------------------