%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWV901-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n014.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:24 EDT 2022
% Result : Unsatisfiable 4.63s 4.82s
% Output : Refutation 4.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 13
% Syntax : Number of clauses : 26 ( 19 unt; 0 nHn; 16 RR)
% Number of literals : 39 ( 11 equ; 17 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 : 22 ( 22 usr; 9 con; 0-5 aty)
% Number of variables : 35 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_set__empty__eq_1,axiom,
c_Option_Oset(c_Option_Ooption_ONone(X),X) = c_Orderings_Obot__class_Obot(tc_fun(X,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_set__empty__eq_1) ).
cnf(cls_Collect__def_0,axiom,
c_Collect(X,Y) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
cnf(cls_singleton__conv2_0,axiom,
c_Collect(hAPP(c_fequal(X),Y),X) = c_Set_Oinsert(Y,c_Orderings_Obot__class_Obot(tc_fun(X,tc_bool)),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
cnf(482,plain,
hAPP(c_fequal(X),Y) = c_Set_Oinsert(Y,c_Option_Oset(c_Option_Ooption_ONone(X),X),X),
inference('REWRITE',[status(thm)],[cls_singleton__conv2_0,cls_set__empty__eq_1,cls_Collect__def_0,theory(equality)]) ).
cnf(cls_Option_Oset_Osimps_I2_J_0,axiom,
c_Option_Oset(c_Option_Ooption_OSome(X,Y),Y) = c_Set_Oinsert(X,c_Orderings_Obot__class_Obot(tc_fun(Y,tc_bool)),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Option_Oset_Osimps_I2_J_0) ).
cnf(548,plain,
c_Option_Oset(c_Option_Ooption_OSome(X,Y),Y) = hAPP(c_fequal(Y),X),
inference('REWRITE',[status(thm)],[cls_Option_Oset_Osimps_I2_J_0,482,cls_set__empty__eq_1,theory(equality)]) ).
cnf(cls_WT__bodiesD_0,axiom,
( hAPP(c_Com_Obody,X) != c_Option_Ooption_OSome(Y,tc_Com_Ocom)
| ~ c_Com_OWT__bodies
| c_Com_OWT(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT__bodiesD_0) ).
cnf(cls_MGF_0,axiom,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Com_OWT(X)
| ~ c_Com_OWT__bodies
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_MGF_0) ).
cnf(576,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X),c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Com_OWT(X)
| ~ c_Com_OWT__bodies
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
inference('REWRITE',[status(thm)],[cls_MGF_0,cls_set__empty__eq_1,theory(equality)]) ).
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_cut_0,axiom,
( c_Hoare__Mirabelle_Ohoare__derivs(X,Y,Z)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X,U,Z)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(U,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cut_0) ).
cnf(cls_empty_0,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(X,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(Y),tc_bool)),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty_0) ).
cnf(626,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X,c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(Y)),tc_Hoare__Mirabelle_Otriple(Y)),Y),
inference('REWRITE',[status(thm)],[cls_empty_0,cls_set__empty__eq_1,theory(equality)]) ).
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_5,negated_conjecture,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
cnf(cls_conjecture_7,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_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
cnf(680,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_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference('REWRITE',[status(thm)],[cls_conjecture_7,cls_set__empty__eq_1,cls_image__image_0,theory(equality)]) ).
cnf(722,plain,
( hAPP(c_Com_Obody,X) != c_Option_Ooption_OSome(Y,tc_Com_Ocom)
| c_Com_OWT(Y) ),
inference('REWRITE',[status(thm)],[cls_WT__bodiesD_0,cls_conjecture_1]) ).
cnf(725,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X),c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Com_OWT(X) ),
inference('REWRITE',[status(thm)],[576,cls_conjecture_1,cls_conjecture_0]) ).
cnf(732,plain,
c_Option_Oset(c_Option_Ooption_OSome(X,Y),Y) = c_Set_Oinsert(X,c_Option_Oset(c_Option_Ooption_ONone(Y),Y),Y),
inference('REWRITE',[status(thm)],[482,548,theory(equality)]) ).
cnf(737,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Option_Oset(c_Option_Ooption_OSome(hAPP(c_Hoare__Mirabelle_OMGT,X),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)
| ~ c_Com_OWT(X) ),
inference('REWRITE',[status(thm)],[725,732,theory(equality)]) ).
cnf(740,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_Option_Oset(c_Option_Ooption_OSome(hAPP(c_Hoare__Mirabelle_OMGT,v_y),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference('REWRITE',[status(thm)],[680,732,theory(equality)]) ).
cnf(875,plain,
c_Com_OWT(v_y),
inference('HYPERRESOLVE',[status(thm)],[722,cls_conjecture_5]) ).
cnf(1981,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Option_Oset(c_Option_Ooption_ONone(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Option_Oset(c_Option_Ooption_OSome(hAPP(c_Hoare__Mirabelle_OMGT,v_y),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference('UR-RESOLVE',[status(thm)],[cls_cut_0,740,626]) ).
cnf(4432,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[737,875]),1981]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV901-1 : TPTP v8.1.0. Released v4.1.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n014.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 : Wed Jun 15 23:30:20 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.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/sandbox/benchmark/theBenchmark.p 2022-06-15T23:30:20
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n014.cluster.edu at 2022-06-15T23:30:20
% 0.47/0.64 WARNING:
% 0.47/0.64 |class_Ring__and__Field_Oordered__idom| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |c_Complete__Lattice_Ocomplete__lattice| is a 9-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |class_OrderedGroup_Opordered__ab__group__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |class_OrderedGroup_Oab__group__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |class_OrderedGroup_Ogroup__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |c_OrderedGroup_Oab__semigroup__mult| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.64 WARNING:
% 0.47/0.64 |class_OrderedGroup_Olordered__ab__group__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 4.63/4.82
% 4.63/4.82
% 4.63/4.82 #||
% 4.63/4.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.63/4.82 % SZS output start Refutation
% See solution above
% 4.63/4.82 ||#
% 4.63/4.82
% 4.63/4.82 ; Summary of computation:
% 4.63/4.82 ; 11251 formulas have been input or derived (from 564 formulas).
% 4.63/4.82 ; 4432 (39%) were retained. Of these,
% 4.63/4.82 ; 882 (20%) were simplified or subsumed later,
% 4.63/4.82 ; 3550 (80%) are still being kept.
% 4.63/4.82 ;
% 4.63/4.82 ; Run time in seconds excluding printing time:
% 4.63/4.82 ; 0.145 3% Read assertion file (1 call)
% 4.63/4.82 ; 0.012 0% Assert (713 calls)
% 4.63/4.82 ; 0.748 17% Process new row (10,223 calls)
% 4.63/4.82 ; 0.392 9% Resolution (1,126 calls)
% 4.63/4.82 ; 0.135 3% Paramodulation (563 calls)
% 4.63/4.82 ; 0.000 0% Factoring (12 calls)
% 4.63/4.82 ; 0.065 1% Condensing (3,971 calls)
% 4.63/4.82 ; 0.893 21% Forward subsumption (3,971 calls)
% 4.63/4.82 ; 0.225 5% Backward subsumption (3,090 calls)
% 4.63/4.82 ; 0.045 1% Clause clause subsumption (10,517 calls)
% 4.63/4.82 ; 0.855 20% Forward simplification (8,575 calls)
% 4.63/4.82 ; 0.129 3% Backward simplification (4,282 calls)
% 4.63/4.82 ; 0.639 15% Ordering (38,056 calls)
% 4.63/4.82 ; 0.000 0% Sortal reasoning (32 calls)
% 4.63/4.82 ; 0.002 0% Purity testing (1 call)
% 4.63/4.82 ; 0.062 1% Other
% 4.63/4.82 ; 4.347 Total
% 4.63/4.82 ; 4.350 Real time
% 4.63/4.82 ;
% 4.63/4.82 ; Term-hash-array has 13,722 terms in all.
% 4.63/4.82 ; Feature-vector-row-index has 2,646 entries (2,646 at peak, 3,090 added, 444 deleted).
% 4.63/4.82 ; Feature-vector-row-index has 33,418 nodes (33,418 at peak, 37,861 added, 4,443 deleted).
% 4.63/4.82 ; Retrieved 14,608 possibly forward subsuming rows in 3,971 calls.
% 4.63/4.82 ; Retrieved 1,701 possibly backward subsumed rows in 3,090 calls.
% 4.63/4.82 ; Path-index has 12,032 entries (12,038 at peak, 14,103 added, 2,071 deleted).
% 4.63/4.82 ; Path-index has 44,725 nodes (44,749 at peak, 48,195 added, 3,470 deleted).
% 4.63/4.82 ; Trie-index has 12,032 entries (12,038 at peak, 14,103 added, 2,071 deleted).
% 4.63/4.82 ; Trie-index has 89,557 nodes (89,887 at peak, 105,208 added, 15,651 deleted).
% 4.63/4.82 ; Retrieved 62,900 generalization terms in 75,495 calls.
% 4.63/4.82 ; Retrieved 4,945 instance terms in 1,412 calls.
% 4.63/4.82 ; Retrieved 466,356 unifiable terms in 9,747 calls.
% 4.63/4.82 ;
% 4.63/4.82 ; The agenda of rows to process has 3 entries:
% 4.63/4.82 ; 1 with value 27 1 with value 28 1 with value 50
% 4.63/4.82 ; The agenda of rows to give has 3075 entries:
% 4.63/4.82 ; 1 with value (4 5) 35 with value (4 68) 8 with value (4 130)
% 4.63/4.82 ; 6 with value (4 6) 46 with value (4 69) 1 with value (4 131)
% 4.63/4.82 ; 21 with value (4 7) 39 with value (4 70) 3 with value (4 132)
% 4.63/4.82 ; 3 with value (4 8) 27 with value (4 71) 5 with value (4 134)
% 4.63/4.82 ; 1 with value (4 9) 26 with value (4 72) 1 with value (4 135)
% 4.63/4.82 ; 5 with value (4 10) 26 with value (4 73) 5 with value (4 136)
% 4.63/4.82 ; 8 with value (4 11) 17 with value (4 74) 3 with value (4 137)
% 4.63/4.82 ; 6 with value (4 12) 22 with value (4 75) 3 with value (4 138)
% 4.63/4.82 ; 11 with value (4 13) 24 with value (4 76) 2 with value (4 139)
% 4.63/4.82 ; 25 with value (4 14) 21 with value (4 77) 4 with value (4 140)
% 4.63/4.82 ; 7 with value (4 15) 33 with value (4 78) 3 with value (4 142)
% 4.63/4.82 ; 16 with value (4 16) 30 with value (4 79) 1 with value (4 143)
% 4.63/4.82 ; 14 with value (4 17) 19 with value (4 80) 5 with value (4 144)
% 4.63/4.82 ; 24 with value (4 18) 20 with value (4 81) 4 with value (4 145)
% 4.63/4.82 ; 27 with value (4 19) 26 with value (4 82) 1 with value (4 146)
% 4.63/4.82 ; 26 with value (4 20) 14 with value (4 83) 2 with value (4 147)
% 4.63/4.82 ; 36 with value (4 21) 15 with value (4 84) 1 with value (4 148)
% 4.63/4.82 ; 28 with value (4 22) 11 with value (4 85) 2 with value (4 149)
% 4.63/4.82 ; 26 with value (4 23) 13 with value (4 86) 1 with value (4 150)
% 4.63/4.82 ; 27 with value (4 24) 14 with value (4 87) 2 with value (4 151)
% 4.63/4.82 ; 38 with value (4 25) 16 with value (4 88) 1 with value (4 152)
% 4.63/4.82 ; 35 with value (4 26) 17 with value (4 89) 1 with value (4 153)
% 4.63/4.82 ; 40 with value (4 27) 24 with value (4 90) 4 with value (4 158)
% 4.63/4.82 ; 50 with value (4 28) 12 with value (4 91) 2 with value (4 159)
% 4.63/4.82 ; 49 with value (4 29) 15 with value (4 92) 2 with value (4 160)
% 4.63/4.82 ; 45 with value (4 30) 8 with value (4 93) 4 with value (4 161)
% 4.63/4.82 ; 52 with value (4 31) 12 with value (4 94) 3 with value (4 162)
% 4.63/4.82 ; 39 with value (4 32) 19 with value (4 95) 1 with value (4 165)
% 4.63/4.82 ; 51 with value (4 33) 17 with value (4 96) 2 with value (4 166)
% 4.63/4.82 ; 49 with value (4 34) 10 with value (4 97) 2 with value (4 167)
% 4.63/4.82 ; 64 with value (4 35) 1 with value (4 98) 1 with value (4 169)
% 4.63/4.82 ; 33 with value (4 36) 7 with value (4 99) 2 with value (4 170)
% 4.63/4.82 ; 57 with value (4 37) 15 with value (4 100) 1 with value (4 171)
% 4.63/4.82 ; 61 with value (4 38) 7 with value (4 101) 1 with value (4 172)
% 4.63/4.82 ; 49 with value (4 39) 2 with value (4 102) 2 with value (4 173)
% 4.63/4.82 ; 37 with value (4 40) 7 with value (4 103) 1 with value (4 175)
% 4.63/4.82 ; 56 with value (4 41) 12 with value (4 104) 1 with value (4 179)
% 4.63/4.82 ; 50 with value (4 42) 5 with value (4 105) 2 with value (4 180)
% 4.63/4.82 ; 44 with value (4 43) 8 with value (4 106) 1 with value (4 181)
% 4.63/4.82 ; 46 with value (4 44) 8 with value (4 107) 1 with value (4 182)
% 4.63/4.82 ; 60 with value (4 45) 5 with value (4 108) 1 with value (4 183)
% 4.63/4.82 ; 59 with value (4 46) 3 with value (4 109) 2 with value (4 185)
% 4.63/4.82 ; 51 with value (4 47) 4 with value (4 110) 2 with value (4 186)
% 4.63/4.82 ; 40 with value (4 48) 7 with value (4 111) 1 with value (4 189)
% 4.63/4.82 ; 44 with value (4 49) 12 with value (4 112) 1 with value (4 190)
% 4.63/4.82 ; 48 with value (4 50) 8 with value (4 113) 2 with value (4 191)
% 4.63/4.82 ; 33 with value (4 51) 6 with value (4 114) 1 with value (4 193)
% 4.63/4.82 ; 41 with value (4 52) 12 with value (4 115) 1 with value (4 194)
% 4.63/4.82 ; 37 with value (4 53) 11 with value (4 116) 1 with value (4 197)
% 4.63/4.82 ; 44 with value (4 54) 3 with value (4 117) 1 with value (4 204)
% 4.63/4.82 ; 40 with value (4 55) 2 with value (4 118) 2 with value (4 206)
% 4.63/4.82 ; 25 with value (4 56) 5 with value (4 119) 2 with value (4 207)
% 4.63/4.82 ; 33 with value (4 57) 9 with value (4 120) 1 with value (4 208)
% 4.63/4.82 ; 45 with value (4 58) 6 with value (4 121) 1 with value (4 209)
% 4.63/4.82 ; 32 with value (4 59) 2 with value (4 122) 1 with value (4 213)
% 4.63/4.82 ; 19 with value (4 60) 7 with value (4 123) 1 with value (4 217)
% 4.63/4.82 ; 30 with value (4 61) 4 with value (4 124) 1 with value (4 218)
% 4.63/4.82 ; 32 with value (4 62) 5 with value (4 125) 1 with value (4 224)
% 4.63/4.82 ; 38 with value (4 63) 6 with value (4 126) 2 with value (4 227)
% 4.63/4.82 ; 26 with value (4 64) 4 with value (4 127) 1 with value (4 247)
% 4.63/4.82 ; 19 with value (4 65) 8 with value (4 128) 1 with value (4 302)
% 4.63/4.82 ; 29 with value (4 66) 7 with value (4 129) 1 with value (4 322)
% 4.63/4.82 ; 31 with value (4 67)
% 4.63/4.82 Evaluation took:
% 4.63/4.82 4.355 seconds of real time
% 4.63/4.82 4.111374 seconds of user run time
% 4.63/4.82 0.243071 seconds of system run time
% 4.63/4.82 [Run times include 0.716 seconds GC run time.]
% 4.63/4.82 0 calls to %EVAL
% 4.63/4.82 0 page faults and
% 4.63/4.82 324,606,520 bytes consed.
% 4.63/4.82 :PROOF-FOUND
% 4.63/4.82 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-15T23:30:25
% 4.63/4.82 :PROOF-FOUND
% 4.63/4.82 *
%------------------------------------------------------------------------------