%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET094-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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 : 300s
% DateTime : Thu May 9 17:39:11 EDT 2024
% Result : Unsatisfiable 41.78s 42.00s
% Output : Refutation 41.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of clauses : 17 ( 11 unt; 1 nHn; 15 RR)
% Number of literals : 25 ( 10 equ; 8 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 14 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_property_of_singletons1_3,negated_conjecture,
member_of(x) != y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_property_of_singletons1_3) ).
cnf(symmetry,axiom,
( X37 != X36
| X36 = X37 ),
theory(equality) ).
cnf(unordered_pair_member,axiom,
( ~ member(X39,unordered_pair(X41,X40))
| X39 = X41
| X39 = X40 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair_member) ).
cnf(equal_implies_subclass2,axiom,
( X15 != X14
| subclass(X14,X15) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(singleton_set,axiom,
unordered_pair(X44,X44) = singleton(X44),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',singleton_set) ).
cnf(c57,plain,
subclass(singleton(X46),unordered_pair(X46,X46)),
inference(resolution,[status(thm)],[singleton_set,equal_implies_subclass2]) ).
cnf(subclass_members,axiom,
( ~ subclass(X6,X5)
| ~ member(X4,X6)
| member(X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(prove_property_of_singletons1_2,negated_conjecture,
member(y,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_property_of_singletons1_2) ).
cnf(c41,plain,
( ~ subclass(x,X93)
| member(y,X93) ),
inference(resolution,[status(thm)],[prove_property_of_singletons1_2,subclass_members]) ).
cnf(prove_property_of_singletons1_1,negated_conjecture,
singleton(member_of(x)) = x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_property_of_singletons1_1) ).
cnf(c84,plain,
subclass(x,singleton(member_of(x))),
inference(resolution,[status(thm)],[prove_property_of_singletons1_1,equal_implies_subclass2]) ).
cnf(c175,plain,
member(y,singleton(member_of(x))),
inference(resolution,[status(thm)],[c84,c41]) ).
cnf(c200,plain,
( ~ subclass(singleton(member_of(x)),X826)
| member(y,X826) ),
inference(resolution,[status(thm)],[c175,subclass_members]) ).
cnf(c7427,plain,
member(y,unordered_pair(member_of(x),member_of(x))),
inference(resolution,[status(thm)],[c200,c57]) ).
cnf(c65242,plain,
y = member_of(x),
inference(resolution,[status(thm)],[c7427,unordered_pair_member]) ).
cnf(c65307,plain,
member_of(x) = y,
inference(resolution,[status(thm)],[c65242,symmetry]) ).
cnf(c65414,plain,
$false,
inference(resolution,[status(thm)],[c65307,prove_property_of_singletons1_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET094-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n017.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 18:45:23 EDT 2024
% 0.15/0.35 % CPUTime :
% 41.78/42.00 % Version: 1.5
% 41.78/42.00 % SZS status Unsatisfiable
% 41.78/42.00 % SZS output start CNFRefutation
% See solution above
% 41.78/42.01
% 41.78/42.01 % Initial clauses : 137
% 41.78/42.01 % Processed clauses : 1812
% 41.78/42.01 % Factors computed : 33
% 41.78/42.01 % Resolvents computed: 65421
% 41.78/42.01 % Tautologies deleted: 10
% 41.78/42.01 % Forward subsumed : 1148
% 41.78/42.01 % Backward subsumed : 17
% 41.78/42.01 % -------- CPU Time ---------
% 41.78/42.01 % User time : 41.497 s
% 41.78/42.01 % System time : 0.146 s
% 41.78/42.01 % Total time : 41.643 s
%------------------------------------------------------------------------------