%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SET192-6 : TPTP v8.1.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n011.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 05:08:13 EDT 2022
% Result : Unsatisfiable 6.03s 6.25s
% Output : Refutation 6.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 8
% Syntax : Number of clauses : 14 ( 9 unt; 2 nHn; 11 RR)
% Number of literals : 21 ( 0 equ; 9 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 12 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(subclass_members,axiom,
( ~ subclass(X,Y)
| ~ member(Z,X)
| member(Z,Y) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X,Y),X)
| subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
cnf(not_subclass_members2,axiom,
( ~ member(not_subclass_element(X,Y),Y)
| subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members2) ).
cnf(class_elements_are_sets,axiom,
subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(complement1,axiom,
( ~ member(X,complement(Y))
| ~ member(X,Y) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(complement2,axiom,
( ~ member(X,universal_class)
| member(X,complement(Y))
| member(X,Y) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement2) ).
cnf(prove_subclass_property9_1,negated_conjecture,
subclass(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_subclass_property9_1) ).
cnf(prove_subclass_property9_2,negated_conjecture,
~ subclass(complement(y),complement(x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_subclass_property9_2) ).
cnf(144,plain,
member(not_subclass_element(complement(y),complement(x)),complement(y)),
inference('HYPERRESOLVE',[status(thm)],[prove_subclass_property9_2,not_subclass_members1]) ).
cnf(145,plain,
~ member(not_subclass_element(complement(y),complement(x)),complement(x)),
inference('UR-RESOLVE',[status(thm)],[not_subclass_members2,prove_subclass_property9_2]) ).
cnf(8853,plain,
member(not_subclass_element(complement(y),complement(x)),universal_class),
inference('HYPERRESOLVE',[status(thm)],[subclass_members,144,class_elements_are_sets]) ).
cnf(8854,plain,
~ member(not_subclass_element(complement(y),complement(x)),y),
inference('UR-RESOLVE',[status(thm)],[complement1,144]) ).
cnf(25768,plain,
member(not_subclass_element(complement(y),complement(x)),x),
inference('UR-RESOLVE',[status(thm)],[complement2,8853,145]) ).
cnf(26108,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[subclass_members,8854,prove_subclass_property9_1]),25768]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SET192-6 : TPTP v8.1.0. Bugfixed v2.1.0.
% 0.11/0.11 % Command : run-snark %s %d
% 0.12/0.30 % Computer : n011.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8042.1875MB
% 0.12/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 600
% 0.12/0.30 % DateTime : Sun Jul 10 04:47:56 EDT 2022
% 0.12/0.31 % CPUTime :
% 0.17/0.41 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 *
% 0.17/0.42 *
% 0.17/0.43 #<PACKAGE "SNARK-USER">
% 0.17/0.43 *
% 0.17/0.43 SNARK-TPTP-OPTIONS
% 0.17/0.43 *
% 0.17/0.43 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.17/0.43 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.17/0.43 (USE-FACTORING :POS)
% 0.17/0.43 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.17/0.43 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.17/0.43 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.17/0.43 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.17/0.43 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.17/0.43 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.17/0.43 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.17/0.43 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.17/0.43 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.17/0.43 (DECLARE-TPTP-SYMBOLS2))
% 0.17/0.43 *
% 0.17/0.43 "."
% 0.17/0.43 *
% 0.17/0.43 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-10T04:47:56
% 0.17/0.43 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n011.cluster.edu at 2022-07-10T04:47:56
% 6.03/6.25
% 6.03/6.25
% 6.03/6.25 #||
% 6.03/6.25 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.03/6.25 % SZS output start Refutation
% See solution above
% 6.03/6.25 ||#
% 6.03/6.25
% 6.03/6.25 ; Summary of computation:
% 6.03/6.25 ; 49828 formulas have been input or derived (from 551 formulas).
% 6.03/6.25 ; 26108 (52%) were retained. Of these,
% 6.03/6.25 ; 373 ( 1%) were simplified or subsumed later,
% 6.03/6.25 ; 25735 (99%) are still being kept.
% 6.03/6.25 ;
% 6.03/6.25 ; Run time in seconds excluding printing time:
% 6.03/6.25 ; 0.021 0% Read assertion file (1 call)
% 6.03/6.25 ; 0.003 0% Assert (114 calls)
% 6.03/6.25 ; 1.734 30% Process new row (48,671 calls)
% 6.03/6.25 ; 2.199 38% Resolution (1,100 calls)
% 6.03/6.25 ; 0.026 0% Paramodulation (550 calls)
% 6.03/6.25 ; 0.000 0% Factoring (11 calls)
% 6.03/6.25 ; 0.024 0% Condensing (3,211 calls)
% 6.03/6.25 ; 0.332 6% Forward subsumption (3,211 calls)
% 6.03/6.25 ; 0.151 3% Backward subsumption (3,159 calls)
% 6.03/6.25 ; 0.017 0% Clause clause subsumption (12,938 calls)
% 6.03/6.25 ; 0.776 13% Forward simplification (48,665 calls)
% 6.03/6.25 ; 0.344 6% Backward simplification (26,093 calls)
% 6.03/6.25 ; 0.012 0% Ordering (8,321 calls)
% 6.03/6.25 ; 0.000 0% Sortal reasoning (32 calls)
% 6.03/6.25 ; 0.001 0% Purity testing (1 call)
% 6.03/6.25 ; 0.175 3% Other
% 6.03/6.25 ; 5.815 Total
% 6.03/6.25 ; 5.824 Real time
% 6.03/6.25 ;
% 6.03/6.25 ; Term-hash-array has 36,248 terms in all.
% 6.03/6.25 ; Feature-vector-row-index has 3,129 entries (3,129 at peak, 3,159 added, 30 deleted).
% 6.03/6.25 ; Feature-vector-row-index has 13,280 nodes (13,280 at peak, 13,406 added, 126 deleted).
% 6.03/6.25 ; Retrieved 15,971 possibly forward subsuming rows in 3,211 calls.
% 6.03/6.25 ; Retrieved 4,231 possibly backward subsumed rows in 3,159 calls.
% 6.03/6.25 ; Path-index has 35,824 entries (35,824 at peak, 36,309 added, 485 deleted).
% 6.03/6.25 ; Path-index has 8,992 nodes (8,992 at peak, 9,117 added, 125 deleted).
% 6.03/6.25 ; Trie-index has 35,824 entries (35,824 at peak, 36,309 added, 485 deleted).
% 6.03/6.25 ; Trie-index has 100,023 nodes (100,023 at peak, 101,148 added, 1,125 deleted).
% 6.03/6.25 ; Retrieved 32,555 generalization terms in 131,665 calls.
% 6.03/6.25 ; Retrieved 23,085 instance terms in 22,933 calls.
% 6.03/6.25 ; Retrieved 4,943,697 unifiable terms in 30,958 calls.
% 6.03/6.25 ;
% 6.03/6.25 ; The agenda of rows to process has 7 entries:
% 6.03/6.25 ; 1 with value 13 2 with value 15 2 with value 18
% 6.03/6.25 ; 1 with value 14 1 with value 16
% 6.03/6.25 ; The agenda of rows to give has 25205 entries:
% 6.03/6.25 ; 1 with value (4 7) 4332 with value (4 22) 3 with value (4 34)
% 6.03/6.25 ; 1 with value (4 9) 1881 with value (4 23) 2 with value (4 37)
% 6.03/6.25 ; 47 with value (4 12) 410 with value (4 24) 1 with value (4 43)
% 6.03/6.25 ; 328 with value (4 13) 10 with value (4 25) 1 with value (4 44)
% 6.03/6.25 ; 492 with value (4 14) 13 with value (4 26) 1 with value (4 45)
% 6.03/6.25 ; 724 with value (4 15) 15 with value (4 27) 4 with value (4 46)
% 6.03/6.25 ; 934 with value (4 16) 11 with value (4 28) 2 with value (4 49)
% 6.03/6.25 ; 1243 with value (4 17) 22 with value (4 29) 1 with value (4 51)
% 6.03/6.25 ; 2191 with value (4 18) 17 with value (4 30) 1 with value (4 53)
% 6.03/6.25 ; 2957 with value (4 19) 3 with value (4 31) 1 with value (4 55)
% 6.03/6.25 ; 4636 with value (4 20) 8 with value (4 32) 1 with value (4 59)
% 6.03/6.25 ; 4908 with value (4 21) 2 with value (4 33) 1 with value (4 63)
% 6.03/6.25 Evaluation took:
% 6.03/6.25 5.827 seconds of real time
% 6.03/6.25 5.404199 seconds of user run time
% 6.03/6.25 0.413989 seconds of system run time
% 6.03/6.25 [Run times include 1.129 seconds GC run time.]
% 6.03/6.25 0 calls to %EVAL
% 6.03/6.25 0 page faults and
% 6.03/6.25 356,825,120 bytes consed.
% 6.03/6.25 :PROOF-FOUND
% 6.03/6.25 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-10T04:48:02
% 6.03/6.25 :PROOF-FOUND
% 6.03/6.25 *
%------------------------------------------------------------------------------