%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU265+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:45:37 AM UTC 2026
% Result : Theorem 3.72s 0.96s
% Output : CNFRefutation 3.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 14
% Syntax : Number of formulae : 88 ( 15 unt; 0 def)
% Number of atoms : 262 ( 76 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 284 ( 110 ~; 129 |; 27 &)
% ( 6 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 4 con; 0-3 aty)
% Number of variables : 183 ( 29 sgn 82 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('theBenchmark.p',cc1_relset_1) ).
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d4_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('theBenchmark.p',d4_relat_1) ).
fof(d5_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(dt_k4_relset_1,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> element(relation_dom_as_subset(A,B,C),powerset(A)) ),
file('theBenchmark.p',dt_k4_relset_1) ).
fof(dt_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('theBenchmark.p',dt_m2_relset_1) ).
fof(redefinition_k4_relset_1,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_dom_as_subset(A,B,C) = relation_dom(C) ),
file('theBenchmark.p',redefinition_k4_relset_1) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t20_relat_1,axiom,
! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(B,relation_rng(C))
& in(A,relation_dom(C)) ) ) ),
file('theBenchmark.p',t20_relat_1) ).
fof(t2_subset,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t2_tarski,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('theBenchmark.p',t2_tarski) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t22_relset_1,conjecture,
! [A,B,C] :
( relation_of2_as_subset(C,B,A)
=> ( ! [D] :
~ ( ! [E] : ~ in(ordered_pair(D,E),C)
& in(D,B) )
<=> relation_dom_as_subset(B,A,C) = B ) ),
file('theBenchmark.p',t22_relset_1) ).
fof(t22_relset_1_neg,negated_conjecture,
~ ! [A,B,C] :
( relation_of2_as_subset(C,B,A)
=> ( ! [D] :
~ ( ! [E] : ~ in(ordered_pair(D,E),C)
& in(D,B) )
<=> relation_dom_as_subset(B,A,C) = B ) ),
inference(assume_negation,[status(cth)],[t22_relset_1]) ).
fof(nnf_4,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) )
& ( ? [X3] : in(ordered_pair(C,X3),A)
| in(C,B) ) )
| relation_dom(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X0,X2),A)
| in(X0,B) )
& ( ? [X1] : in(ordered_pair(X0,X1),A)
| ~ in(X0,B) ) )
| relation_dom(A) != B ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d4_relat_1]) ).
fof(sk_d4_relat_1_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ! [D] : ~ in(ordered_pair(sK7(A,B),D),A)
| ~ in(sK7(A,B),B) )
& ( in(ordered_pair(sK7(A,B),sK8(A,B)),A)
| in(sK7(A,B),B) ) )
| relation_dom(A) = B )
& ( ! [X0] :
( ( ! [X2] : ~ in(ordered_pair(X0,X2),A)
| in(X0,B) )
& ( in(ordered_pair(X0,sK0(A,B,X0)),A)
| ~ in(X0,B) ) )
| relation_dom(A) != B ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK7,sK8]),skolemize(X1,sK0(A,B,X0)),skolemize(C,sK7(A,B)),skolemize(X3,sK8(A,B))],[nnf_4]) ).
fof(sk_d4_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ in(ordered_pair(sK7(VAR_0,VAR_1),VAR_2),VAR_0)
| ~ in(sK7(VAR_0,VAR_1),VAR_1)
| relation_dom(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK7(VAR_0,VAR_1),sK8(VAR_0,VAR_1)),VAR_0)
| in(sK7(VAR_0,VAR_1),VAR_1)
| relation_dom(VAR_0) = VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(ordered_pair(VAR_2,VAR_3),VAR_0)
| in(VAR_2,VAR_1)
| relation_dom(VAR_0) != VAR_1
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(VAR_2,sK0(VAR_0,VAR_1,VAR_2)),VAR_0)
| ~ in(VAR_2,VAR_1)
| relation_dom(VAR_0) != VAR_1
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d4_relat_1_sk]) ).
cnf(c_38,plain,
( in(ordered_pair(C,sK0(A,B,C)),A)
| ~ in(C,B)
| relation_dom(A) != B
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d4_relat_1]) ).
cnf(c_39,plain,
( relation(A)
| ~ element(A,powerset(cartesian_product2(B,C))) ),
inference(clausify,[status(thm)],[cc1_relset_1]) ).
cnf(c_43,plain,
( in(B,relation_dom(A))
| ~ in(ordered_pair(B,C),A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t20_relat_1]) ).
cnf(c_45,plain,
( relation_of2(A,B,C)
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_47,plain,
( relation_dom_as_subset(B,C,A) = relation_dom(A)
| ~ relation_of2(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k4_relset_1]) ).
cnf(c_49,plain,
( element(relation_dom_as_subset(B,C,A),powerset(B))
| ~ relation_of2(A,B,C) ),
inference(clausify,[status(thm)],[dt_k4_relset_1]) ).
cnf(c_51,plain,
( ~ relation_of2_as_subset(C,A,B)
| element(relation_dom_as_subset(A,B,C),powerset(A)) ),
inference(resolve,[status(thm)],[c_49,c_45]) ).
cnf(c_52,plain,
( ~ relation_of2_as_subset(C,A,B)
| relation_dom_as_subset(A,B,C) = relation_dom(C) ),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_53,plain,
( element(A,powerset(cartesian_product2(B,C)))
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[dt_m2_relset_1]) ).
fof(nnf_37,plain,
? [A,B,C] :
( ( relation_dom_as_subset(B,A,C) != B
| ? [D] :
( ! [E] : ~ in(ordered_pair(D,E),C)
& in(D,B) ) )
& ( relation_dom_as_subset(B,A,C) = B
| ! [X3] :
( ? [X0] : in(ordered_pair(X3,X0),C)
| ~ in(X3,B) ) )
& relation_of2_as_subset(C,B,A) ),
inference(fof_nnf,[status(thm)],[t22_relset_1_neg]) ).
fof(sk_t22_relset_1_neg_sk,plain,
( ( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| ( ! [E] : ~ in(ordered_pair(sK6,E),sK1)
& in(sK6,sK2) ) )
& ( relation_dom_as_subset(sK2,sK3,sK1) = sK2
| ! [X3] :
( in(ordered_pair(X3,sK5(X3)),sK1)
| ~ in(X3,sK2) ) )
& relation_of2_as_subset(sK1,sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK5,sK6]),skolemize(A,sK3),skolemize(B,sK2),skolemize(C,sK1),skolemize(X0,sK5(X3)),skolemize(D,sK6)],[nnf_37]) ).
fof(sk_t22_relset_1_neg,plain,
( ! [VAR_0] :
( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| ~ in(ordered_pair(sK6,VAR_0),sK1) )
& ( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| in(sK6,sK2) )
& ! [VAR_0] :
( relation_dom_as_subset(sK2,sK3,sK1) = sK2
| in(ordered_pair(VAR_0,sK5(VAR_0)),sK1)
| ~ in(VAR_0,sK2) )
& relation_of2_as_subset(sK1,sK2,sK3) ),
inference(cnf_transformation,[status(thm)],[sk_t22_relset_1_neg_sk]) ).
cnf(c_55,negated_conjecture,
relation_of2_as_subset(sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_t22_relset_1_neg]) ).
cnf(c_63,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_64,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_72,plain,
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
fof(nnf_30,plain,
! [A,B] :
( B = A
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(fof_nnf,[status(thm)],[t2_tarski]) ).
fof(sk_t2_tarski_sk,plain,
! [A,B] :
( B = A
| ( ( ~ in(sK4(A,B),B)
| ~ in(sK4(A,B),A) )
& ( in(sK4(A,B),B)
| in(sK4(A,B),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(C,sK4(A,B))],[nnf_30]) ).
fof(sk_t2_tarski,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ in(sK4(VAR_0,VAR_1),VAR_1)
| ~ in(sK4(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| in(sK4(VAR_0,VAR_1),VAR_1)
| in(sK4(VAR_0,VAR_1),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t2_tarski_sk]) ).
cnf(c_73,plain,
( B = A
| in(sK4(A,B),B)
| in(sK4(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_74,plain,
( B = A
| ~ in(sK4(A,B),B)
| ~ in(sK4(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_75,plain,
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_76,plain,
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
cnf(c_80,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) = sK2
| in(ordered_pair(A,sK5(A)),sK1)
| ~ in(A,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t22_relset_1_neg]) ).
cnf(c_2616,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) = sK2
| in(unordered_pair(unordered_pair(A,sK5(A)),singleton(A)),sK1)
| ~ in(A,sK2) ),
inference(paramod,[status(thm)],[c_64,c_80]) ).
cnf(c_81,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) = sK2
| in(unordered_pair(singleton(A),unordered_pair(A,sK5(A))),sK1)
| ~ in(A,sK2) ),
inference(paramod,[status(thm)],[c_63,c_2616]) ).
cnf(c_82,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| in(sK6,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t22_relset_1_neg]) ).
cnf(c_83,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| ~ in(ordered_pair(sK6,A),sK1) ),
inference(split_conjunct,[status(thm)],[sk_t22_relset_1_neg]) ).
cnf(c_84,negated_conjecture,
( relation_dom_as_subset(sK2,sK3,sK1) != sK2
| ~ in(unordered_pair(unordered_pair(sK6,A),singleton(sK6)),sK1) ),
inference(paramod,[status(thm)],[c_64,c_83]) ).
cnf(c_85,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(ordered_pair(C,sK0(A,B,C)),A)
| ~ in(C,B)
| relation_dom(A) != B ),
inference(resolve,[status(thm)],[c_38,c_39]) ).
cnf(c_2617,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(unordered_pair(unordered_pair(C,sK0(A,B,C)),singleton(C)),A)
| ~ in(C,B)
| relation_dom(A) != B ),
inference(paramod,[status(thm)],[c_64,c_85]) ).
cnf(c_86,plain,
( ~ element(A,powerset(cartesian_product2(D,E)))
| in(unordered_pair(singleton(C),unordered_pair(C,sK0(A,B,C))),A)
| ~ in(C,B)
| relation_dom(A) != B ),
inference(paramod,[status(thm)],[c_63,c_2617]) ).
cnf(c_93,plain,
( ~ element(C,powerset(cartesian_product2(D,E)))
| in(A,relation_dom(C))
| ~ in(ordered_pair(A,B),C) ),
inference(resolve,[status(thm)],[c_43,c_39]) ).
cnf(c_94,plain,
( ~ element(C,powerset(cartesian_product2(D,E)))
| in(A,relation_dom(C))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),C) ),
inference(paramod,[status(thm)],[c_64,c_93]) ).
cnf(c_105,negated_conjecture,
element(sK1,powerset(cartesian_product2(sK2,sK3))),
inference(resolve,[status(thm)],[c_55,c_53]) ).
cnf(c_106,negated_conjecture,
relation_dom_as_subset(sK2,sK3,sK1) = relation_dom(sK1),
inference(resolve,[status(thm)],[c_55,c_52]) ).
cnf(c_107,negated_conjecture,
element(relation_dom_as_subset(sK2,sK3,sK1),powerset(sK2)),
inference(resolve,[status(thm)],[c_55,c_51]) ).
cnf(c_108,negated_conjecture,
element(relation_dom(sK1),powerset(sK2)),
inference(paramod,[status(thm)],[c_106,c_107]) ).
cnf(c_110,negated_conjecture,
( relation_dom(sK1) != sK2
| ~ in(unordered_pair(unordered_pair(sK6,A),singleton(sK6)),sK1) ),
inference(paramod,[status(thm)],[c_106,c_84]) ).
cnf(c_111,negated_conjecture,
( relation_dom(sK1) != sK2
| in(sK6,sK2) ),
inference(paramod,[status(thm)],[c_106,c_82]) ).
cnf(c_112,negated_conjecture,
( relation_dom(sK1) = sK2
| in(unordered_pair(singleton(A),unordered_pair(A,sK5(A))),sK1)
| ~ in(A,sK2) ),
inference(paramod,[status(thm)],[c_106,c_81]) ).
cnf(c_181,plain,
( in(A,relation_dom(sK1))
| ~ in(unordered_pair(unordered_pair(A,B),singleton(A)),sK1) ),
inference(resolve,[status(thm)],[c_105,c_94]) ).
cnf(c_189,plain,
( ~ empty(sK2)
| ~ in(A,relation_dom(sK1)) ),
inference(resolve,[status(thm)],[c_108,c_76]) ).
cnf(c_190,plain,
( element(A,sK2)
| ~ in(A,relation_dom(sK1)) ),
inference(resolve,[status(thm)],[c_108,c_75]) ).
cnf(c_209,plain,
( relation_dom(sK1) != sK2
| ~ in(unordered_pair(singleton(sK6),unordered_pair(sK6,A)),sK1) ),
inference(paramod,[status(thm)],[c_63,c_110]) ).
cnf(c_210,plain,
( sK2 = A
| in(sK4(A,sK2),A)
| relation_dom(sK1) = sK2
| in(unordered_pair(singleton(sK4(A,sK2)),unordered_pair(sK4(A,sK2),sK5(sK4(A,sK2)))),sK1) ),
inference(resolve,[status(thm)],[c_112,c_73]) ).
cnf(c_459,plain,
( in(A,relation_dom(sK1))
| ~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK1) ),
inference(paramod,[status(thm)],[c_63,c_181]) ).
cnf(c_1971,plain,
( in(sK4(A,sK2),relation_dom(sK1))
| sK2 = A
| in(sK4(A,sK2),A)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_210,c_459]) ).
cnf(c_2618,plain,
( sK2 = relation_dom(sK1)
| in(sK4(relation_dom(sK1),sK2),relation_dom(sK1))
| relation_dom(sK1) = sK2 ),
inference(factor,[status(thm)],[c_1971]) ).
cnf(c_2619,plain,
( relation_dom(sK1) = sK2
| in(sK4(relation_dom(sK1),sK2),relation_dom(sK1))
| relation_dom(sK1) = sK2 ),
inference(copy,[status(thm)],[c_2618]) ).
cnf(c_1985,plain,
( in(sK4(relation_dom(sK1),sK2),relation_dom(sK1))
| relation_dom(sK1) = sK2 ),
inference(copy,[status(thm)],[c_2619]) ).
cnf(c_2002,plain,
( element(sK4(relation_dom(sK1),sK2),sK2)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_1985,c_190]) ).
cnf(c_2003,plain,
( ~ empty(sK2)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_1985,c_189]) ).
cnf(c_2620,plain,
( sK2 = relation_dom(sK1)
| ~ in(sK4(relation_dom(sK1),sK2),sK2)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_1985,c_74]) ).
cnf(c_2621,plain,
( relation_dom(sK1) = sK2
| ~ in(sK4(relation_dom(sK1),sK2),sK2)
| relation_dom(sK1) = sK2 ),
inference(copy,[status(thm)],[c_2620]) ).
cnf(c_2012,plain,
( ~ in(sK4(relation_dom(sK1),sK2),sK2)
| relation_dom(sK1) = sK2 ),
inference(copy,[status(thm)],[c_2621]) ).
cnf(c_2015,plain,
( in(sK4(relation_dom(sK1),sK2),sK2)
| empty(sK2)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_2002,c_72]) ).
cnf(c_2622,plain,
( relation_dom(sK1) = sK2
| empty(sK2)
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_2015,c_2012]) ).
cnf(c_2104,plain,
( empty(sK2)
| relation_dom(sK1) = sK2 ),
inference(copy,[status(thm)],[c_2622]) ).
cnf(c_2623,plain,
( relation_dom(sK1) = sK2
| relation_dom(sK1) = sK2 ),
inference(resolve,[status(thm)],[c_2104,c_2003]) ).
cnf(c_2105,plain,
relation_dom(sK1) = sK2,
inference(copy,[status(thm)],[c_2623]) ).
cnf(c_2624,plain,
( sK2 != sK2
| ~ in(unordered_pair(singleton(sK6),unordered_pair(sK6,A)),sK1) ),
inference(paramod,[status(thm)],[c_2105,c_209]) ).
cnf(c_2204,plain,
~ in(unordered_pair(singleton(sK6),unordered_pair(sK6,A)),sK1),
inference(copy,[status(thm)],[c_2624]) ).
cnf(c_2625,negated_conjecture,
( sK2 != sK2
| in(sK6,sK2) ),
inference(paramod,[status(thm)],[c_2105,c_111]) ).
cnf(c_2212,negated_conjecture,
in(sK6,sK2),
inference(copy,[status(thm)],[c_2625]) ).
cnf(c_2626,negated_conjecture,
( ~ element(A,powerset(cartesian_product2(B,C)))
| in(unordered_pair(singleton(sK6),unordered_pair(sK6,sK0(A,sK2,sK6))),A)
| relation_dom(A) != sK2 ),
inference(resolve,[status(thm)],[c_86,c_2212]) ).
cnf(c_2627,negated_conjecture,
( ~ element(sK1,powerset(cartesian_product2(A,B)))
| relation_dom(sK1) != sK2 ),
inference(resolve,[status(thm)],[c_2626,c_2204]) ).
cnf(c_2628,negated_conjecture,
relation_dom(sK1) != sK2,
inference(resolve,[status(thm)],[c_2627,c_105]) ).
cnf(c_2629,negated_conjecture,
sK2 != sK2,
inference(paramod,[status(thm)],[c_2105,c_2628]) ).
cnf(c_2615,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2629]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU265+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 09:04:59 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 3655444 was started by sandbox2 on n015,
% 0.12/0.36 % Sat Sep 26 09:04:59 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 3.72/0.96
% 3.72/0.96 % given #500 (F,wt=25): 1090 -in(unordered_pair(unordered_pair(unordered_pair(unordered_pair(A,B),singleton(A)),C),singleton(unordered_pair(unordered_pair(A,B),singleton(A)))),f6(unordered_pair(singleton(A),unordered_pair(B,A)),D)). [ur(162,b,576,a)].
% 3.72/0.96
% 3.72/0.96 % SZS status Theorem for theBenchmark
% 3.72/0.96
% 3.72/0.96 % Proof 1 at 0.43 (+ 0.09) seconds.
% 3.72/0.96 % Length of proof is 64.
% 3.72/0.96 % Level of proof is 13.
% 3.72/0.96 % Maximum clause weight is 27.000.
% 3.72/0.96 % Given clauses 609.
% 3.72/0.96
% 3.72/0.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------