%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET957+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 02:11:03 PM UTC 2026
% Result : Theorem 0.16s 0.55s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 25
% Syntax : Number of formulae : 120 ( 19 unt; 19 def)
% Number of atoms : 305 ( 50 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 310 ( 125 ~; 126 |; 31 &)
% ( 23 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 23 ( 21 usr; 20 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 138 ( 114 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C,D] :
~ ( ! [E,F] :
~ ( D = ordered_pair(E,F)
& in(F,C)
& in(E,B) )
& in(D,A)
& subset(A,cartesian_product2(B,C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,conjecture,
! [A,B,C,D,E,F] :
( ( ! [G,H] :
( in(ordered_pair(G,H),A)
<=> in(ordered_pair(G,H),D) )
& subset(D,cartesian_product2(E,F))
& subset(A,cartesian_product2(B,C)) )
=> A = D ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
~ ! [A,B,C,D,E,F] :
( ( ! [G,H] :
( in(ordered_pair(G,H),A)
<=> in(ordered_pair(G,H),D) )
& subset(D,cartesian_product2(E,F))
& subset(A,cartesian_product2(B,C)) )
=> A = D ),
inference(negated_conjecture,[status(cth)],[f9]) ).
fof(f11,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f14,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f15,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f23,plain,
! [A,B,C,D] :
( ? [E,F] :
( D = ordered_pair(E,F)
& in(F,C)
& in(E,B) )
| ~ in(D,A)
| ~ subset(A,cartesian_product2(B,C)) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f24,plain,
! [B,C,D] :
( ? [E,F] :
( D = ordered_pair(E,F)
& in(F,C)
& in(E,B) )
| ! [A] :
( ~ in(D,A)
| ~ subset(A,cartesian_product2(B,C)) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f25,plain,
! [B,C,D] :
( ( D = ordered_pair(sK2_skl(D,C,B),sK3_skl(D,C,B))
& in(sK3_skl(D,C,B),C)
& in(sK2_skl(D,C,B),B) )
| ! [A] :
( ~ in(D,A)
| ~ subset(A,cartesian_product2(B,C)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(E,sK2_skl(D,C,B)),skolemize(F,sK3_skl(D,C,B))],[f24]) ).
fof(f28,plain,
! [X0,X1,X2,X3] :
( X3 = ordered_pair(sK2_skl(X3,X2,X1),sK3_skl(X3,X2,X1))
| ~ in(X3,X0)
| ~ subset(X0,cartesian_product2(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f29,plain,
? [A,B,C,D,E,F] :
( A != D
& ! [G,H] :
( in(ordered_pair(G,H),A)
<=> in(ordered_pair(G,H),D) )
& subset(D,cartesian_product2(E,F))
& subset(A,cartesian_product2(B,C)) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
? [A,B,C,D,E,F] :
( A != D
& ! [G,H] :
( ( ~ in(ordered_pair(G,H),D)
| in(ordered_pair(G,H),A) )
& ( in(ordered_pair(G,H),D)
| ~ in(ordered_pair(G,H),A) ) )
& subset(D,cartesian_product2(E,F))
& subset(A,cartesian_product2(B,C)) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
? [A,D] :
( A != D
& ! [G,H] :
( ~ in(ordered_pair(G,H),D)
| in(ordered_pair(G,H),A) )
& ! [G,H] :
( in(ordered_pair(G,H),D)
| ~ in(ordered_pair(G,H),A) )
& ? [E,F] : subset(D,cartesian_product2(E,F))
& ? [B,C] : subset(A,cartesian_product2(B,C)) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f32,plain,
( sK4_skl != sK5_skl
& ! [G,H] :
( ~ in(ordered_pair(G,H),sK5_skl)
| in(ordered_pair(G,H),sK4_skl) )
& ! [G,H] :
( in(ordered_pair(G,H),sK5_skl)
| ~ in(ordered_pair(G,H),sK4_skl) )
& subset(sK5_skl,cartesian_product2(sK8_skl,sK9_skl))
& subset(sK4_skl,cartesian_product2(sK6_skl,sK7_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(A,sK4_skl),skolemize(D,sK5_skl),skolemize(B,sK6_skl),skolemize(C,sK7_skl),skolemize(E,sK8_skl),skolemize(F,sK9_skl)],[f31]) ).
fof(f33,plain,
subset(sK4_skl,cartesian_product2(sK6_skl,sK7_skl)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
subset(sK5_skl,cartesian_product2(sK8_skl,sK9_skl)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f35,plain,
! [X0,X1] :
( in(ordered_pair(X0,X1),sK5_skl)
| ~ in(ordered_pair(X0,X1),sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f36,plain,
! [X0,X1] :
( ~ in(ordered_pair(X0,X1),sK5_skl)
| in(ordered_pair(X0,X1),sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f37,plain,
sK4_skl != sK5_skl,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f38,plain,
! [A,B] :
( A = B
| ? [C] :
( in(C,A)
<~> in(C,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f39,plain,
! [A,B] :
( A = B
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(NNF_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [A,B] :
( A = B
| ( ( ~ in(sK10_skl(B,A),B)
| ~ in(sK10_skl(B,A),A) )
& ( in(sK10_skl(B,A),B)
| in(sK10_skl(B,A),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f39]) ).
fof(f41,plain,
! [X0,X1] :
( X1 = X0
| in(sK10_skl(X0,X1),X0)
| in(sK10_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( X1 = X0
| ~ in(sK10_skl(X0,X1),X0)
| ~ in(sK10_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
! [X0,X1] :
( ~ in(ordered_pair(X0,X1),sK4_skl)
| ~ in(sK5_skl,ordered_pair(X0,X1)) ),
inference(resolution,[status(thm)],[f13,f35]) ).
fof(f49,plain,
! [X0,X1] : ordered_pair(unordered_pair(X0,X1),singleton(X0)) = unordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),
inference(paramodulation,[status(thm)],[f15,f15]) ).
fof(f50,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X1,X0),singleton(X0)),
inference(paramodulation,[status(thm)],[f14,f15]) ).
fof(f63,plain,
! [X0] :
( X0 = ordered_pair(sK2_skl(X0,sK9_skl,sK8_skl),sK3_skl(X0,sK9_skl,sK8_skl))
| ~ in(X0,sK5_skl) ),
inference(resolution,[status(thm)],[f28,f34]) ).
fof(f64,plain,
! [X0] :
( X0 = ordered_pair(sK2_skl(X0,sK7_skl,sK6_skl),sK3_skl(X0,sK7_skl,sK6_skl))
| ~ in(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f28,f33]) ).
fof(f67,plain,
! [X0,X1] : ordered_pair(unordered_pair(unordered_pair(X0,X1),singleton(X1)),singleton(unordered_pair(X0,X1))) = unordered_pair(ordered_pair(unordered_pair(X0,X1),singleton(X1)),singleton(ordered_pair(X1,X0))),
inference(paramodulation,[status(thm)],[f50,f49]) ).
fof(f68,plain,
! [X0,X1] : ordered_pair(unordered_pair(unordered_pair(X0,X1),singleton(X0)),singleton(unordered_pair(X0,X1))) = unordered_pair(ordered_pair(unordered_pair(X0,X1),singleton(X0)),singleton(ordered_pair(X0,X1))),
inference(paramodulation,[status(thm)],[f15,f49]) ).
fof(f74,plain,
! [X0,X1] : ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))) = unordered_pair(ordered_pair(unordered_pair(X1,X0),singleton(X0)),singleton(ordered_pair(X0,X1))),
inference(forward_demodulation,[status(thm)],[f50,f67]) ).
fof(f75,plain,
! [X0,X1] : ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))) = unordered_pair(ordered_pair(unordered_pair(X0,X1),singleton(X0)),singleton(ordered_pair(X0,X1))),
inference(forward_demodulation,[status(thm)],[f15,f68]) ).
fof(f78,plain,
! [X0] :
( sK5_skl = X0
| in(sK10_skl(X0,sK5_skl),X0)
| sK10_skl(X0,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(X0,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(X0,sK5_skl),sK9_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f63,f41]) ).
fof(f89,plain,
( sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl))
| sK5_skl = sK4_skl
| sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f78,f64]) ).
fof(f102,definition,
( sQ3_spl
<=> sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f103,plain,
( ~ sQ3_spl
| sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f102]) ).
fof(f105,definition,
( sQ4_spl
<=> sK5_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f106,plain,
( ~ sQ4_spl
| sK5_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f108,definition,
( sQ5_spl
<=> sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f109,plain,
( ~ sQ5_spl
| sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,plain,
( sQ5_spl
| sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f89,f102,f105,f108]) ).
fof(f148,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f106,f37]) ).
fof(f149,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f148]) ).
fof(f304,plain,
! [X0,X1] : ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))) = unordered_pair(ordered_pair(unordered_pair(X1,X0),singleton(X0)),singleton(ordered_pair(X0,X1))),
inference(paramodulation,[status(thm)],[f14,f75]) ).
fof(f324,plain,
! [X0,X1] : ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))) = ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),
inference(forward_demodulation,[status(thm)],[f74,f304]) ).
fof(f521,plain,
! [X0,X1] :
( ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),sK4_skl)
| ~ in(sK5_skl,ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0)))) ),
inference(paramodulation,[status(thm)],[f324,f43]) ).
fof(f522,plain,
! [X0,X1] :
( ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),sK5_skl)
| in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f324,f36]) ).
fof(f523,plain,
! [X0,X1] :
( in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),sK5_skl)
| ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f324,f35]) ).
fof(f532,plain,
! [X0,X1] :
( ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),sK4_skl)
| ~ in(sK5_skl,ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f324,f43]) ).
fof(f533,plain,
! [X0,X1] :
( ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),sK5_skl)
| in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f324,f36]) ).
fof(f534,plain,
! [X0,X1] :
( in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X0,X1))),sK5_skl)
| ~ in(ordered_pair(ordered_pair(X0,X1),singleton(unordered_pair(X1,X0))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f324,f35]) ).
fof(f756,plain,
( ~ sQ3_spl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK5_skl)
| in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)),sK4_skl) ),
inference(paramodulation,[status(thm)],[f103,f36]) ).
fof(f757,plain,
( ~ sQ3_spl
| in(sK10_skl(sK4_skl,sK5_skl),sK5_skl)
| ~ in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)),sK4_skl) ),
inference(paramodulation,[status(thm)],[f103,f35]) ).
fof(f765,definition,
( sQ16_spl
<=> in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ16_spl
| in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f767,plain,
( sQ16_spl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f772,definition,
( sQ18_spl
<=> in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f773,plain,
( ~ sQ18_spl
| in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)),sK4_skl) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f774,plain,
( sQ18_spl
| ~ in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)),sK4_skl) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f776,definition,
( sQ19_spl
<=> in(sK10_skl(sK4_skl,sK5_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( ~ sQ19_spl
| in(sK10_skl(sK4_skl,sK5_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f776]) ).
fof(f778,plain,
( sQ19_spl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f776]) ).
fof(f779,plain,
( ~ sQ3_spl
| ~ sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f756,f772,f776,f102]) ).
fof(f780,plain,
( ~ sQ3_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f757,f772,f776,f102]) ).
fof(f784,plain,
( ~ sQ18_spl
| ~ sQ3_spl
| in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f103,f773]) ).
fof(f807,definition,
( sQ21_spl
<=> sK10_skl(cartesian_product2(sK8_skl,sK9_skl),sK5_skl) = sK10_skl(cartesian_product2(sK8_skl,sK9_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f809,plain,
( sQ21_spl
| sK10_skl(cartesian_product2(sK8_skl,sK9_skl),sK5_skl) != sK10_skl(cartesian_product2(sK8_skl,sK9_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f816,plain,
( ~ sQ19_spl
| sK5_skl = sK4_skl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(resolution,[status(thm)],[f777,f42]) ).
fof(f817,plain,
( ~ sQ19_spl
| sK10_skl(sK4_skl,sK5_skl) = ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK9_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f777,f63]) ).
fof(f819,plain,
( ~ sQ19_spl
| sQ4_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f816,f765,f105,f776]) ).
fof(f820,plain,
( sQ16_spl
| ~ sQ18_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f784]) ).
fof(f821,plain,
( sQ16_spl
| ~ sQ18_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f820]) ).
fof(f822,plain,
( sQ18_spl
| ~ sQ3_spl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f103,f774]) ).
fof(f825,plain,
( sQ19_spl
| sK5_skl = sK4_skl
| in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(resolution,[status(thm)],[f778,f41]) ).
fof(f826,plain,
( sQ19_spl
| sQ4_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f825,f765,f105,f776]) ).
fof(f827,plain,
( ~ sQ16_spl
| sQ18_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f766,f822]) ).
fof(f828,plain,
( ~ sQ16_spl
| sQ18_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f827]) ).
fof(f829,plain,
( ~ sQ19_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f817,f102,f776]) ).
fof(f922,plain,
( sQ21_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f809]) ).
fof(f923,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f922]) ).
fof(f1615,definition,
( sQ44_spl
<=> sK10_skl(cartesian_product2(sK6_skl,sK7_skl),sK4_skl) = sK10_skl(cartesian_product2(sK6_skl,sK7_skl),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1617,plain,
( sQ44_spl
| sK10_skl(cartesian_product2(sK6_skl,sK7_skl),sK4_skl) != sK10_skl(cartesian_product2(sK6_skl,sK7_skl),sK4_skl) ),
inference(component_clause,[status(thm)],[f1615]) ).
fof(f1628,plain,
( sQ44_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1617]) ).
fof(f1629,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f1628]) ).
fof(f1812,plain,
( ~ sQ5_spl
| in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl)
| ~ in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f109,f534]) ).
fof(f1813,plain,
( ~ sQ5_spl
| ~ in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl)
| in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f109,f533]) ).
fof(f1814,plain,
( ~ sQ5_spl
| ~ in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl)
| ~ in(sK5_skl,ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl))))) ),
inference(paramodulation,[status(thm)],[f109,f532]) ).
fof(f1815,plain,
( ~ sQ5_spl
| in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl)
| ~ in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f109,f523]) ).
fof(f1816,plain,
( ~ sQ5_spl
| ~ in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl)
| in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
inference(paramodulation,[status(thm)],[f109,f522]) ).
fof(f1817,plain,
( ~ sQ5_spl
| ~ in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl)
| ~ in(sK5_skl,ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl))))) ),
inference(paramodulation,[status(thm)],[f109,f521]) ).
fof(f1832,plain,
( ~ sQ5_spl
| in(sK10_skl(sK4_skl,sK5_skl),sK5_skl)
| ~ in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),sK4_skl) ),
inference(paramodulation,[status(thm)],[f109,f35]) ).
fof(f1833,definition,
( sQ57_spl
<=> in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1836,definition,
( sQ58_spl
<=> in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1839,plain,
( ~ sQ5_spl
| sQ58_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f1812,f1833,f1836,f108]) ).
fof(f1840,definition,
( sQ59_spl
<=> in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1843,definition,
( sQ60_spl
<=> in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1846,plain,
( ~ sQ5_spl
| ~ sQ60_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1813,f1840,f1843,f108]) ).
fof(f1847,definition,
( sQ61_spl
<=> in(sK5_skl,ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( ~ sQ5_spl
| ~ sQ59_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f1814,f1847,f1840,f108]) ).
fof(f1851,definition,
( sQ62_spl
<=> in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1854,definition,
( sQ63_spl
<=> in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1857,plain,
( ~ sQ5_spl
| sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f1815,f1851,f1854,f108]) ).
fof(f1858,definition,
( sQ64_spl
<=> in(ordered_pair(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),singleton(unordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1861,definition,
( sQ65_spl
<=> in(ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)))),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1864,plain,
( ~ sQ5_spl
| ~ sQ65_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1816,f1858,f1861,f108]) ).
fof(f1865,definition,
( sQ66_spl
<=> in(sK5_skl,ordered_pair(sK10_skl(sK4_skl,sK5_skl),singleton(unordered_pair(sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1868,plain,
( ~ sQ5_spl
| ~ sQ64_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1817,f1865,f1858,f108]) ).
fof(f1880,definition,
( sQ68_spl
<=> in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1882,plain,
( sQ68_spl
| ~ in(ordered_pair(sK2_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK4_skl,sK5_skl),sK7_skl,sK6_skl)),sK4_skl) ),
inference(component_clause,[status(thm)],[f1880]) ).
fof(f1885,plain,
( ~ sQ5_spl
| sQ19_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f1832,f1880,f776,f108]) ).
fof(f1891,plain,
( sQ68_spl
| ~ sQ5_spl
| ~ in(sK10_skl(sK4_skl,sK5_skl),sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f109,f1882]) ).
fof(f1892,plain,
( sQ68_spl
| ~ sQ5_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1891,f766]) ).
fof(f1893,plain,
( sQ68_spl
| ~ sQ5_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f1892]) ).
fof(f1894,plain,
$false,
inference(sat_refutation,[status(thm)],[f111,f149,f779,f780,f819,f821,f826,f828,f829,f923,f1629,f1839,f1846,f1850,f1857,f1864,f1868,f1885,f1893]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET957+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n005.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 05:45:32 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 0.16/0.55 % Refutation found
% 0.16/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/0.60 % Elapsed time: 0.200746 seconds
% 0.16/0.60 % CPU time: 1.033698 seconds
% 0.16/0.60 % Total memory used: 122.361 MB
% 0.16/0.60 % Net memory used: 121.892 MB
%------------------------------------------------------------------------------