%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SEU340+1 : TPTP v8.1.0. Released v3.3.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 : Tue Jul 19 14:21:26 EDT 2022
% Result : Theorem 36.43s 36.66s
% Output : Refutation 36.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 22
% Syntax : Number of clauses : 42 ( 26 unt; 4 nHn; 42 RR)
% Number of literals : 75 ( 2 equ; 38 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 41 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
( ~ element(X,powerset(cartesian_product2(Y,Z)))
| relation(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
cnf(3,axiom,
( ~ rel_str(X)
| ~ transitive_relstr(X)
| is_transitive_in(the_InternalRel(X),the_carrier(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_orders_2) ).
cnf(6,axiom,
( ~ relation(X)
| ~ is_transitive_in(X,Y)
| ~ in(Z,Y)
| ~ in(U,Y)
| ~ in(V,Y)
| ~ in(ordered_pair(Z,U),X)
| ~ in(ordered_pair(U,V),X)
| in(ordered_pair(Z,V),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_relat_2) ).
cnf(13,axiom,
( ~ rel_str(X)
| ~ element(Y,the_carrier(X))
| ~ element(Z,the_carrier(X))
| ~ related(X,Y,Z)
| in(ordered_pair(Y,Z),the_InternalRel(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_orders_2) ).
cnf(14,axiom,
( ~ rel_str(X)
| ~ element(Y,the_carrier(X))
| ~ element(Z,the_carrier(X))
| related(X,Y,Z)
| ~ in(ordered_pair(Y,Z),the_InternalRel(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_orders_2) ).
cnf(15,axiom,
( ~ relation_of2_as_subset(X,Y,Z)
| element(X,powerset(cartesian_product2(Y,Z))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
cnf(16,axiom,
( ~ rel_str(X)
| relation_of2_as_subset(the_InternalRel(X),the_carrier(X),the_carrier(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_orders_2) ).
cnf(22,axiom,
empty(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
cnf(35,axiom,
( ~ in(ordered_pair(X,Y),cartesian_product2(Z,U))
| in(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t106_zfmisc_1) ).
cnf(39,negated_conjecture,
transitive_relstr('SKOLEMAAAV13'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(40,negated_conjecture,
rel_str('SKOLEMAAAV13'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(41,negated_conjecture,
element('SKOLEMAAAV14',the_carrier('SKOLEMAAAV13')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(42,negated_conjecture,
element('SKOLEMAAAV15',the_carrier('SKOLEMAAAV13')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(43,negated_conjecture,
element('SKOLEMAAAV16',the_carrier('SKOLEMAAAV13')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(44,negated_conjecture,
related('SKOLEMAAAV13','SKOLEMAAAV14','SKOLEMAAAV15'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(45,negated_conjecture,
related('SKOLEMAAAV13','SKOLEMAAAV15','SKOLEMAAAV16'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(46,negated_conjecture,
~ related('SKOLEMAAAV13','SKOLEMAAAV14','SKOLEMAAAV16'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_orders_2) ).
cnf(47,axiom,
( ~ element(X,Y)
| empty(Y)
| in(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
cnf(50,axiom,
( ~ in(X,Y)
| ~ element(Y,powerset(Z))
| element(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
cnf(51,axiom,
( ~ in(X,Y)
| ~ element(Y,powerset(Z))
| ~ empty(Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
cnf(53,axiom,
( ~ in(X,Y)
| ~ empty(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
cnf(54,axiom,
( ~ empty(X)
| X = Y
| ~ empty(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
cnf(58,plain,
~ in(X,empty_set),
inference('UR-RESOLVE',[status(thm)],[53,22]) ).
cnf(78,plain,
( empty(the_carrier('SKOLEMAAAV13'))
| in('SKOLEMAAAV14',the_carrier('SKOLEMAAAV13')) ),
inference('HYPERRESOLVE',[status(thm)],[47,41]) ).
cnf(79,plain,
( empty(the_carrier('SKOLEMAAAV13'))
| in('SKOLEMAAAV15',the_carrier('SKOLEMAAAV13')) ),
inference('HYPERRESOLVE',[status(thm)],[47,42]) ).
cnf(80,plain,
( empty(the_carrier('SKOLEMAAAV13'))
| in('SKOLEMAAAV16',the_carrier('SKOLEMAAAV13')) ),
inference('HYPERRESOLVE',[status(thm)],[47,43]) ).
cnf(86,plain,
relation_of2_as_subset(the_InternalRel('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13')),
inference('HYPERRESOLVE',[status(thm)],[16,40]) ).
cnf(104,plain,
is_transitive_in(the_InternalRel('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13')),
inference('HYPERRESOLVE',[status(thm)],[3,40,39]) ).
cnf(110,plain,
in(ordered_pair('SKOLEMAAAV14','SKOLEMAAAV15'),the_InternalRel('SKOLEMAAAV13')),
inference('HYPERRESOLVE',[status(thm)],[13,40,41,42,44]) ).
cnf(111,plain,
in(ordered_pair('SKOLEMAAAV15','SKOLEMAAAV16'),the_InternalRel('SKOLEMAAAV13')),
inference('HYPERRESOLVE',[status(thm)],[13,40,42,43,45]) ).
cnf(112,plain,
~ in(ordered_pair('SKOLEMAAAV14','SKOLEMAAAV16'),the_InternalRel('SKOLEMAAAV13')),
inference('UR-RESOLVE',[status(thm)],[14,40,41,43,46]) ).
cnf(117,plain,
~ in(ordered_pair(X,Y),cartesian_product2(empty_set,Z)),
inference('UR-RESOLVE',[status(thm)],[35,58]) ).
cnf(566,plain,
element(the_InternalRel('SKOLEMAAAV13'),powerset(cartesian_product2(the_carrier('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13')))),
inference('HYPERRESOLVE',[status(thm)],[15,86]) ).
cnf(90991,plain,
relation(the_InternalRel('SKOLEMAAAV13')),
inference('HYPERRESOLVE',[status(thm)],[2,566]) ).
cnf(90992,plain,
~ empty(cartesian_product2(the_carrier('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13'))),
inference('UR-RESOLVE',[status(thm)],[51,566,110]) ).
cnf(90994,plain,
element(ordered_pair('SKOLEMAAAV14','SKOLEMAAAV15'),cartesian_product2(the_carrier('SKOLEMAAAV13'),the_carrier('SKOLEMAAAV13'))),
inference('HYPERRESOLVE',[status(thm)],[50,566,110]) ).
cnf(90999,plain,
empty(the_carrier('SKOLEMAAAV13')),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[6,90991,104,78,79,80,110,111]),112]) ).
cnf(91005,plain,
the_carrier('SKOLEMAAAV13') = empty_set,
inference('HYPERRESOLVE',[status(thm)],[54,90999,22]) ).
cnf(91012,plain,
~ empty(cartesian_product2(empty_set,empty_set)),
inference('REWRITE',[status(thm)],[90992,91005,theory(equality)]) ).
cnf(91014,plain,
element(ordered_pair('SKOLEMAAAV14','SKOLEMAAAV15'),cartesian_product2(empty_set,empty_set)),
inference('REWRITE',[status(thm)],[90994,91005,theory(equality)]) ).
cnf(91021,plain,
~ element(ordered_pair(X,Y),cartesian_product2(empty_set,empty_set)),
inference('UR-RESOLVE',[status(thm)],[47,91012,117]) ).
cnf(91022,plain,
$false,
inference('REWRITE',[status(thm)],[91014,91021]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU340+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jun 20 01:02:48 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.44 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 *
% 0.18/0.45 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-20T01:02:48
% 0.18/0.46 ; 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-20T01:02:48
% 0.18/0.48
% 0.18/0.48 ; Recognized commutativity assertion (= (|unordered_pair| ?X ?Y) (|unordered_pair| ?Y ?X)).
% 0.18/0.48 WARNING:
% 0.18/0.48 |one_sorted_str| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 36.43/36.66 ; Declaring unordered_pair to be commutative.
% 36.43/36.66
% 36.43/36.66 #||
% 36.43/36.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.43/36.66 % SZS output start Refutation
% See solution above
% 36.48/36.66 ||#
% 36.48/36.66
% 36.48/36.66 ; Summary of computation:
% 36.48/36.66 ; 96330 formulas have been input or derived (from 625 formulas).
% 36.48/36.66 ; 91022 (94%) were retained. Of these,
% 36.48/36.66 ; 286 ( 0%) were simplified or subsumed later,
% 36.48/36.66 ; 90736 (100%) are still being kept.
% 36.48/36.66 ;
% 36.48/36.66 ; Run time in seconds excluding printing time:
% 36.48/36.67 ; 0.007 0% Read assertion file (1 call)
% 36.48/36.67 ; 0.003 0% Assert (46 calls)
% 36.48/36.67 ; 9.414 26% Process new row (94,736 calls)
% 36.48/36.67 ; 14.184 39% Resolution (1,248 calls)
% 36.48/36.67 ; 0.174 0% Paramodulation (624 calls)
% 36.48/36.67 ; 0.000 0% Factoring (8 calls)
% 36.48/36.67 ; 0.007 0% Condensing (629 calls)
% 36.48/36.67 ; 0.033 0% Forward subsumption (629 calls)
% 36.48/36.67 ; 0.014 0% Backward subsumption (622 calls)
% 36.48/36.67 ; 0.000 0% Clause clause subsumption (1,462 calls)
% 36.48/36.67 ; 1.410 4% Forward simplification (94,674 calls)
% 36.48/36.67 ; 10.528 29% Backward simplification (91,022 calls)
% 36.48/36.67 ; 0.001 0% Ordering (1,189 calls)
% 36.48/36.67 ; 0.000 0% Sortal reasoning (32 calls)
% 36.48/36.67 ; 0.000 0% Purity testing (1 call)
% 36.48/36.67 ; 0.419 1% Other
% 36.48/36.67 ; 36.194 Total
% 36.48/36.67 ; 36.203 Real time
% 36.48/36.67 ;
% 36.48/36.67 ; Term-hash-array has 181,701 terms in all.
% 36.48/36.67 ; Feature-vector-row-index has 367 entries (614 at peak, 622 added, 255 deleted).
% 36.48/36.67 ; Feature-vector-row-index has 1,275 nodes (2,482 at peak, 2,515 added, 1,240 deleted).
% 36.48/36.67 ; Retrieved 1,265 possibly forward subsuming rows in 629 calls.
% 36.48/36.67 ; Retrieved 720 possibly backward subsumed rows in 622 calls.
% 36.48/36.67 ; Path-index has 181,136 entries (181,648 at peak, 181,709 added, 573 deleted).
% 36.48/36.67 ; Path-index has 7,065 nodes (7,065 at peak, 7,129 added, 64 deleted).
% 36.48/36.67 ; Trie-index has 181,136 entries (181,648 at peak, 181,709 added, 573 deleted).
% 36.48/36.67 ; Trie-index has 471,027 nodes (473,224 at peak, 473,379 added, 2,352 deleted).
% 36.48/36.67 ; Retrieved 6,155 generalization terms in 137,126 calls.
% 36.48/36.67 ; Retrieved 91,174 instance terms in 90,399 calls.
% 36.48/36.67 ; Retrieved 20,086,112 unifiable terms in 180,838 calls.
% 36.48/36.67 ;
% 36.48/36.67 ; The agenda of rows to process has 595 entries:
% 36.48/36.67 ; 1 with value 13 22 with value 17 144 with value 20
% 36.48/36.67 ; 8 with value 14 50 with value 18 166 with value 21
% 36.48/36.67 ; 12 with value 15 80 with value 19 100 with value 22
% 36.48/36.67 ; 12 with value 16
% 36.48/36.67 ; The agenda of rows to give has 90128 entries:
% 36.48/36.67 ; 1 with value (4 10) 7398 with value (4 21) 27 with value (4 31)
% 36.48/36.67 ; 2 with value (4 11) 12087 with value (4 22) 12 with value (4 32)
% 36.48/36.67 ; 3 with value (4 12) 18244 with value (4 23) 2 with value (4 36)
% 36.48/36.67 ; 3 with value (4 13) 20863 with value (4 24) 4 with value (4 40)
% 36.48/36.67 ; 1 with value (4 14) 15184 with value (4 25) 8 with value (4 41)
% 36.48/36.67 ; 229 with value (4 15) 5026 with value (4 26) 4 with value (4 42)
% 36.48/36.67 ; 548 with value (4 16) 292 with value (4 27) 4 with value (4 43)
% 36.48/36.67 ; 979 with value (4 17) 12 with value (4 28) 12 with value (4 45)
% 36.48/36.67 ; 1665 with value (4 18) 13 with value (4 29) 18 with value (4 46)
% 36.48/36.67 ; 2795 with value (4 19) 26 with value (4 30) 8 with value (4 49)
% 36.48/36.67 ; 4658 with value (4 20)
% 36.48/36.67 Evaluation took:
% 36.48/36.67 36.209 seconds of real time
% 36.48/36.67 34.927097 seconds of user run time
% 36.48/36.67 1.275611 seconds of system run time
% 36.48/36.67 [Run times include 6.373 seconds GC run time.]
% 36.48/36.67 0 calls to %EVAL
% 36.48/36.67 0 page faults and
% 36.48/36.67 1,255,352,736 bytes consed.
% 36.48/36.67 :PROOF-FOUND
% 36.48/36.67 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-20T01:03:24
% 36.48/36.67 :PROOF-FOUND
% 36.48/36.67 *
%------------------------------------------------------------------------------