%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET024-3 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 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 : 300s
% DateTime : Thu May 9 17:38:53 EDT 2024
% Result : Unsatisfiable 117.48s 117.71s
% Output : Refutation 117.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of clauses : 18 ( 9 unt; 1 nHn; 10 RR)
% Number of literals : 32 ( 8 equ; 14 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 28 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_membership_of_singleton_set,negated_conjecture,
~ member(a,singleton_set(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_membership_of_singleton_set) ).
cnf(singleton_set,axiom,
singleton_set(X45) = non_ordered_pair(X45,X45),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',singleton_set) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(subset2,axiom,
( subset(X230,X231)
| member(f17(X230,X231),X230) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset2) ).
cnf(subset3,axiom,
( subset(X240,X241)
| ~ member(f17(X240,X241),X241) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset3) ).
cnf(c948,plain,
subset(X242,X242),
inference(resolution,[status(thm)],[subset3,subset2]) ).
cnf(c56,axiom,
( X931 != X933
| X934 != X932
| ~ subset(X931,X934)
| subset(X933,X932) ),
theory(equality) ).
cnf(c6417,plain,
( X2571 != X2570
| X2571 != X2572
| subset(X2570,X2572) ),
inference(resolution,[status(thm)],[c56,c948]) ).
cnf(c69655,plain,
( X2576 != X2575
| subset(X2575,X2576) ),
inference(resolution,[status(thm)],[c6417,reflexivity]) ).
cnf(c69830,plain,
subset(non_ordered_pair(X2581,X2581),singleton_set(X2581)),
inference(resolution,[status(thm)],[c69655,singleton_set]) ).
cnf(a_little_set,plain,
little_set(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_little_set) ).
cnf(non_ordered_pair2,axiom,
( member(X32,non_ordered_pair(X31,X33))
| ~ little_set(X32)
| X32 != X31 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair2) ).
cnf(c102,plain,
( member(X131,non_ordered_pair(X131,X130))
| ~ little_set(X131) ),
inference(resolution,[status(thm)],[non_ordered_pair2,reflexivity]) ).
cnf(c324,plain,
member(a,non_ordered_pair(a,X132)),
inference(resolution,[status(thm)],[c102,a_little_set]) ).
cnf(subset1,axiom,
( ~ subset(X304,X306)
| ~ member(X305,X304)
| member(X305,X306) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset1) ).
cnf(c1342,plain,
( ~ subset(non_ordered_pair(a,X3849),X3850)
| member(a,X3850) ),
inference(resolution,[status(thm)],[subset1,c324]) ).
cnf(c116471,plain,
member(a,singleton_set(a)),
inference(resolution,[status(thm)],[c1342,c69830]) ).
cnf(c116540,plain,
$false,
inference(resolution,[status(thm)],[c116471,prove_membership_of_singleton_set]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET024-3 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:12:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 117.48/117.71 % Version: 1.5
% 117.48/117.71 % SZS status Unsatisfiable
% 117.48/117.71 % SZS output start CNFRefutation
% See solution above
% 117.48/117.72
% 117.48/117.72 % Initial clauses : 220
% 117.48/117.72 % Processed clauses : 2755
% 117.48/117.72 % Factors computed : 75
% 117.48/117.72 % Resolvents computed: 116436
% 117.48/117.72 % Tautologies deleted: 18
% 117.48/117.72 % Forward subsumed : 2715
% 117.48/117.72 % Backward subsumed : 41
% 117.48/117.72 % -------- CPU Time ---------
% 117.48/117.72 % User time : 117.058 s
% 117.48/117.72 % System time : 0.226 s
% 117.48/117.72 % Total time : 117.284 s
%------------------------------------------------------------------------------