%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWV892-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n029.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:22 EDT 2022
% Result : Unsatisfiable 124.23s 124.42s
% Output : Refutation 124.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of clauses : 24 ( 16 unt; 1 nHn; 17 RR)
% Number of literals : 33 ( 16 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-4 aty)
% Number of variables : 39 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_Collect__def_0,axiom,
c_Collect(X,Y) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
cnf(cls_WTs__elim__cases_I7_J_0,axiom,
( hAPP(c_Com_Obody,X) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X),tc_Com_Ocom)
| ~ c_Com_OWT(c_Com_Ocom_OBODY(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WTs__elim__cases_I7_J_0) ).
cnf(cls_COMBC__def_0,axiom,
hAPP(hAPP(c_COMBC(X,Y,Z,U),V),W) = hAPP(hAPP(X,W),V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
cnf(cls_Collect__mem__eq_0,axiom,
c_Collect(hAPP(c_COMBC(c_in(X),X,tc_fun(X,tc_bool),tc_bool),Y),X) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__mem__eq_0) ).
cnf(490,plain,
hAPP(c_COMBC(c_in(X),X,tc_fun(X,tc_bool),tc_bool),Y) = Y,
inference('REWRITE',[status(thm)],[cls_Collect__mem__eq_0,cls_Collect__def_0,theory(equality)]) ).
cnf(cls_CollectD_0,axiom,
( hBOOL(hAPP(X,Y))
| ~ hBOOL(hAPP(hAPP(c_in(Z),Y),c_Collect(X,Z))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CollectD_0) ).
cnf(515,plain,
( hBOOL(hAPP(X,Y))
| ~ hBOOL(hAPP(hAPP(c_in(Z),Y),X)) ),
inference('REWRITE',[status(thm)],[cls_CollectD_0,cls_Collect__def_0,theory(equality)]) ).
cnf(cls_WT_OBody_0,axiom,
( c_Com_OWT(c_Com_Ocom_OBODY(X))
| hAPP(c_Com_Obody,X) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_WT_OBody_0) ).
cnf(cls_the_Osimps_0,axiom,
c_Option_Othe(c_Option_Ooption_OSome(X,Y),Y) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_the_Osimps_0) ).
cnf(cls_domIff_0,axiom,
( hAPP(X,Y) != c_Option_Ooption_ONone(Z)
| ~ hBOOL(hAPP(hAPP(c_in(U),Y),c_Map_Odom(X,U,Z))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_domIff_0) ).
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_conjecture_1,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_3,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
cnf(cls_conjecture_4,negated_conjecture,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
cnf(617,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(810,plain,
hAPP(c_Com_Obody,X) != c_Option_Ooption_OSome(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom),tc_Com_Ocom),
inference('UR-RESOLVE',[status(thm)],[617,cls_conjecture_4]) ).
cnf(1436,plain,
hBOOL(hAPP(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_pn)),
inference('HYPERRESOLVE',[status(thm)],[515,cls_conjecture_3]) ).
cnf(1606,plain,
hAPP(X,Y) = hAPP(hAPP(c_in(Z),Y),X),
inference('PARAMODULATE',[status(thm)],[cls_COMBC__def_0,490,theory(equality)]) ).
cnf(1630,plain,
( hAPP(X,Y) != c_Option_Ooption_ONone(Z)
| ~ hBOOL(hAPP(c_Map_Odom(X,U,Z),Y)) ),
inference('REWRITE',[status(thm)],[cls_domIff_0,1606,theory(equality)]) ).
cnf(28161,plain,
hAPP(c_Com_Obody,v_pn) != c_Option_Ooption_ONone(tc_Com_Ocom),
inference('UR-RESOLVE',[status(thm)],[1630,1436]) ).
cnf(29515,plain,
c_Com_OWT(c_Com_Ocom_OBODY(v_pn)),
inference('UR-RESOLVE',[status(thm)],[cls_WT_OBody_0,28161]) ).
cnf(29595,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom),
inference('HYPERRESOLVE',[status(thm)],[cls_WTs__elim__cases_I7_J_0,29515]) ).
cnf(29603,plain,
hAPP(c_Com_Obody,X) != c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom),
inference('REWRITE',[status(thm)],[810,cls_the_Osimps_0,29595,theory(equality)]) ).
cnf(29604,plain,
$false,
inference('REWRITE',[status(thm)],[29595,29603]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWV892-1 : TPTP v8.1.0. Released v4.1.0.
% 0.13/0.14 % Command : run-snark %s %d
% 0.13/0.35 % Computer : n029.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Tue Jun 14 17:02:11 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.46 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.47 *
% 0.20/0.47 *
% 0.20/0.48 #<PACKAGE "SNARK-USER">
% 0.20/0.48 *
% 0.20/0.48 SNARK-TPTP-OPTIONS
% 0.20/0.48 *
% 0.20/0.48 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.48 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.48 (USE-FACTORING :POS)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.48 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.48 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.48 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.48 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.48 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.48 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.48 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.48 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.48 *
% 0.20/0.48 "."
% 0.20/0.48 *
% 0.20/0.48 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-14T17:02:11
% 0.20/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n029.cluster.edu at 2022-06-14T17:02:11
% 0.47/0.66 WARNING:
% 0.47/0.66 |class_Ring__and__Field_Oordered__idom| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.66 WARNING:
% 0.47/0.66 |class_Ring__and__Field_Oring| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.66 WARNING:
% 0.47/0.66 |class_OrderedGroup_Oab__group__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.66 WARNING:
% 0.47/0.66 |class_OrderedGroup_Opordered__ab__group__add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 124.23/124.42
% 124.23/124.42
% 124.23/124.42 #||
% 124.23/124.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 124.23/124.42 % SZS output start Refutation
% See solution above
% 124.23/124.43 ||#
% 124.23/124.43
% 124.23/124.43 ; Summary of computation:
% 124.23/124.43 ; 47771 formulas have been input or derived (from 645 formulas).
% 124.23/124.43 ; 29604 (62%) were retained. Of these,
% 124.23/124.43 ; 8039 (27%) were simplified or subsumed later,
% 124.23/124.43 ; 21565 (73%) are still being kept.
% 124.23/124.43 ;
% 124.23/124.43 ; Run time in seconds excluding printing time:
% 124.23/124.43 ; 0.151 0% Read assertion file (1 call)
% 124.23/124.43 ; 0.011 0% Assert (704 calls)
% 124.23/124.43 ; 6.659 5% Process new row (46,034 calls)
% 124.23/124.43 ; 4.083 3% Resolution (1,288 calls)
% 124.23/124.43 ; 0.378 0% Paramodulation (644 calls)
% 124.23/124.43 ; 0.000 0% Factoring (24 calls)
% 124.23/124.43 ; 1.198 1% Condensing (29,143 calls)
% 124.23/124.43 ; 76.914 62% Forward subsumption (29,143 calls)
% 124.23/124.43 ; 4.101 3% Backward subsumption (23,277 calls)
% 124.23/124.43 ; 3.397 3% Clause clause subsumption (595,073 calls)
% 124.23/124.43 ; 12.601 10% Forward simplification (45,471 calls)
% 124.23/124.43 ; 2.169 2% Backward simplification (29,562 calls)
% 124.23/124.43 ; 12.054 10% Ordering (346,366 calls)
% 124.23/124.43 ; 0.000 0% Sortal reasoning (32 calls)
% 124.23/124.43 ; 0.002 0% Purity testing (1 call)
% 124.23/124.43 ; 0.222 0% Other
% 124.23/124.43 ; 123.940 Total
% 124.23/124.43 ; 123.947 Real time
% 124.23/124.43 ;
% 124.23/124.44 ; Term-hash-array has 65,706 terms in all.
% 124.23/124.44 ; Feature-vector-row-index has 16,564 entries (16,565 at peak, 23,277 added, 6,713 deleted).
% 124.23/124.44 ; Feature-vector-row-index has 130,243 nodes (130,260 at peak, 178,300 added, 48,057 deleted).
% 124.23/124.44 ; Retrieved 1,435,383 possibly forward subsuming rows in 29,143 calls.
% 124.23/124.44 ; Retrieved 109,184 possibly backward subsumed rows in 23,277 calls.
% 124.23/124.44 ; Path-index has 56,127 entries (56,273 at peak, 74,682 added, 18,555 deleted).
% 124.23/124.44 ; Path-index has 86,469 nodes (86,701 at peak, 103,806 added, 17,337 deleted).
% 124.23/124.44 ; Trie-index has 56,127 entries (56,273 at peak, 74,682 added, 18,555 deleted).
% 124.23/124.44 ; Trie-index has 243,000 nodes (243,990 at peak, 395,927 added, 152,927 deleted).
% 124.23/124.44 ; Retrieved 1,507,513 generalization terms in 604,889 calls.
% 124.23/124.44 ; Retrieved 95,913 instance terms in 7,555 calls.
% 124.23/124.44 ; Retrieved 8,178,038 unifiable terms in 17,739 calls.
% 124.23/124.44 ;
% 124.23/124.44 ; The agenda of backward simplifiable rows to process has 52 entries:
% 124.23/124.44 ; 52 with value 0
% 124.23/124.44 ; The agenda of rows to process has 162 entries:
% 124.23/124.44 ; 53 with value 15 40 with value 18 2 with value 22
% 124.23/124.44 ; 24 with value 16 20 with value 19 1 with value 29
% 124.23/124.44 ; 20 with value 17 2 with value 21
% 124.23/124.44 ; The agenda of input rows to give has 1 entry:
% 124.23/124.44 ; 1 with value 5
% 124.23/124.44 ; The agenda of rows to give has 20984 entries:
% 124.23/124.44 ; 3 with value (4 9) 141 with value (4 93) 19 with value (4 177)
% 124.23/124.44 ; 3 with value (4 10) 134 with value (4 94) 29 with value (4 178)
% 124.23/124.44 ; 61 with value (4 11) 149 with value (4 95) 6 with value (4 179)
% 124.23/124.44 ; 107 with value (4 12) 139 with value (4 96) 14 with value (4 180)
% 124.23/124.44 ; 139 with value (4 13) 150 with value (4 97) 9 with value (4 181)
% 124.23/124.44 ; 282 with value (4 14) 110 with value (4 98) 23 with value (4 182)
% 124.23/124.44 ; 303 with value (4 15) 121 with value (4 99) 6 with value (4 183)
% 124.23/124.44 ; 329 with value (4 16) 137 with value (4 100) 9 with value (4 184)
% 124.23/124.44 ; 361 with value (4 17) 128 with value (4 101) 12 with value (4 185)
% 124.23/124.44 ; 361 with value (4 18) 123 with value (4 102) 25 with value (4 186)
% 124.23/124.44 ; 232 with value (4 19) 138 with value (4 103) 8 with value (4 187)
% 124.23/124.44 ; 166 with value (4 20) 126 with value (4 104) 7 with value (4 188)
% 124.23/124.44 ; 126 with value (4 21) 112 with value (4 105) 9 with value (4 189)
% 124.23/124.44 ; 105 with value (4 22) 99 with value (4 106) 17 with value (4 190)
% 124.23/124.44 ; 158 with value (4 23) 128 with value (4 107) 9 with value (4 191)
% 124.23/124.44 ; 112 with value (4 24) 126 with value (4 108) 3 with value (4 192)
% 124.23/124.44 ; 145 with value (4 25) 114 with value (4 109) 8 with value (4 193)
% 124.23/124.44 ; 128 with value (4 26) 84 with value (4 110) 5 with value (4 194)
% 124.23/124.44 ; 59 with value (4 27) 116 with value (4 111) 10 with value (4 195)
% 124.23/124.44 ; 93 with value (4 28) 102 with value (4 112) 5 with value (4 196)
% 124.23/124.44 ; 126 with value (4 29) 96 with value (4 113) 5 with value (4 197)
% 124.23/124.44 ; 127 with value (4 30) 77 with value (4 114) 7 with value (4 198)
% 124.23/124.44 ; 162 with value (4 31) 74 with value (4 115) 13 with value (4 199)
% 124.23/124.44 ; 196 with value (4 32) 74 with value (4 116) 5 with value (4 200)
% 124.23/124.44 ; 223 with value (4 33) 93 with value (4 117) 6 with value (4 201)
% 124.23/124.44 ; 275 with value (4 34) 97 with value (4 118) 3 with value (4 202)
% 124.23/124.44 ; 298 with value (4 35) 67 with value (4 119) 6 with value (4 203)
% 124.23/124.44 ; 365 with value (4 36) 79 with value (4 120) 1 with value (4 204)
% 124.23/124.44 ; 339 with value (4 37) 93 with value (4 121) 1 with value (4 205)
% 124.23/124.44 ; 392 with value (4 38) 95 with value (4 122) 2 with value (4 206)
% 124.23/124.44 ; 319 with value (4 39) 54 with value (4 123) 12 with value (4 207)
% 124.23/124.44 ; 205 with value (4 40) 91 with value (4 124) 4 with value (4 208)
% 124.23/124.44 ; 221 with value (4 41) 57 with value (4 125) 5 with value (4 209)
% 124.23/124.44 ; 210 with value (4 42) 83 with value (4 126) 2 with value (4 210)
% 124.23/124.44 ; 219 with value (4 43) 57 with value (4 127) 5 with value (4 211)
% 124.23/124.44 ; 194 with value (4 44) 78 with value (4 128) 3 with value (4 212)
% 124.23/124.44 ; 219 with value (4 45) 70 with value (4 129) 9 with value (4 213)
% 124.23/124.44 ; 190 with value (4 46) 58 with value (4 130) 1 with value (4 214)
% 124.23/124.44 ; 151 with value (4 47) 54 with value (4 131) 2 with value (4 215)
% 124.23/124.44 ; 158 with value (4 48) 46 with value (4 132) 1 with value (4 216)
% 124.23/124.44 ; 207 with value (4 49) 58 with value (4 133) 4 with value (4 217)
% 124.23/124.44 ; 160 with value (4 50) 46 with value (4 134) 6 with value (4 220)
% 124.23/124.44 ; 173 with value (4 51) 77 with value (4 135) 2 with value (4 221)
% 124.23/124.44 ; 150 with value (4 52) 32 with value (4 136) 2 with value (4 222)
% 124.23/124.44 ; 202 with value (4 53) 50 with value (4 137) 8 with value (4 223)
% 124.23/124.44 ; 190 with value (4 54) 61 with value (4 138) 1 with value (4 224)
% 124.23/124.44 ; 145 with value (4 55) 69 with value (4 139) 1 with value (4 225)
% 124.23/124.44 ; 181 with value (4 56) 50 with value (4 140) 3 with value (4 226)
% 124.23/124.44 ; 142 with value (4 57) 59 with value (4 141) 2 with value (4 228)
% 124.23/124.44 ; 118 with value (4 58) 53 with value (4 142) 4 with value (4 229)
% 124.23/124.44 ; 163 with value (4 59) 43 with value (4 143) 2 with value (4 230)
% 124.23/124.44 ; 162 with value (4 60) 47 with value (4 144) 6 with value (4 233)
% 124.23/124.44 ; 191 with value (4 61) 38 with value (4 145) 3 with value (4 234)
% 124.23/124.44 ; 159 with value (4 62) 45 with value (4 146) 3 with value (4 235)
% 124.23/124.44 ; 189 with value (4 63) 45 with value (4 147) 2 with value (4 240)
% 124.23/124.44 ; 214 with value (4 64) 42 with value (4 148) 1 with value (4 242)
% 124.23/124.44 ; 192 with value (4 65) 24 with value (4 149) 1 with value (4 244)
% 124.23/124.44 ; 187 with value (4 66) 42 with value (4 150) 1 with value (4 248)
% 124.23/124.44 ; 166 with value (4 67) 34 with value (4 151) 1 with value (4 249)
% 124.23/124.44 ; 140 with value (4 68) 44 with value (4 152) 1 with value (4 253)
% 124.23/124.44 ; 166 with value (4 69) 47 with value (4 153) 3 with value (4 255)
% 124.23/124.44 ; 176 with value (4 70) 45 with value (4 154) 1 with value (4 256)
% 124.23/124.44 ; 170 with value (4 71) 27 with value (4 155) 1 with value (4 258)
% 124.23/124.44 ; 191 with value (4 72) 51 with value (4 156) 1 with value (4 268)
% 124.23/124.44 ; 143 with value (4 73) 35 with value (4 157) 1 with value (4 275)
% 124.23/124.44 ; 180 with value (4 74) 28 with value (4 158) 1 with value (4 280)
% 124.23/124.44 ; 193 with value (4 75) 27 with value (4 159) 1 with value (4 283)
% 124.23/124.44 ; 177 with value (4 76) 56 with value (4 160) 1 with value (4 284)
% 124.23/124.44 ; 132 with value (4 77) 30 with value (4 161) 1 with value (4 290)
% 124.23/124.44 ; 147 with value (4 78) 19 with value (4 162) 1 with value (4 302)
% 124.23/124.44 ; 136 with value (4 79) 17 with value (4 163) 2 with value (4 332)
% 124.23/124.44 ; 173 with value (4 80) 23 with value (4 164) 2 with value (4 344)
% 124.23/124.44 ; 143 with value (4 81) 22 with value (4 165) 1 with value (4 354)
% 124.23/124.44 ; 114 with value (4 82) 21 with value (4 166) 1 with value (4 419)
% 124.23/124.44 ; 160 with value (4 83) 23 with value (4 167) 1 with value (4 469)
% 124.23/124.44 ; 142 with value (4 84) 26 with value (4 168) 2 with value (4 471)
% 124.23/124.44 ; 126 with value (4 85) 28 with value (4 169) 1 with value (4 487)
% 124.23/124.44 ; 138 with value (4 86) 28 with value (4 170) 1 with value (4 490)
% 124.23/124.44 ; 145 with value (4 87) 20 with value (4 171) 1 with value (4 576)
% 124.23/124.44 ; 134 with value (4 88) 38 with value (4 172) 1 with value (4 645)
% 124.23/124.44 ; 143 with value (4 89) 21 with value (4 173) 1 with value (4 698)
% 124.23/124.44 ; 122 with value (4 90) 24 with value (4 174) 1 with value (4 716)
% 124.23/124.44 ; 182 with value (4 91) 11 with value (4 175) 1 with value (4 997)
% 124.23/124.44 ; 142 with value (4 92) 11 with value (4 176) 1 with value (4 1120)
% 124.23/124.44 Evaluation took:
% 124.23/124.44 123.961 seconds of real time
% 124.23/124.44 119.00007 seconds of user run time
% 124.23/124.44 4.95723 seconds of system run time
% 124.23/124.44 [Run times include 32.52 seconds GC run time.]
% 124.23/124.44 0 calls to %EVAL
% 124.23/124.44 0 page faults and
% 124.23/124.44 10,759,329,376 bytes consed.
% 124.23/124.44 :PROOF-FOUND
% 124.23/124.44 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-14T17:04:15
% 124.23/124.44 :PROOF-FOUND
% 124.23/124.44 *
%------------------------------------------------------------------------------