%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWW470_2 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n018.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 : Thu Jul 21 01:25:08 EDT 2022
% Result : Theorem 105.10s 105.36s
% Output : Refutation 105.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 15 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 191 ( 8 equ)
% Maximal formula atoms : 2 ( 12 avg)
% Number of connectives : 6 ( 4 ~; 2 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 174 ( 174 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 60 ( 58 usr; 32 prp; 0-4 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 23 ( 0 sgn 23 !; 0 ?; 23 :)
% Comments :
%------------------------------------------------------------------------------
tff(19,axiom,
! [X: fun_a_fun_state_bool,Y: fun_Ho287446294a_bool,Z: com,U: fun_a_fun_state_bool] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X,'SKOLEMAABG1.x_a'(X,Y,Z,U)),'SKOLEMAABG2.state'(X,Y,Z,U)))
| hBOOL(hAPP_f2063540982l_bool(hoare_1546678894rivs_a(Y),hAPP_f909437487a_bool(hAPP_H762155206a_bool(insert1051021594iple_a,hoare_196563068iple_a(X,Z,U)),bot_bo1766443648a_bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_escape) ).
tff(49,axiom,
! [X: hoare_1544627872iple_a] : ( collec445968053iple_a(hAPP_H1472549281a_bool(fequal1057774495iple_a,X)) = hAPP_f909437487a_bool(hAPP_H762155206a_bool(insert1051021594iple_a,X),bot_bo1766443648a_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_singleton__conv2) ).
tff(347,axiom,
! [X: fun_Ho287446294a_bool] : ( collec445968053iple_a(X) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_Collect__def) ).
tff(1023,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
tff(1035,axiom,
! [X: bool,Y: state] : ( hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X),Y) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) ).
tff(1041,axiom,
! [X: fun_state_bool,Y: x_a] : ( hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X),Y) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) ).
tff(1103,axiom,
! [X: fun_fu1441721944l_bool,Y: fun_Ho965678415a_bool,Z: hoare_1544627872iple_a] : ( hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,X),Y),Z) = hAPP_f2063540982l_bool(X,hAPP_H1472549281a_bool(Y,Z)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBB_1_1_COMBB_000tc__fun_Itc__Hoare____Mirabelle____xlrqixeqwe__Otriple_I) ).
tff(1110,axiom,
! [X: fun_Ho611385006a_bool,Y: fun_Ho287446294a_bool,Z: hoare_1544627872iple_a] : ( hAPP_H1472549281a_bool(hAPP_f693853672a_bool(hAPP_f1399402097a_bool(cOMBC_894585277a_bool,X),Y),Z) = hAPP_f909437487a_bool(hAPP_H762155206a_bool(X,Z),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_COMBC_000tc__Hoare____Mirabelle____xlrqixeqwe__Otriple_It__a_J_00_235) ).
tff(1116,negated_conjecture,
~ hBOOL(hAPP_f2063540982l_bool(hoare_1546678894rivs_a(g),hAPP_f909437487a_bool(hAPP_H762155206a_bool(insert1051021594iple_a,hoare_196563068iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1766443648a_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(1117,plain,
~ hBOOL(hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,hoare_1546678894rivs_a(g)),hAPP_f693853672a_bool(hAPP_f1399402097a_bool(cOMBC_894585277a_bool,insert1051021594iple_a),bot_bo1766443648a_bool)),hoare_196563068iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))),
inference('REWRITE',[status(thm)],[1116,1103,1110,theory(equality)]) ).
tff(1312,plain,
! [X: hoare_1544627872iple_a] : ( hAPP_H1472549281a_bool(fequal1057774495iple_a,X) = hAPP_H1472549281a_bool(hAPP_f693853672a_bool(hAPP_f1399402097a_bool(cOMBC_894585277a_bool,insert1051021594iple_a),bot_bo1766443648a_bool),X) ),
inference('REWRITE',[status(thm)],[49,1110,347,theory(equality)]) ).
tff(1365,plain,
! [X: fun_a_fun_state_bool,Y: fun_Ho287446294a_bool,Z: com,U: fun_a_fun_state_bool] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X,'SKOLEMAABG1.x_a'(X,Y,Z,U)),'SKOLEMAABG2.state'(X,Y,Z,U)))
| hBOOL(hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,hoare_1546678894rivs_a(Y)),fequal1057774495iple_a),hoare_196563068iple_a(X,Z,U))) ),
inference('REWRITE',[status(thm)],[19,1103,347,49,theory(equality)]) ).
tff(5114,plain,
! [X: fun_fu1441721944l_bool,Y: hoare_1544627872iple_a] : ( hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,X),hAPP_f693853672a_bool(hAPP_f1399402097a_bool(cOMBC_894585277a_bool,insert1051021594iple_a),bot_bo1766443648a_bool)),Y) = hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,X),fequal1057774495iple_a),Y) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[1103,1312,theory(equality)]),1103,theory(equality)]) ).
tff(5124,plain,
~ hBOOL(hAPP_H2006434664a_bool(hAPP_f1726109544a_bool(hAPP_f1948079815a_bool(cOMBB_1474127043iple_a,hoare_1546678894rivs_a(g)),fequal1057774495iple_a),hoare_196563068iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))),
inference('REWRITE',[status(thm)],[1117,5114,theory(equality)]) ).
cnf(22744,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[1365,5124]),1023,1035,1041,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.13 % Problem : SWW470_2 : TPTP v8.1.0. Released v5.3.0.
% 0.10/0.14 % Command : run-snark %s %d
% 0.15/0.35 % Computer : n018.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 600
% 0.15/0.35 % DateTime : Sun Jun 5 13:38:18 EDT 2022
% 0.15/0.35 % CPUTime :
% 0.21/0.50 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.52 *
% 0.21/0.52 *
% 0.21/0.52 #<PACKAGE "SNARK-USER">
% 0.21/0.52 *
% 0.21/0.52 SNARK-TPTP-OPTIONS
% 0.21/0.52 *
% 0.21/0.53 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.53 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.53 (USE-FACTORING :POS)
% 0.21/0.53 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.53 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.53 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.53 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.53 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.53 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.53 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.53 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.53 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.53 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.53 *
% 0.21/0.53 "."
% 0.21/0.53 *
% 0.21/0.53 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-05T13:38:19
% 0.21/0.53 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n018.cluster.edu at 2022-06-05T13:38:19
% 105.10/105.36
% 105.10/105.36
% 105.10/105.36 #||
% 105.10/105.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 105.10/105.36 % SZS output start Refutation
% See solution above
% 105.10/105.37 ||#
% 105.10/105.37
% 105.10/105.37 ; Summary of computation:
% 105.10/105.37 ; 65946 formulas have been input or derived (from 854 formulas).
% 105.10/105.37 ; 22744 (34%) were retained. Of these,
% 105.10/105.37 ; 1722 ( 8%) were simplified or subsumed later,
% 105.10/105.37 ; 21022 (92%) are still being kept.
% 105.10/105.37 ;
% 105.10/105.37 ; Run time in seconds excluding printing time:
% 105.10/105.37 ; 0.388 0% Read assertion file (1 call)
% 105.10/105.37 ; 0.043 0% Assert (802 calls)
% 105.10/105.37 ; 8.060 8% Process new row (63,540 calls)
% 105.10/105.37 ; 11.174 11% Resolution (1,706 calls)
% 105.10/105.37 ; 0.206 0% Paramodulation (853 calls)
% 105.10/105.37 ; 0.000 0% Factoring (77 calls)
% 105.10/105.37 ; 0.747 1% Condensing (27,639 calls)
% 105.10/105.37 ; 63.336 60% Forward subsumption (27,639 calls)
% 105.10/105.37 ; 3.841 4% Backward subsumption (18,199 calls)
% 105.10/105.37 ; 1.077 1% Clause clause subsumption (44,034 calls)
% 105.10/105.37 ; 9.530 9% Forward simplification (63,327 calls)
% 105.10/105.37 ; 0.642 1% Backward simplification (22,596 calls)
% 105.10/105.37 ; 4.555 4% Ordering (388,137 calls)
% 105.10/105.37 ; 0.679 1% Sortal reasoning (642,181 calls)
% 105.10/105.37 ; 0.002 0% Purity testing (1 call)
% 105.10/105.37 ; 0.481 0% Other
% 105.10/105.37 ; 104.761 Total
% 105.10/105.37 ; 104.840 Real time
% 105.10/105.37 ;
% 105.10/105.41 ; Term-hash-array has 68,007 terms in all.
% 105.10/105.41 ; Feature-vector-row-index has 17,435 entries (17,435 at peak, 18,199 added, 764 deleted).
% 105.10/105.41 ; Feature-vector-row-index has 401,907 nodes (401,907 at peak, 412,991 added, 11,084 deleted).
% 105.10/105.41 ; Retrieved 106,862 possibly forward subsuming rows in 27,639 calls.
% 105.10/105.41 ; Retrieved 2,442 possibly backward subsumed rows in 18,199 calls.
% 105.10/105.41 ; Path-index has 64,633 entries (64,633 at peak, 68,860 added, 4,227 deleted).
% 105.10/105.41 ; Path-index has 146,565 nodes (146,565 at peak, 150,306 added, 3,741 deleted).
% 105.10/105.41 ; Trie-index has 64,633 entries (64,633 at peak, 68,860 added, 4,227 deleted).
% 105.10/105.41 ; Trie-index has 342,682 nodes (342,682 at peak, 358,794 added, 16,112 deleted).
% 105.10/105.41 ; Retrieved 410,689 generalization terms in 850,027 calls.
% 105.10/105.41 ; Retrieved 8,952 instance terms in 5,161 calls.
% 105.10/105.41 ; Retrieved 4,995,949 unifiable terms in 18,613 calls.
% 105.10/105.41 ;
% 105.10/105.41 ; The agenda of rows to process has 9 entries:
% 105.10/105.41 ; 1 with value 73 1 with value 78 2 with value 112
% 105.10/105.41 ; 1 with value 77 4 with value 82
% 105.10/105.41 ; The agenda of input rows to give has 87 entries:
% 105.10/105.41 ; 7 with value 44 4 with value 53 1 with value 62
% 105.10/105.41 ; 6 with value 45 6 with value 54 1 with value 64
% 105.10/105.41 ; 9 with value 46 2 with value 55 1 with value 65
% 105.10/105.41 ; 7 with value 47 3 with value 56 1 with value 66
% 105.10/105.41 ; 8 with value 48 1 with value 58 1 with value 69
% 105.10/105.41 ; 1 with value 49 1 with value 59 1 with value 75
% 105.10/105.41 ; 5 with value 50 8 with value 60 1 with value 92
% 105.10/105.41 ; 1 with value 51 2 with value 61 1 with value 94
% 105.10/105.41 ; 8 with value 52
% 105.10/105.41 ; The agenda of rows to give has 20116 entries:
% 105.10/105.41 ; 4 with value (4 7) 185 with value (4 68) 24 with value (4 129)
% 105.10/105.41 ; 5 with value (4 8) 212 with value (4 69) 13 with value (4 130)
% 105.10/105.41 ; 7 with value (4 9) 181 with value (4 70) 15 with value (4 131)
% 105.10/105.41 ; 37 with value (4 10) 147 with value (4 71) 26 with value (4 132)
% 105.10/105.41 ; 32 with value (4 11) 138 with value (4 72) 8 with value (4 133)
% 105.10/105.41 ; 40 with value (4 12) 139 with value (4 73) 16 with value (4 134)
% 105.10/105.41 ; 67 with value (4 13) 123 with value (4 74) 16 with value (4 135)
% 105.10/105.41 ; 57 with value (4 14) 126 with value (4 75) 24 with value (4 136)
% 105.10/105.41 ; 110 with value (4 15) 102 with value (4 76) 13 with value (4 137)
% 105.10/105.41 ; 158 with value (4 16) 98 with value (4 77) 16 with value (4 138)
% 105.10/105.41 ; 116 with value (4 17) 120 with value (4 78) 25 with value (4 139)
% 105.10/105.41 ; 118 with value (4 18) 118 with value (4 79) 13 with value (4 140)
% 105.10/105.41 ; 134 with value (4 19) 82 with value (4 80) 12 with value (4 141)
% 105.10/105.41 ; 234 with value (4 20) 114 with value (4 81) 13 with value (4 142)
% 105.10/105.41 ; 139 with value (4 21) 104 with value (4 82) 11 with value (4 143)
% 105.10/105.41 ; 183 with value (4 22) 94 with value (4 83) 8 with value (4 144)
% 105.10/105.41 ; 197 with value (4 23) 125 with value (4 84) 7 with value (4 145)
% 105.10/105.41 ; 199 with value (4 24) 97 with value (4 85) 11 with value (4 146)
% 105.10/105.41 ; 307 with value (4 25) 69 with value (4 86) 11 with value (4 147)
% 105.10/105.41 ; 258 with value (4 26) 80 with value (4 87) 6 with value (4 148)
% 105.10/105.41 ; 305 with value (4 27) 77 with value (4 88) 15 with value (4 149)
% 105.10/105.41 ; 304 with value (4 28) 53 with value (4 89) 8 with value (4 150)
% 105.10/105.41 ; 304 with value (4 29) 58 with value (4 90) 4 with value (4 151)
% 105.10/105.41 ; 327 with value (4 30) 63 with value (4 91) 11 with value (4 152)
% 105.10/105.41 ; 304 with value (4 31) 68 with value (4 92) 18 with value (4 153)
% 105.10/105.41 ; 326 with value (4 32) 44 with value (4 93) 2 with value (4 154)
% 105.10/105.41 ; 400 with value (4 33) 47 with value (4 94) 4 with value (4 155)
% 105.10/105.41 ; 433 with value (4 34) 40 with value (4 95) 10 with value (4 156)
% 105.10/105.41 ; 439 with value (4 35) 37 with value (4 96) 4 with value (4 157)
% 105.10/105.41 ; 337 with value (4 36) 57 with value (4 97) 12 with value (4 158)
% 105.10/105.41 ; 478 with value (4 37) 54 with value (4 98) 9 with value (4 159)
% 105.10/105.41 ; 369 with value (4 38) 50 with value (4 99) 12 with value (4 160)
% 105.10/105.41 ; 389 with value (4 39) 53 with value (4 100) 3 with value (4 161)
% 105.10/105.41 ; 401 with value (4 40) 65 with value (4 101) 3 with value (4 162)
% 105.10/105.41 ; 359 with value (4 41) 47 with value (4 102) 8 with value (4 163)
% 105.10/105.41 ; 386 with value (4 42) 60 with value (4 103) 1 with value (4 164)
% 105.10/105.41 ; 358 with value (4 43) 55 with value (4 104) 1 with value (4 165)
% 105.10/105.41 ; 423 with value (4 44) 60 with value (4 105) 2 with value (4 166)
% 105.10/105.41 ; 387 with value (4 45) 42 with value (4 106) 1 with value (4 167)
% 105.10/105.41 ; 361 with value (4 46) 37 with value (4 107) 1 with value (4 168)
% 105.10/105.41 ; 336 with value (4 47) 70 with value (4 108) 3 with value (4 169)
% 105.10/105.41 ; 381 with value (4 48) 45 with value (4 109) 2 with value (4 170)
% 105.10/105.41 ; 435 with value (4 49) 36 with value (4 110) 4 with value (4 171)
% 105.10/105.41 ; 345 with value (4 50) 37 with value (4 111) 1 with value (4 172)
% 105.10/105.41 ; 280 with value (4 51) 62 with value (4 112) 5 with value (4 173)
% 105.10/105.41 ; 267 with value (4 52) 45 with value (4 113) 1 with value (4 174)
% 105.10/105.41 ; 328 with value (4 53) 29 with value (4 114) 2 with value (4 175)
% 105.10/105.41 ; 330 with value (4 54) 48 with value (4 115) 5 with value (4 177)
% 105.10/105.41 ; 316 with value (4 55) 24 with value (4 116) 2 with value (4 179)
% 105.10/105.41 ; 333 with value (4 56) 20 with value (4 117) 1 with value (4 180)
% 105.10/105.41 ; 292 with value (4 57) 48 with value (4 118) 2 with value (4 181)
% 105.10/105.41 ; 257 with value (4 58) 35 with value (4 119) 3 with value (4 182)
% 105.10/105.41 ; 215 with value (4 59) 28 with value (4 120) 4 with value (4 184)
% 105.10/105.41 ; 192 with value (4 60) 26 with value (4 121) 2 with value (4 187)
% 105.10/105.41 ; 210 with value (4 61) 42 with value (4 122) 1 with value (4 190)
% 105.10/105.41 ; 185 with value (4 62) 35 with value (4 123) 1 with value (4 196)
% 105.10/105.41 ; 195 with value (4 63) 25 with value (4 124) 1 with value (4 202)
% 105.10/105.41 ; 212 with value (4 64) 37 with value (4 125) 1 with value (4 203)
% 105.10/105.41 ; 198 with value (4 65) 22 with value (4 126) 1 with value (4 206)
% 105.10/105.41 ; 125 with value (4 66) 14 with value (4 127) 1 with value (4 208)
% 105.10/105.41 ; 161 with value (4 67) 22 with value (4 128)
% 105.10/105.41 Evaluation took:
% 105.10/105.41 104.882 seconds of real time
% 105.10/105.41 99.940926 seconds of user run time
% 105.10/105.41 4.864185 seconds of system run time
% 105.10/105.41 [Run times include 30.161 seconds GC run time.]
% 105.10/105.41 0 calls to %EVAL
% 105.10/105.41 0 page faults and
% 105.10/105.41 8,431,050,744 bytes consed.
% 105.10/105.41 :PROOF-FOUND
% 105.10/105.41 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-05T13:40:04
% 105.10/105.41 :PROOF-FOUND
% 105.10/105.41 *
%------------------------------------------------------------------------------