%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SEU339+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n003.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:25 EDT 2022
% Result : Theorem 33.44s 33.62s
% Output : Refutation 33.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 20
% Syntax : Number of clauses : 38 ( 24 unt; 3 nHn; 38 RR)
% Number of literals : 65 ( 4 equ; 32 neg)
% Maximal clause size : 7 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 37 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
( ~ element(X,powerset(cartesian_product2(Y,Z)))
| relation(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
cnf(3,axiom,
( ~ relation(X)
| ~ is_antisymmetric_in(X,Y)
| ~ in(Z,Y)
| ~ in(U,Y)
| ~ in(ordered_pair(Z,U),X)
| ~ in(ordered_pair(U,Z),X)
| Z = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_2) ).
cnf(10,axiom,
( ~ rel_str(X)
| ~ antisymmetric_relstr(X)
| is_antisymmetric_in(the_InternalRel(X),the_carrier(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_orders_2) ).
cnf(12,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/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
cnf(14,axiom,
( ~ relation_of2_as_subset(X,Y,Z)
| element(X,powerset(cartesian_product2(Y,Z))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
cnf(15,axiom,
( ~ rel_str(X)
| relation_of2_as_subset(the_InternalRel(X),the_carrier(X),the_carrier(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
cnf(21,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
cnf(34,axiom,
( ~ in(ordered_pair(X,Y),cartesian_product2(Z,U))
| in(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
cnf(38,negated_conjecture,
antisymmetric_relstr('SKOLEMAAAU12'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(39,negated_conjecture,
rel_str('SKOLEMAAAU12'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(40,negated_conjecture,
element('SKOLEMAAAU13',the_carrier('SKOLEMAAAU12')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(41,negated_conjecture,
element('SKOLEMAAAU14',the_carrier('SKOLEMAAAU12')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(42,negated_conjecture,
related('SKOLEMAAAU12','SKOLEMAAAU13','SKOLEMAAAU14'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(43,negated_conjecture,
related('SKOLEMAAAU12','SKOLEMAAAU14','SKOLEMAAAU13'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(44,negated_conjecture,
'SKOLEMAAAU13' != 'SKOLEMAAAU14',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
cnf(45,axiom,
( ~ element(X,Y)
| empty(Y)
| in(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
cnf(48,axiom,
( ~ in(X,Y)
| ~ element(Y,powerset(Z))
| element(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
cnf(49,axiom,
( ~ in(X,Y)
| ~ element(Y,powerset(Z))
| ~ empty(Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
cnf(51,axiom,
( ~ in(X,Y)
| ~ empty(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
cnf(52,axiom,
( ~ empty(X)
| X = Y
| ~ empty(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
cnf(56,plain,
~ in(X,empty_set),
inference('UR-RESOLVE',[status(thm)],[51,21]) ).
cnf(76,plain,
( empty(the_carrier('SKOLEMAAAU12'))
| in('SKOLEMAAAU13',the_carrier('SKOLEMAAAU12')) ),
inference('HYPERRESOLVE',[status(thm)],[45,40]) ).
cnf(77,plain,
( empty(the_carrier('SKOLEMAAAU12'))
| in('SKOLEMAAAU14',the_carrier('SKOLEMAAAU12')) ),
inference('HYPERRESOLVE',[status(thm)],[45,41]) ).
cnf(83,plain,
relation_of2_as_subset(the_InternalRel('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12')),
inference('HYPERRESOLVE',[status(thm)],[15,39]) ).
cnf(104,plain,
is_antisymmetric_in(the_InternalRel('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12')),
inference('HYPERRESOLVE',[status(thm)],[10,39,38]) ).
cnf(107,plain,
in(ordered_pair('SKOLEMAAAU13','SKOLEMAAAU14'),the_InternalRel('SKOLEMAAAU12')),
inference('HYPERRESOLVE',[status(thm)],[12,39,40,41,42]) ).
cnf(108,plain,
in(ordered_pair('SKOLEMAAAU14','SKOLEMAAAU13'),the_InternalRel('SKOLEMAAAU12')),
inference('HYPERRESOLVE',[status(thm)],[12,39,41,40,43]) ).
cnf(112,plain,
~ in(ordered_pair(X,Y),cartesian_product2(empty_set,Z)),
inference('UR-RESOLVE',[status(thm)],[34,56]) ).
cnf(557,plain,
element(the_InternalRel('SKOLEMAAAU12'),powerset(cartesian_product2(the_carrier('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12')))),
inference('HYPERRESOLVE',[status(thm)],[14,83]) ).
cnf(90821,plain,
relation(the_InternalRel('SKOLEMAAAU12')),
inference('HYPERRESOLVE',[status(thm)],[2,557]) ).
cnf(90822,plain,
~ empty(cartesian_product2(the_carrier('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12'))),
inference('UR-RESOLVE',[status(thm)],[49,557,107]) ).
cnf(90824,plain,
element(ordered_pair('SKOLEMAAAU13','SKOLEMAAAU14'),cartesian_product2(the_carrier('SKOLEMAAAU12'),the_carrier('SKOLEMAAAU12'))),
inference('HYPERRESOLVE',[status(thm)],[48,557,107]) ).
cnf(90829,plain,
empty(the_carrier('SKOLEMAAAU12')),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[3,90821,104,76,77,107,108]),44]) ).
cnf(90834,plain,
the_carrier('SKOLEMAAAU12') = empty_set,
inference('HYPERRESOLVE',[status(thm)],[52,90829,21]) ).
cnf(90840,plain,
~ empty(cartesian_product2(empty_set,empty_set)),
inference('REWRITE',[status(thm)],[90822,90834,theory(equality)]) ).
cnf(90842,plain,
element(ordered_pair('SKOLEMAAAU13','SKOLEMAAAU14'),cartesian_product2(empty_set,empty_set)),
inference('REWRITE',[status(thm)],[90824,90834,theory(equality)]) ).
cnf(90849,plain,
~ element(ordered_pair(X,Y),cartesian_product2(empty_set,empty_set)),
inference('UR-RESOLVE',[status(thm)],[45,90840,112]) ).
cnf(90850,plain,
$false,
inference('REWRITE',[status(thm)],[90842,90849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SEU339+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n003.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 03:26:29 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 *
% 0.19/0.45 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-20T03:26:29
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n003.cluster.edu at 2022-06-20T03:26:29
% 0.19/0.48
% 0.19/0.48 ; Recognized commutativity assertion (= (|unordered_pair| ?X ?Y) (|unordered_pair| ?Y ?X)).
% 0.19/0.48 WARNING:
% 0.19/0.48 |one_sorted_str| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 33.44/33.62 ; Declaring unordered_pair to be commutative.
% 33.44/33.62
% 33.44/33.62 #||
% 33.44/33.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.44/33.62 % SZS output start Refutation
% See solution above
% 33.44/33.62 ||#
% 33.44/33.62
% 33.44/33.62 ; Summary of computation:
% 33.44/33.62 ; 94915 formulas have been input or derived (from 616 formulas).
% 33.44/33.62 ; 90850 (96%) were retained. Of these,
% 33.44/33.62 ; 198 ( 0%) were simplified or subsumed later,
% 33.44/33.62 ; 90652 (100%) are still being kept.
% 33.44/33.62 ;
% 33.44/33.62 ; Run time in seconds excluding printing time:
% 33.44/33.62 ; 0.008 0% Read assertion file (1 call)
% 33.44/33.62 ; 0.001 0% Assert (46 calls)
% 33.44/33.62 ; 10.677 32% Process new row (93,605 calls)
% 33.44/33.62 ; 11.101 33% Resolution (1,230 calls)
% 33.44/33.62 ; 0.096 0% Paramodulation (615 calls)
% 33.44/33.62 ; 0.000 0% Factoring (7 calls)
% 33.44/33.62 ; 0.005 0% Condensing (506 calls)
% 33.44/33.62 ; 0.024 0% Forward subsumption (506 calls)
% 33.44/33.62 ; 0.012 0% Backward subsumption (500 calls)
% 33.44/33.62 ; 0.002 0% Clause clause subsumption (1,499 calls)
% 33.44/33.62 ; 1.315 4% Forward simplification (93,543 calls)
% 33.44/33.62 ; 9.533 29% Backward simplification (90,850 calls)
% 33.44/33.62 ; 0.003 0% Ordering (970 calls)
% 33.44/33.62 ; 0.000 0% Sortal reasoning (32 calls)
% 33.44/33.62 ; 0.000 0% Purity testing (1 call)
% 33.44/33.62 ; 0.378 1% Other
% 33.44/33.62 ; 33.155 Total
% 33.44/33.62 ; 33.159 Real time
% 33.45/33.63 ;
% 33.45/33.63 ; Term-hash-array has 181,389 terms in all.
% 33.45/33.63 ; Feature-vector-row-index has 332 entries (494 at peak, 500 added, 168 deleted).
% 33.45/33.63 ; Feature-vector-row-index has 1,173 nodes (2,011 at peak, 2,037 added, 864 deleted).
% 33.45/33.63 ; Retrieved 1,670 possibly forward subsuming rows in 506 calls.
% 33.45/33.63 ; Retrieved 818 possibly backward subsumed rows in 500 calls.
% 33.45/33.63 ; Path-index has 180,986 entries (181,338 at peak, 181,396 added, 410 deleted).
% 33.45/33.63 ; Path-index has 6,848 nodes (6,848 at peak, 6,907 added, 59 deleted).
% 33.45/33.63 ; Trie-index has 180,986 entries (181,338 at peak, 181,396 added, 410 deleted).
% 33.45/33.63 ; Trie-index has 470,550 nodes (472,029 at peak, 472,178 added, 1,628 deleted).
% 33.45/33.63 ; Retrieved 5,191 generalization terms in 135,380 calls.
% 33.45/33.63 ; Retrieved 91,124 instance terms in 90,349 calls.
% 33.45/33.63 ; Retrieved 18,008,398 unifiable terms in 111,866 calls.
% 33.45/33.63 ;
% 33.45/33.63 ; The agenda of rows to process has 595 entries:
% 33.45/33.63 ; 1 with value 13 22 with value 17 144 with value 20
% 33.45/33.63 ; 8 with value 14 50 with value 18 166 with value 21
% 33.45/33.63 ; 12 with value 15 80 with value 19 100 with value 22
% 33.45/33.63 ; 12 with value 16
% 33.45/33.63 ; The agenda of rows to give has 90051 entries:
% 33.45/33.63 ; 1 with value (4 10) 7383 with value (4 21) 18 with value (4 31)
% 33.45/33.63 ; 2 with value (4 11) 12087 with value (4 22) 8 with value (4 32)
% 33.45/33.63 ; 3 with value (4 12) 18244 with value (4 23) 2 with value (4 36)
% 33.45/33.63 ; 3 with value (4 13) 20863 with value (4 24) 4 with value (4 40)
% 33.45/33.63 ; 1 with value (4 14) 15183 with value (4 25) 8 with value (4 41)
% 33.45/33.63 ; 227 with value (4 15) 5026 with value (4 26) 4 with value (4 42)
% 33.45/33.63 ; 546 with value (4 16) 291 with value (4 27) 4 with value (4 43)
% 33.45/33.63 ; 977 with value (4 17) 8 with value (4 28) 12 with value (4 45)
% 33.45/33.63 ; 1656 with value (4 18) 10 with value (4 29) 18 with value (4 46)
% 33.45/33.63 ; 2788 with value (4 19) 18 with value (4 30) 8 with value (4 49)
% 33.45/33.63 ; 4648 with value (4 20)
% 33.45/33.63 Evaluation took:
% 33.45/33.63 33.166 seconds of real time
% 33.45/33.63 31.872496 seconds of user run time
% 33.45/33.63 1.291961 seconds of system run time
% 33.45/33.63 [Run times include 5.949 seconds GC run time.]
% 33.45/33.63 0 calls to %EVAL
% 33.45/33.63 0 page faults and
% 33.45/33.63 1,172,975,312 bytes consed.
% 33.45/33.63 :PROOF-FOUND
% 33.45/33.63 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-20T03:27:02
% 33.45/33.63 :PROOF-FOUND
% 33.45/33.63 *
%------------------------------------------------------------------------------