%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM011-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:16:01 AM UTC 2026
% Result : Unsatisfiable 232.86s 46.35s
% Output : CNFRefutation 232.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 34 ( 22 unt; 0 def)
% Number of atoms : 50 ( 11 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 38 ( 22 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 42 ( 10 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_zero_is_first,axiom,
empty_set = successor(f75),
file('theBenchmark.p',prove_zero_is_first) ).
cnf(c_132,plain,
empty_set = successor(f75),
inference(clausify,[status(thm)],[prove_zero_is_first]) ).
fof(a_natural_number,axiom,
member(f75,natural_numbers),
file('theBenchmark.p',a_natural_number) ).
cnf(c_133,plain,
member(f75,natural_numbers),
inference(clausify,[status(thm)],[a_natural_number]) ).
fof(empty_set,axiom,
! [VAR_0] : ~ member(VAR_0,empty_set),
file('theBenchmark.p',empty_set) ).
cnf(c_271,plain,
~ member(A,empty_set),
inference(clausify,[status(thm)],[empty_set]) ).
cnf(c_272,plain,
~ member(A,successor(f75)),
inference(paramod,[status(thm)],[c_132,c_271]) ).
fof(successor,axiom,
! [VAR_0] : successor(VAR_0) = union(VAR_0,singleton_set(VAR_0)),
file('theBenchmark.p',successor) ).
cnf(c_273,plain,
successor(A) = union(A,singleton_set(A)),
inference(clausify,[status(thm)],[successor]) ).
fof(union,axiom,
! [VAR_0,VAR_1] : union(VAR_0,VAR_1) = complement(intersection(complement(VAR_0),complement(VAR_1))),
file('theBenchmark.p',union) ).
cnf(c_303,plain,
union(A,B) = complement(intersection(complement(A),complement(B))),
inference(clausify,[status(thm)],[union]) ).
fof(complement2,axiom,
! [VAR_0,VAR_1] :
( member(VAR_0,VAR_1)
| ~ little_set(VAR_0)
| member(VAR_0,complement(VAR_1)) ),
file('theBenchmark.p',complement2) ).
cnf(c_304,plain,
( member(A,B)
| ~ little_set(A)
| member(A,complement(B)) ),
inference(clausify,[status(thm)],[complement2]) ).
fof(complement1,axiom,
! [VAR_0,VAR_1] :
( ~ member(VAR_0,VAR_1)
| ~ member(VAR_0,complement(VAR_1)) ),
file('theBenchmark.p',complement1) ).
cnf(c_305,plain,
( ~ member(A,B)
| ~ member(A,complement(B)) ),
inference(clausify,[status(thm)],[complement1]) ).
fof(intersection2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(VAR_0,VAR_2)
| ~ member(VAR_0,intersection(VAR_1,VAR_2)) ),
file('theBenchmark.p',intersection2) ).
cnf(c_307,plain,
( member(A,C)
| ~ member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection2]) ).
fof(singleton_set,axiom,
! [VAR_0] : singleton_set(VAR_0) = non_ordered_pair(VAR_0,VAR_0),
file('theBenchmark.p',singleton_set) ).
cnf(c_333,plain,
singleton_set(A) = non_ordered_pair(A,A),
inference(clausify,[status(thm)],[singleton_set]) ).
fof(non_ordered_pair3,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 != VAR_2
| ~ little_set(VAR_0)
| member(VAR_0,non_ordered_pair(VAR_1,VAR_2)) ),
file('theBenchmark.p',non_ordered_pair3) ).
cnf(c_335,plain,
( A != C
| ~ little_set(A)
| member(A,non_ordered_pair(B,C)) ),
inference(clausify,[status(thm)],[non_ordered_pair3]) ).
fof(a2,axiom,
! [VAR_0,VAR_1] :
( little_set(VAR_0)
| ~ member(VAR_0,VAR_1) ),
file('theBenchmark.p',a2) ).
cnf(c_341,plain,
( little_set(A)
| ~ member(A,B) ),
inference(clausify,[status(thm)],[a2]) ).
cnf(c_56155,plain,
~ member(A,union(f75,singleton_set(f75))),
inference(paramod,[status(thm)],[c_273,c_272]) ).
cnf(c_56156,plain,
~ member(A,union(f75,non_ordered_pair(f75,f75))),
inference(paramod,[status(thm)],[c_333,c_56155]) ).
cnf(c_611,plain,
~ member(A,complement(intersection(complement(f75),complement(non_ordered_pair(f75,f75))))),
inference(paramod,[status(thm)],[c_303,c_56156]) ).
cnf(c_1187,plain,
little_set(f75),
inference(resolve,[status(thm)],[c_341,c_133]) ).
cnf(c_2233,plain,
( f75 != B
| member(f75,non_ordered_pair(A,B)) ),
inference(resolve,[status(thm)],[c_1187,c_335]) ).
cnf(c_2234,plain,
( member(f75,A)
| member(f75,complement(A)) ),
inference(resolve,[status(thm)],[c_1187,c_304]) ).
cnf(c_12547,plain,
member(f75,intersection(complement(f75),complement(non_ordered_pair(f75,f75)))),
inference(resolve,[status(thm)],[c_2234,c_611]) ).
cnf(c_26034,plain,
member(f75,non_ordered_pair(A,f75)),
inference(xxres,[status(thm)],[c_2233]) ).
cnf(c_56032,plain,
member(f75,complement(non_ordered_pair(f75,f75))),
inference(resolve,[status(thm)],[c_12547,c_307]) ).
cnf(c_56157,plain,
~ member(f75,non_ordered_pair(f75,f75)),
inference(resolve,[status(thm)],[c_56032,c_305]) ).
cnf(c_56154,plain,
$false,
inference(resolve,[status(thm)],[c_26034,c_56157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM011-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n014.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 01:52:32 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 1848814 was started by sandbox on n014,
% 0.10/0.38 % Sat Sep 26 01:52:32 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 232.86/46.35
% 232.86/46.35 % given #500 (T,wt=4): 2479 little_set(powerset(sigma(f75))). [resolve(2236,a,256,a)].
% 232.86/46.35
% 232.86/46.35 % given #1000 (T,wt=7): 8731 member(sigma(sigma(powerset(sigma(f75)))),universal_set). [resolve(4776,a,270,b)].
% 232.86/46.35
% 232.86/46.35 % given #1500 (T,wt=7): 26187 member(f23(natural_numbers,non_ordered_pair(A,f75)),universal_set). [resolve(26174,a,270,b)].
% 232.86/46.35
% 232.86/46.35 % given #2000 (T,wt=8): 14609 little_set(sigma(image(powerset(sigma(powerset(infinity))),f25))). [resolve(5422,a,262,a)].
% 232.86/46.35
% 232.86/46.35 % given #2500 (T,wt=8): 19504 little_set(powerset(sigma(powerset(sigma(f23(universal_set,universal_set)))))). [resolve(10292,a,256,a)].
% 232.86/46.35
% 232.86/46.35 % given #3000 (T,wt=8): 24347 member(powerset(powerset(powerset(f23(natural_numbers,universal_set)))),universal_set). [resolve(23894,a,270,b)].
% 232.86/46.35
% 232.86/46.35 % given #3500 (T,wt=6): 47186 little_set(sigma(sigma(f16(f75,universal_set)))). [resolve(47057,a,262,a)].
% 232.86/46.35
% 232.86/46.35 % given #4000 (T,wt=8): 53226 ordered_pair_predicate(sigma(powerset(powerset(infinity)))) | little_set(f18(universal_set)). [resolve(8203,b,341,a)].
% 232.86/46.35
% 232.86/46.35 % SZS status Unsatisfiable for theBenchmark
% 232.86/46.35
% 232.86/46.35 % Proof 1 at 23.44 (+ 6.18) seconds.
% 232.86/46.35 % Length of proof is 20.
% 232.86/46.35 % Level of proof is 5.
% 232.86/46.35 % Maximum clause weight is 10.000.
% 232.86/46.35 % Given clauses 4400.
% 232.86/46.35
% 232.86/46.35 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------