%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : PUZ135_2 : TPTP v8.1.0. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n024.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 : Mon Jul 18 18:26:55 EDT 2022
% Result : Theorem 0.70s 0.90s
% Output : Refutation 0.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 25
% Syntax : Number of formulae : 86 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 557 ( 152 equ)
% Maximal formula atoms : 7 ( 6 avg)
% Number of connectives : 138 ( 71 ~; 67 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 404 ( 404 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 16 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 16 ( 0 sgn 16 !; 0 ?; 16 :)
% Comments :
%------------------------------------------------------------------------------
tff(1,axiom,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_b) ).
tff(2,axiom,
a != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_c) ).
tff(3,axiom,
a != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_d) ).
tff(4,axiom,
b != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_c) ).
tff(5,axiom,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_d) ).
tff(6,axiom,
c != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_d) ).
tff(20,axiom,
! [X: entry] :
( ( X = collage_painting )
| ( X = holography )
| ( X = laser_etching )
| ( X = reconstituted_materials_sculpture ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_entries) ).
tff(21,axiom,
! [X: place] :
( ( X = first )
| ( X = second )
| ( X = third )
| ( X = fourth ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_places) ).
tff(22,axiom,
! [X: knowheyan,Y: knowheyan] :
( ( X = Y )
| ( entry_of(X) != entry_of(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_entrys) ).
tff(23,axiom,
! [X: knowheyan,Y: knowheyan] :
( ( X = Y )
| ( place_of(X) != place_of(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_places) ).
tff(24,axiom,
place_of(a) != first,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_info) ).
tff(25,axiom,
entry_of(a) != holography,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_info) ).
tff(26,axiom,
! [X: knowheyan] :
( ( place_of(X) != fourth )
| ( entry_of(X) != reconstituted_materials_sculpture ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fourth_info) ).
tff(27,axiom,
! [X: knowheyan] :
( ( place_of(X) != fourth )
| ( entry_of(X) != holography ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fourth_info) ).
tff(28,axiom,
! [X: knowheyan] :
( ( entry_of(X) != collage_painting )
| ( X != a ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',collage_info) ).
tff(29,axiom,
! [X: knowheyan] :
( ( entry_of(X) != collage_painting )
| ( X != c ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',collage_info) ).
tff(31,axiom,
! [X: knowheyan] :
( ( entry_of(X) != collage_painting )
| ( place_of(X) != second ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',collage_info) ).
tff(32,axiom,
place_of(b) != fourth,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fourth_info2) ).
tff(33,axiom,
! [X: knowheyan] :
( ( entry_of(X) != laser_etching )
| ( place_of(X) != fourth ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fourth_info2) ).
tff(34,axiom,
place_of(b) != third,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',third_info) ).
tff(35,axiom,
place_of(c) != third,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',third_info) ).
tff(36,axiom,
entry_of(b) != laser_etching,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',laser_etching_info) ).
tff(37,axiom,
! [X: knowheyan] :
( ( entry_of(X) != laser_etching )
| ( X != a ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',laser_etching_info) ).
tff(38,axiom,
! [X: knowheyan] :
( ( entry_of(X) != laser_etching )
| ( place_of(X) != second ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',laser_etching_info) ).
tff(39,negated_conjecture,
( ( place_of(a) != third )
| ( place_of(b) != second )
| ( place_of(c) != first )
| ( place_of(d) != fourth ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',places) ).
tff(40,plain,
entry_of(a) != collage_painting,
inference('UR-RESOLVE',[status(thm)],[28,theory(equality)]) ).
tff(41,plain,
entry_of(c) != collage_painting,
inference('UR-RESOLVE',[status(thm)],[29,theory(equality)]) ).
tff(42,plain,
entry_of(a) != laser_etching,
inference('UR-RESOLVE',[status(thm)],[37,theory(equality)]) ).
tff(43,plain,
entry_of(a) != entry_of(d),
inference('UR-RESOLVE',[status(thm)],[22,3]) ).
tff(44,plain,
entry_of(b) != entry_of(d),
inference('UR-RESOLVE',[status(thm)],[22,5]) ).
tff(45,plain,
entry_of(c) != entry_of(d),
inference('UR-RESOLVE',[status(thm)],[22,6]) ).
tff(46,plain,
entry_of(a) != entry_of(c),
inference('UR-RESOLVE',[status(thm)],[22,2]) ).
tff(47,plain,
entry_of(b) != entry_of(c),
inference('UR-RESOLVE',[status(thm)],[22,4]) ).
tff(48,plain,
entry_of(a) != entry_of(b),
inference('UR-RESOLVE',[status(thm)],[22,1]) ).
tff(49,plain,
place_of(a) != place_of(d),
inference('UR-RESOLVE',[status(thm)],[23,3]) ).
tff(50,plain,
place_of(b) != place_of(d),
inference('UR-RESOLVE',[status(thm)],[23,5]) ).
tff(51,plain,
place_of(c) != place_of(d),
inference('UR-RESOLVE',[status(thm)],[23,6]) ).
tff(52,plain,
place_of(a) != place_of(c),
inference('UR-RESOLVE',[status(thm)],[23,2]) ).
tff(53,plain,
place_of(b) != place_of(c),
inference('UR-RESOLVE',[status(thm)],[23,4]) ).
tff(54,plain,
place_of(a) != place_of(b),
inference('UR-RESOLVE',[status(thm)],[23,1]) ).
tff(58,plain,
( ( place_of(b) = first )
| ( place_of(b) = second ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[34,21]),32]) ).
tff(59,plain,
( ( place_of(c) = first )
| ( place_of(c) = second )
| ( place_of(c) = fourth ) ),
inference('HYPERRESOLVE',[status(thm)],[35,21]) ).
tff(62,plain,
! [X: place,Y: place] :
( ( X = first )
| ( X = second )
| ( X = fourth )
| ( Y = first )
| ( Y = second )
| ( Y = X )
| ( Y = fourth ) ),
inference('PARAMODULATE',[status(thm)],[21,21,theory(equality)]) ).
tff(65,plain,
entry_of(a) = reconstituted_materials_sculpture,
inference('UR-RESOLVE',[status(thm)],[20,42,40,25]) ).
tff(66,plain,
reconstituted_materials_sculpture != entry_of(d),
inference('REWRITE',[status(thm)],[43,65,theory(equality)]) ).
tff(67,plain,
reconstituted_materials_sculpture != entry_of(c),
inference('REWRITE',[status(thm)],[46,65,theory(equality)]) ).
tff(68,plain,
reconstituted_materials_sculpture != entry_of(b),
inference('REWRITE',[status(thm)],[48,65,theory(equality)]) ).
tff(69,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(d) = holography )
| ( entry_of(d) = laser_etching ) ),
inference('HYPERRESOLVE',[status(thm)],[66,20]) ).
tff(72,plain,
( ( entry_of(c) = holography )
| ( entry_of(c) = laser_etching ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[67,20]),41]) ).
tff(74,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(b) = holography ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[68,20]),36]) ).
tff(76,plain,
place_of(a) != fourth,
inference('UR-RESOLVE',[status(thm)],[26,65]) ).
tff(78,plain,
( ( place_of(b) = first )
| ( place_of(a) != second ) ),
inference('PARAMODULATE',[status(thm)],[54,58,theory(equality)]) ).
tff(80,plain,
( ( place_of(b) = first )
| ( second != place_of(d) ) ),
inference('PARAMODULATE',[status(thm)],[50,58,theory(equality)]) ).
tff(81,plain,
( ( place_of(b) = first )
| ( entry_of(b) != collage_painting ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[31,58,theory(equality)]),theory(equality)]) ).
tff(83,plain,
( ( place_of(b) = first )
| ( place_of(a) != third )
| ( place_of(c) != first )
| ( place_of(d) != fourth ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[39,58,theory(equality)]),theory(equality)]) ).
tff(96,plain,
( ( place_of(c) = first )
| ( place_of(c) = fourth )
| ( entry_of(c) = holography ) ),
inference('HYPERRESOLVE',[status(thm)],[38,59,72]) ).
tff(103,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(d) = holography )
| ( place_of(d) != fourth ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[33,69,theory(equality)]),theory(equality)]) ).
tff(105,plain,
( ( place_of(c) = first )
| ( entry_of(c) = holography ) ),
inference('HYPERRESOLVE',[status(thm)],[33,96,72]) ).
tff(106,plain,
( ( entry_of(c) = holography )
| ( place_of(b) != first ) ),
inference('PARAMODULATE',[status(thm)],[53,105,theory(equality)]) ).
tff(107,plain,
( ( entry_of(c) = holography )
| ( first != place_of(d) ) ),
inference('PARAMODULATE',[status(thm)],[51,105,theory(equality)]) ).
tff(170,plain,
( ( first = place_of(d) )
| ( second = place_of(d) )
| ( place_of(d) = fourth )
| ( place_of(a) = second ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[49,62]),76,24]) ).
tff(198,plain,
( ( first = place_of(d) )
| ( place_of(d) = fourth )
| ( place_of(a) = second )
| ( place_of(b) = first ) ),
inference('HYPERRESOLVE',[status(thm)],[80,170]) ).
tff(201,plain,
( ( first = place_of(d) )
| ( place_of(d) = fourth )
| ( place_of(a) = second )
| ( entry_of(d) != laser_etching ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[38,170,theory(equality)]),theory(equality)]) ).
tff(227,plain,
( ( first = place_of(d) )
| ( place_of(a) = second )
| ( place_of(b) = first )
| ( entry_of(c) = holography ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[83,198,21,105]),76,24]) ).
tff(261,plain,
( ( place_of(a) = second )
| ( place_of(b) = first )
| ( entry_of(c) = holography ) ),
inference('HYPERRESOLVE',[status(thm)],[107,227]) ).
tff(262,plain,
( ( place_of(a) = second )
| ( entry_of(c) = holography ) ),
inference('HYPERRESOLVE',[status(thm)],[106,261]) ).
tff(263,plain,
( ( entry_of(c) = holography )
| ( place_of(b) = first ) ),
inference('HYPERRESOLVE',[status(thm)],[78,262]) ).
tff(267,plain,
entry_of(c) = holography,
inference('HYPERRESOLVE',[status(thm)],[106,263]) ).
tff(268,plain,
entry_of(d) != holography,
inference('REWRITE',[status(thm)],[45,267,theory(equality)]) ).
tff(269,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(d) = laser_etching ) ),
inference('REWRITE',[status(thm)],[69,268]) ).
tff(271,plain,
( ( entry_of(d) = collage_painting )
| ( place_of(d) != fourth ) ),
inference('REWRITE',[status(thm)],[103,268]) ).
tff(281,plain,
entry_of(b) != holography,
inference('REWRITE',[status(thm)],[47,267,theory(equality)]) ).
tff(282,plain,
entry_of(b) = collage_painting,
inference('REWRITE',[status(thm)],[74,281]) ).
tff(283,plain,
entry_of(d) != collage_painting,
inference('REWRITE',[status(thm)],[44,282,theory(equality)]) ).
tff(284,plain,
entry_of(d) = laser_etching,
inference('REWRITE',[status(thm)],[269,283]) ).
tff(286,plain,
( ( first = place_of(d) )
| ( place_of(d) = fourth )
| ( place_of(a) = second ) ),
inference('REWRITE',[status(thm)],[201,284,theory(equality)]) ).
tff(289,plain,
place_of(d) != fourth,
inference('REWRITE',[status(thm)],[271,283]) ).
tff(293,plain,
( ( first = place_of(d) )
| ( place_of(a) = second ) ),
inference('REWRITE',[status(thm)],[286,289]) ).
tff(300,plain,
place_of(b) = first,
inference('REWRITE',[status(thm)],[81,282,theory(equality)]) ).
tff(301,plain,
first != place_of(d),
inference('REWRITE',[status(thm)],[50,300,theory(equality)]) ).
tff(303,plain,
place_of(a) = second,
inference('REWRITE',[status(thm)],[293,301]) ).
tff(304,plain,
place_of(c) != second,
inference('REWRITE',[status(thm)],[52,303,theory(equality)]) ).
tff(305,plain,
( ( place_of(c) = first )
| ( place_of(c) = fourth ) ),
inference('REWRITE',[status(thm)],[59,304]) ).
tff(309,plain,
place_of(c) != first,
inference('REWRITE',[status(thm)],[53,300,theory(equality)]) ).
tff(310,plain,
place_of(c) = fourth,
inference('REWRITE',[status(thm)],[305,309]) ).
cnf(313,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[27,310]),267,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ135_2 : TPTP v8.1.0. Released v5.1.0.
% 0.03/0.13 % Command : run-snark %s %d
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Sat May 28 19:51:52 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.21/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.46 *
% 0.21/0.46 *
% 0.21/0.47 #<PACKAGE "SNARK-USER">
% 0.21/0.47 *
% 0.21/0.47 SNARK-TPTP-OPTIONS
% 0.21/0.47 *
% 0.21/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.47 (USE-FACTORING :POS)
% 0.21/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.47 *
% 0.21/0.47 "."
% 0.21/0.47 *
% 0.21/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-05-28T19:51:52
% 0.21/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n024.cluster.edu at 2022-05-28T19:51:52
% 0.70/0.90
% 0.70/0.90
% 0.70/0.90 #||
% 0.70/0.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.70/0.90 % SZS output start Refutation
% See solution above
% 0.70/0.91 ||#
% 0.70/0.91
% 0.70/0.91 ; Summary of computation:
% 0.70/0.91 ; 1803 formulas have been input or derived (from 142 formulas).
% 0.70/0.91 ; 313 (17%) were retained. Of these,
% 0.70/0.91 ; 239 (76%) were simplified or subsumed later,
% 0.70/0.91 ; 74 (24%) are still being kept.
% 0.70/0.91 ;
% 0.70/0.91 ; Run time in seconds excluding printing time:
% 0.70/0.91 ; 0.006 1% Read assertion file (1 call)
% 0.70/0.91 ; 0.001 0% Assert (30 calls)
% 0.70/0.91 ; 0.040 9% Process new row (1,608 calls)
% 0.70/0.91 ; 0.114 26% Resolution (282 calls)
% 0.70/0.91 ; 0.026 6% Paramodulation (141 calls)
% 0.70/0.91 ; 0.001 0% Factoring (27 calls)
% 0.70/0.91 ; 0.019 4% Condensing (691 calls)
% 0.70/0.91 ; 0.061 14% Forward subsumption (691 calls)
% 0.70/0.91 ; 0.005 1% Backward subsumption (254 calls)
% 0.70/0.91 ; 0.013 3% Clause clause subsumption (616 calls)
% 0.70/0.91 ; 0.071 16% Forward simplification (1,444 calls)
% 0.70/0.91 ; 0.010 2% Backward simplification (313 calls)
% 0.70/0.91 ; 0.025 6% Ordering (11,404 calls)
% 0.70/0.91 ; 0.012 3% Sortal reasoning (11,862 calls)
% 0.70/0.91 ; 0.000 0% Purity testing (1 call)
% 0.70/0.91 ; 0.029 7% Other
% 0.70/0.91 ; 0.433 Total
% 0.70/0.91 ; 0.442 Real time
% 0.70/0.91 ;
% 0.70/0.91 ; Term-hash-array has 166 terms in all.
% 0.70/0.91 ; Feature-vector-row-index has 45 entries (197 at peak, 254 added, 209 deleted).
% 0.70/0.91 ; Feature-vector-row-index has 241 nodes (1,927 at peak, 2,475 added, 2,234 deleted).
% 0.70/0.91 ; Retrieved 890 possibly forward subsuming rows in 691 calls.
% 0.70/0.91 ; Retrieved 82 possibly backward subsumed rows in 254 calls.
% 0.70/0.91 ; Path-index has 109 entries (172 at peak, 193 added, 84 deleted).
% 0.70/0.91 ; Path-index has 51 nodes (51 at peak, 51 added, 0 deleted).
% 0.70/0.91 ; Trie-index has 109 entries (172 at peak, 193 added, 84 deleted).
% 0.70/0.91 ; Trie-index has 108 nodes (155 at peak, 168 added, 60 deleted).
% 0.70/0.91 ; Retrieved 1,556 generalization terms in 8,644 calls.
% 0.70/0.91 ; Retrieved 58 instance terms in 58 calls.
% 0.70/0.91 ; Retrieved 55,563 unifiable terms in 2,267 calls.
% 0.70/0.91 ;
% 0.70/0.91 ; The agenda of rows to process has 26 entries:
% 0.70/0.91 ; 1 with value 8 1 with value 22 7 with value 32
% 0.70/0.91 ; 8 with value 12 1 with value 24 1 with value 33
% 0.70/0.91 ; 1 with value 20 3 with value 26 2 with value 44
% 0.70/0.91 ; 1 with value 21
% 0.70/0.91 ; The agenda of rows to give has 31 entries:
% 0.70/0.91 ; 3 with value (4 8) 1 with value (4 25) 4 with value (4 38)
% 0.70/0.91 ; 3 with value (4 9) 2 with value (4 30) 1 with value (4 39)
% 0.70/0.91 ; 1 with value (4 13) 1 with value (4 31) 2 with value (4 40)
% 0.70/0.91 ; 1 with value (4 15) 3 with value (4 32) 1 with value (4 41)
% 0.70/0.91 ; 1 with value (4 16) 1 with value (4 33) 1 with value (4 42)
% 0.70/0.91 ; 1 with value (4 20) 2 with value (4 36) 2 with value (4 54)
% 0.70/0.91 Evaluation took:
% 0.70/0.91 0.442 seconds of real time
% 0.70/0.91 0.384027 seconds of user run time
% 0.70/0.91 0.058129 seconds of system run time
% 0.70/0.91 [Run times include 0.008 seconds GC run time.]
% 0.70/0.91 0 calls to %EVAL
% 0.70/0.91 0 page faults and
% 0.70/0.91 26,693,048 bytes consed.
% 0.70/0.91 :PROOF-FOUND
% 0.70/0.91 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-05-28T19:51:52
% 0.70/0.91 :PROOF-FOUND
% 0.70/0.91 *
%------------------------------------------------------------------------------