%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : PUZ135_1 : TPTP v8.1.0. Released v5.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 : Mon Jul 18 18:26:55 EDT 2022
% Result : Theorem 0.38s 0.56s
% Output : Refutation 0.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 19
% Syntax : Number of formulae : 49 ( 26 unt; 0 typ; 0 def)
% Number of atoms : 300 ( 83 equ)
% Maximal formula atoms : 4 ( 6 avg)
% Number of connectives : 82 ( 47 ~; 35 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 216 ( 216 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 : 9 ( 0 sgn 9 !; 0 ?; 9 :)
% 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(25,axiom,
entry_of(a) != holography,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_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(30,axiom,
! [X: knowheyan] :
( ( entry_of(X) != collage_painting )
| ( place_of(X) != first ) ),
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(34,axiom,
place_of(b) != 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(39,negated_conjecture,
( ( entry_of(a) != reconstituted_materials_sculpture )
| ( entry_of(b) != holography )
| ( entry_of(c) != laser_etching )
| ( entry_of(d) != collage_painting ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',entries) ).
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(58,plain,
( ( place_of(b) = first )
| ( place_of(b) = second ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[34,21]),32]) ).
tff(65,plain,
entry_of(a) = reconstituted_materials_sculpture,
inference('UR-RESOLVE',[status(thm)],[20,42,40,25]) ).
tff(66,plain,
( ( entry_of(b) != holography )
| ( entry_of(c) != laser_etching )
| ( entry_of(d) != collage_painting ) ),
inference('REWRITE',[status(thm)],[39,65,theory(equality)]) ).
tff(67,plain,
reconstituted_materials_sculpture != entry_of(d),
inference('REWRITE',[status(thm)],[43,65,theory(equality)]) ).
tff(68,plain,
reconstituted_materials_sculpture != entry_of(c),
inference('REWRITE',[status(thm)],[46,65,theory(equality)]) ).
tff(69,plain,
reconstituted_materials_sculpture != entry_of(b),
inference('REWRITE',[status(thm)],[48,65,theory(equality)]) ).
tff(71,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(d) = holography )
| ( entry_of(d) = laser_etching ) ),
inference('HYPERRESOLVE',[status(thm)],[67,20]) ).
tff(74,plain,
( ( entry_of(c) = holography )
| ( entry_of(c) = laser_etching ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[68,20]),41]) ).
tff(76,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(b) = holography ) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[69,20]),36]) ).
tff(83,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(87,plain,
( ( entry_of(c) = holography )
| ( entry_of(d) != laser_etching ) ),
inference('PARAMODULATE',[status(thm)],[45,74,theory(equality)]) ).
tff(91,plain,
( ( entry_of(c) = holography )
| ( entry_of(b) != holography )
| ( entry_of(d) != collage_painting ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66,74,theory(equality)]),theory(equality)]) ).
tff(92,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(c) != holography ) ),
inference('PARAMODULATE',[status(thm)],[47,76,theory(equality)]) ).
tff(93,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(d) != holography ) ),
inference('PARAMODULATE',[status(thm)],[44,76,theory(equality)]) ).
tff(104,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(d) = holography )
| ( entry_of(c) = holography ) ),
inference('HYPERRESOLVE',[status(thm)],[87,71]) ).
tff(108,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(c) = holography )
| ( entry_of(d) != collage_painting ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[91,76,theory(equality)]),theory(equality)]) ).
tff(121,plain,
( ( entry_of(d) = collage_painting )
| ( entry_of(c) = holography )
| ( entry_of(b) = collage_painting ) ),
inference('HYPERRESOLVE',[status(thm)],[93,104]) ).
tff(127,plain,
( ( entry_of(c) = holography )
| ( entry_of(b) = collage_painting ) ),
inference('HYPERRESOLVE',[status(thm)],[108,121]) ).
tff(128,plain,
entry_of(b) = collage_painting,
inference('HYPERRESOLVE',[status(thm)],[92,127]) ).
tff(138,plain,
place_of(b) = first,
inference('REWRITE',[status(thm)],[83,128,theory(equality)]) ).
cnf(153,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[30,138]),128,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : PUZ135_1 : TPTP v8.1.0. Released v5.1.0.
% 0.06/0.12 % Command : run-snark %s %d
% 0.14/0.33 % Computer : n029.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 600
% 0.14/0.33 % DateTime : Sun May 29 03:45:13 EDT 2022
% 0.14/0.33 % CPUTime :
% 0.20/0.44 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 *
% 0.20/0.45 *
% 0.20/0.46 #<PACKAGE "SNARK-USER">
% 0.20/0.46 *
% 0.20/0.46 SNARK-TPTP-OPTIONS
% 0.20/0.46 *
% 0.20/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.46 (USE-FACTORING :POS)
% 0.20/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.46 *
% 0.20/0.46 "."
% 0.20/0.46 *
% 0.20/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-05-29T03:45:13
% 0.20/0.46 ; 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-05-29T03:45:13
% 0.38/0.56
% 0.38/0.56
% 0.38/0.56 #||
% 0.38/0.56 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.56 % SZS output start Refutation
% See solution above
% 0.38/0.57 ||#
% 0.38/0.57
% 0.38/0.57 ; Summary of computation:
% 0.38/0.57 ; 545 formulas have been input or derived (from 106 formulas).
% 0.38/0.57 ; 153 (28%) were retained. Of these,
% 0.38/0.57 ; 90 (59%) were simplified or subsumed later,
% 0.38/0.57 ; 63 (41%) are still being kept.
% 0.38/0.57 ;
% 0.38/0.57 ; Run time in seconds excluding printing time:
% 0.38/0.57 ; 0.005 5% Read assertion file (1 call)
% 0.38/0.57 ; 0.002 2% Assert (30 calls)
% 0.38/0.57 ; 0.014 14% Process new row (511 calls)
% 0.38/0.57 ; 0.012 12% Resolution (210 calls)
% 0.38/0.57 ; 0.013 13% Paramodulation (105 calls)
% 0.38/0.57 ; 0.000 0% Factoring (14 calls)
% 0.38/0.57 ; 0.002 2% Condensing (156 calls)
% 0.38/0.57 ; 0.004 4% Forward subsumption (156 calls)
% 0.38/0.57 ; 0.002 2% Backward subsumption (98 calls)
% 0.38/0.57 ; 0.001 1% Clause clause subsumption (71 calls)
% 0.38/0.57 ; 0.016 16% Forward simplification (435 calls)
% 0.38/0.57 ; 0.004 4% Backward simplification (153 calls)
% 0.38/0.57 ; 0.003 3% Ordering (1,607 calls)
% 0.38/0.57 ; 0.001 1% Sortal reasoning (838 calls)
% 0.38/0.57 ; 0.000 0% Purity testing (1 call)
% 0.38/0.57 ; 0.024 23% Other
% 0.38/0.57 ; 0.103 Total
% 0.38/0.57 ; 0.106 Real time
% 0.38/0.57 ;
% 0.38/0.57 ; Term-hash-array has 113 terms in all.
% 0.38/0.57 ; Feature-vector-row-index has 29 entries (77 at peak, 98 added, 69 deleted).
% 0.38/0.57 ; Feature-vector-row-index has 151 nodes (604 at peak, 770 added, 619 deleted).
% 0.38/0.57 ; Retrieved 69 possibly forward subsuming rows in 156 calls.
% 0.38/0.57 ; Retrieved 5 possibly backward subsumed rows in 98 calls.
% 0.38/0.57 ; Path-index has 96 entries (118 at peak, 132 added, 36 deleted).
% 0.38/0.57 ; Path-index has 51 nodes (51 at peak, 51 added, 0 deleted).
% 0.38/0.57 ; Trie-index has 96 entries (118 at peak, 132 added, 36 deleted).
% 0.38/0.57 ; Trie-index has 114 nodes (142 at peak, 159 added, 45 deleted).
% 0.38/0.57 ; Retrieved 296 generalization terms in 1,525 calls.
% 0.38/0.57 ; Retrieved 54 instance terms in 54 calls.
% 0.38/0.57 ; Retrieved 9,188 unifiable terms in 890 calls.
% 0.38/0.57 ;
% 0.38/0.57 ; The agenda of rows to process has 8 entries:
% 0.38/0.57 ; 8 with value 13
% 0.38/0.57 ; The agenda of rows to give has 18 entries:
% 0.38/0.57 ; 1 with value (4 8) 1 with value (4 14) 2 with value (4 26)
% 0.38/0.57 ; 2 with value (4 9) 1 with value (4 18) 3 with value (4 29)
% 0.38/0.57 ; 1 with value (4 10) 1 with value (4 20) 2 with value (4 34)
% 0.38/0.57 ; 3 with value (4 13) 1 with value (4 25)
% 0.38/0.57 Evaluation took:
% 0.38/0.57 0.107 seconds of real time
% 0.38/0.57 0.093706 seconds of user run time
% 0.38/0.57 0.013124 seconds of system run time
% 0.38/0.57 0 calls to %EVAL
% 0.38/0.57 0 page faults and
% 0.38/0.57 7,235,328 bytes consed.
% 0.38/0.57 :PROOF-FOUND
% 0.38/0.57 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-05-29T03:45:13
% 0.38/0.57 :PROOF-FOUND
% 0.38/0.57 *
%------------------------------------------------------------------------------