%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : RNG092+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 08:55:09 AM UTC 2026
% Result : Theorem 88.33s 88.64s
% Output : Proof 88.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 2
% Syntax : Number of formulae : 73 ( 38 unt; 0 def)
% Number of atoms : 852 ( 160 equ)
% Maximal formula atoms : 43 ( 11 avg)
% Number of connectives : 1065 ( 286 ~; 229 |; 538 &)
% ( 2 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-3 aty)
% Number of variables : 339 ( 2 sgn 188 !; 145 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsC_01,axiom,
aElement0(sz10),
file('theBenchmark.p',mSortsC_01) ).
fof(m__,conjecture,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ)) )
=> ( aIdeal0(sdtpldt1(xI,xJ))
| ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ)) )
& ! [W1] :
( aElementOf0(W1,sdtpldt1(xI,xJ))
=> aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ)) ) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(f_3_1,plain,
aElement0(sz10),
inference(fof_nnf,[status(thm)],[mSortsC_01]) ).
cnf(f_3_2,plain,
aElement0(sz10),
inference(clausify,[status(thm)],[f_3_1]) ).
fof(f_26_1,negated_conjecture,
( ~ ( aIdeal0(sdtpldt1(xI,xJ))
| ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ)) )
& ! [W1] :
( aElementOf0(W1,sdtpldt1(xI,xJ))
=> aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ)) ) ) ) )
& ! [W0] :
( aElementOf0(W0,sdtpldt1(xI,xJ))
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ( aElement0(W2)
& ( aElementOf0(W1,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W1
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
& ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ? [W3,W4] :
( sdtpldt0(W3,W4) = W0
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) ) ),
inference(negate,[status(cth)],[m__]) ).
fof(f_26_2,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [W0] :
( ( ? [W1] :
( ~ aElementOf0(sdtasdt0(W1,W0),sdtpldt1(xI,xJ))
& aElement0(W1) )
| ? [W1] :
( ~ aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& aElementOf0(W1,sdtpldt1(xI,xJ)) ) )
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
& ! [W0] :
( ( aElementOf0(W0,sdtpldt1(xI,xJ))
| ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,xJ)
| ~ aElementOf0(W1,xI) ) )
& ( ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,xJ)
& aElementOf0(W1,xI) )
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtasdt0(W2,W0)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W7,W8] :
( sdtpldt0(W7,W8) = sdtpldt0(W0,W1)
& aElementOf0(W8,xJ)
& aElementOf0(W7,xI) )
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| ~ aElement0(W2)
| ( ~ aElementOf0(W1,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W1
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) )
| ( ~ aElementOf0(W0,sdtpldt1(xI,xJ))
& ! [W3,W4] :
( sdtpldt0(W3,W4) != W0
| ~ aElementOf0(W4,xJ)
| ~ aElementOf0(W3,xI) ) ) ) ),
inference(fof_nnf,[status(thm)],[f_26_1]) ).
fof(f_26_3,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_97] :
( ( aElementOf0(U_97,sdtpldt1(xI,xJ))
| ! [U_96,U_95] :
( sdtpldt0(U_96,U_95) != U_97
| ~ aElementOf0(U_95,xJ)
| ~ aElementOf0(U_96,xI) ) )
& ( ? [U_94,U_93] :
( sdtpldt0(U_94,U_93) = U_97
& aElementOf0(U_93,xJ)
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_97,sdtpldt1(xI,xJ)) ) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ? [U_89,U_88] :
( ? [U_87,U_86] :
( aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85,U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ)
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& ? [U_83,U_82] :
( sdtpldt0(U_83,U_82) = sdtpldt0(U_92,U_91)
& aElementOf0(U_82,xJ)
& aElementOf0(U_83,xI) )
& sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(U_89,U_87),sdtpldt0(U_88,U_86))
& aElementOf0(sdtasdt0(U_90,U_88),xJ)
& aElementOf0(sdtasdt0(U_90,U_89),xI)
& aElementOf0(sdtpldt0(U_88,U_86),xJ)
& aElementOf0(sdtpldt0(U_89,U_87),xI)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ)
& aElementOf0(U_87,xI) )
& U_92 = sdtpldt0(U_89,U_88)
& aElementOf0(U_88,xJ)
& aElementOf0(U_89,xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81,U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ)
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79,U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ)
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(variable_rename,[status(thm)],[f_26_2]) ).
fof(f_26_4,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ? [U_89] :
( ? [U_88] :
( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(U_89,U_87),sdtpldt0(U_88,U_86))
& aElementOf0(sdtpldt0(U_88,U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(U_89,U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85] :
( ? [U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& ? [U_83] :
( ? [U_82] :
( sdtpldt0(U_83,U_82) = sdtpldt0(U_92,U_91)
& aElementOf0(U_82,xJ) )
& aElementOf0(U_83,xI) )
& aElementOf0(sdtasdt0(U_90,U_88),xJ)
& aElementOf0(sdtasdt0(U_90,U_89),xI)
& U_92 = sdtpldt0(U_89,U_88)
& aElementOf0(U_88,xJ) )
& aElementOf0(U_89,xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(miniscope,[status(thm)],[f_26_3]) ).
fof(f_26_5,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_88] :
( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(U_88,U_86))
& aElementOf0(sdtpldt0(U_88,U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85] :
( ? [U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& ? [U_83] :
( ? [U_82] :
( sdtpldt0(U_83,U_82) = sdtpldt0(U_92,U_91)
& aElementOf0(U_82,xJ) )
& aElementOf0(U_83,xI) )
& aElementOf0(sdtasdt0(U_90,U_88),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),U_88)
& aElementOf0(U_88,xJ) )
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_89,sK14(U_92,U_91,U_90))],[f_26_4]) ).
fof(f_26_6,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85] :
( ? [U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& ? [U_83] :
( ? [U_82] :
( sdtpldt0(U_83,U_82) = sdtpldt0(U_92,U_91)
& aElementOf0(U_82,xJ) )
& aElementOf0(U_83,xI) )
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_88,sK15(U_92,U_91,U_90))],[f_26_5]) ).
fof(f_26_7,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85] :
( ? [U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& ? [U_82] :
( sdtpldt0(sK16(U_92,U_91,U_90),U_82) = sdtpldt0(U_92,U_91)
& aElementOf0(U_82,xJ) )
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_83,sK16(U_92,U_91,U_90))],[f_26_6]) ).
fof(f_26_8,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_85] :
( ? [U_84] :
( sdtpldt0(U_85,U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(U_85,xI) )
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_82,sK17(U_92,U_91,U_90))],[f_26_7]) ).
fof(f_26_9,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& ? [U_84] :
( sdtpldt0(sK18(U_92,U_91,U_90),U_84) = sdtasdt0(U_90,U_92)
& aElementOf0(U_84,xJ) )
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_85,sK18(U_92,U_91,U_90))],[f_26_8]) ).
fof(f_26_10,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_87] :
( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(U_87,U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),U_87),xI)
& aElementOf0(U_87,xI) )
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_84,sK19(U_92,U_91,U_90))],[f_26_9]) ).
fof(f_26_11,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( ? [U_86] :
( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),U_86))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),U_86),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),U_86)
& aElementOf0(U_86,xJ) )
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_87,sK20(U_92,U_91,U_90))],[f_26_10]) ).
fof(f_26_12,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ? [U_94] :
( ? [U_93] :
( sdtpldt0(U_94,U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(U_94,xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_86,sK21(U_92,U_91,U_90))],[f_26_11]) ).
fof(f_26_13,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ( ? [U_93] :
( sdtpldt0(sK22(U_101),U_93) = U_101
& aElementOf0(U_93,xJ) )
& aElementOf0(sK22(U_101),xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_94,sK22(U_101))],[f_26_12]) ).
fof(f_26_14,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ? [U_100] :
( ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,U_100),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(U_100,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(U_100,sdtpldt1(xI,xJ)) )
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ( sdtpldt0(sK22(U_101),sK23(U_101)) = U_101
& aElementOf0(sK23(U_101),xJ)
& aElementOf0(sK22(U_101),xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_93,sK23(U_101))],[f_26_13]) ).
fof(f_26_15,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,sK24),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ? [U_98] :
( ~ aElementOf0(sdtpldt0(sK24,U_98),sdtpldt1(xI,xJ))
& aElementOf0(U_98,sdtpldt1(xI,xJ)) ) )
& aElementOf0(sK24,sdtpldt1(xI,xJ))
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ( sdtpldt0(sK22(U_101),sK23(U_101)) = U_101
& aElementOf0(sK23(U_101),xJ)
& aElementOf0(sK22(U_101),xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_100,sK24)],[f_26_14]) ).
fof(f_26_16,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ( ? [U_99] :
( ~ aElementOf0(sdtasdt0(U_99,sK24),sdtpldt1(xI,xJ))
& aElement0(U_99) )
| ( ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ))
& aElementOf0(sK25,sdtpldt1(xI,xJ)) ) )
& aElementOf0(sK24,sdtpldt1(xI,xJ))
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ( sdtpldt0(sK22(U_101),sK23(U_101)) = U_101
& aElementOf0(sK23(U_101),xJ)
& aElementOf0(sK22(U_101),xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_98,sK25)],[f_26_15]) ).
fof(f_26_17,negated_conjecture,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ( ( ~ aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
& aElement0(sK26) )
| ( ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ))
& aElementOf0(sK25,sdtpldt1(xI,xJ)) ) )
& aElementOf0(sK24,sdtpldt1(xI,xJ))
& ! [U_102] :
( aElementOf0(U_102,sdtpldt1(xI,xJ))
| ! [U_96] :
( ! [U_95] :
( sdtpldt0(U_96,U_95) != U_102
| ~ aElementOf0(U_95,xJ) )
| ~ aElementOf0(U_96,xI) ) )
& ! [U_101] :
( ( sdtpldt0(sK22(U_101),sK23(U_101)) = U_101
& aElementOf0(sK23(U_101),xJ)
& aElementOf0(sK22(U_101),xI) )
| ~ aElementOf0(U_101,sdtpldt1(xI,xJ)) )
& aSet0(sdtpldt1(xI,xJ))
& ! [U_92,U_91,U_90] :
( ( sdtpldt0(U_92,U_91) = sdtpldt0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)))
& aElementOf0(sdtpldt0(sK15(U_92,U_91,U_90),sK21(U_92,U_91,U_90)),xJ)
& U_91 = sdtpldt0(sK20(U_92,U_91,U_90),sK21(U_92,U_91,U_90))
& aElementOf0(sK21(U_92,U_91,U_90),xJ)
& aElementOf0(sdtpldt0(sK14(U_92,U_91,U_90),sK20(U_92,U_91,U_90)),xI)
& aElementOf0(sK20(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ))
& sdtpldt0(sK18(U_92,U_91,U_90),sK19(U_92,U_91,U_90)) = sdtasdt0(U_90,U_92)
& aElementOf0(sK19(U_92,U_91,U_90),xJ)
& aElementOf0(sK18(U_92,U_91,U_90),xI)
& aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ))
& sdtpldt0(sK16(U_92,U_91,U_90),sK17(U_92,U_91,U_90)) = sdtpldt0(U_92,U_91)
& aElementOf0(sK17(U_92,U_91,U_90),xJ)
& aElementOf0(sK16(U_92,U_91,U_90),xI)
& aElementOf0(sdtasdt0(U_90,sK15(U_92,U_91,U_90)),xJ)
& aElementOf0(sdtasdt0(U_90,sK14(U_92,U_91,U_90)),xI)
& U_92 = sdtpldt0(sK14(U_92,U_91,U_90),sK15(U_92,U_91,U_90))
& aElementOf0(sK15(U_92,U_91,U_90),xJ)
& aElementOf0(sK14(U_92,U_91,U_90),xI) )
| ~ aElement0(U_90)
| ( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
& ! [U_81] :
( ! [U_80] :
( sdtpldt0(U_81,U_80) != U_91
| ~ aElementOf0(U_80,xJ) )
| ~ aElementOf0(U_81,xI) ) )
| ( ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
& ! [U_79] :
( ! [U_78] :
( sdtpldt0(U_79,U_78) != U_92
| ~ aElementOf0(U_78,xJ) )
| ~ aElementOf0(U_79,xI) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_99,sK26)],[f_26_16]) ).
cnf(f_26_53,negated_conjecture,
( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
| ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
| ~ aElement0(U_90)
| aElementOf0(sdtpldt0(U_92,U_91),sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_69,negated_conjecture,
( ~ aElementOf0(U_91,sdtpldt1(xI,xJ))
| ~ aElementOf0(U_92,sdtpldt1(xI,xJ))
| ~ aElement0(U_90)
| aElementOf0(sdtasdt0(U_90,U_92),sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_99,negated_conjecture,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_100,negated_conjecture,
( aElement0(sK26)
| aElementOf0(sK25,sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_101,negated_conjecture,
( ~ aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
| aElementOf0(sK25,sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_102,negated_conjecture,
( aElement0(sK26)
| ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(f_26_103,negated_conjecture,
( ~ aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
| ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)) ),
inference(clausify,[status(thm)],[f_26_17]) ).
cnf(t1,plain,
( ~ aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
| ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)) ),
inference(start,[status(thm),parent(0:0)],[f_26_103]) ).
cnf(t2,plain,
( ~ aElement0(sK26)
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| ~ aElementOf0(sK25,sdtpldt1(xI,xJ))
| aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t1:1)],[f_26_53]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
| aElementOf0(sK25,sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t2:2)],[f_26_101]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ aElement0(sK26)
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t4:2)],[f_26_69]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(extension,[status(thm),parent(t6:2)],[f_26_99]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(l4,lemma,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(lemma,[status(cth),parent(t6:2),below(t4:2)],[t6:2]) ).
cnf(t10,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(lemma_extension,[status(thm),parent(t6:3)],[l4:1]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t6:3]) ).
cnf(t12,plain,
( aElementOf0(sK25,sdtpldt1(xI,xJ))
| aElement0(sK26) ),
inference(extension,[status(thm),parent(t6:4)],[f_26_100]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t6:4]) ).
cnf(t14,plain,
$false,
inference(reduction,[status(thm),parent(t12:2)],[t12:2,t2:2]) ).
cnf(t15,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(extension,[status(thm),parent(t2:3)],[f_26_99]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t2:3]) ).
cnf(l7,lemma,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(lemma,[status(cth),parent(t2:3),below(t1:1)],[t2:3]) ).
cnf(t17,plain,
( aElementOf0(sK25,sdtpldt1(xI,xJ))
| aElement0(sK26) ),
inference(extension,[status(thm),parent(t2:4)],[f_26_100]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t2:4]) ).
cnf(t19,plain,
( ~ aElement0(sz10)
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ))
| ~ aElementOf0(sK25,sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t17:2)],[f_26_53]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t17:2]) ).
cnf(t21,plain,
$false,
inference(reduction,[status(thm),parent(t19:2)],[t19:2,t1:1]) ).
cnf(t22,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(lemma_extension,[status(thm),parent(t19:3)],[l7:1]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t19:3]) ).
cnf(t24,plain,
aElement0(sz10),
inference(extension,[status(thm),parent(t19:4)],[f_3_2]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t19:4]) ).
cnf(l1,lemma,
aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)),
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t26,plain,
( ~ aElement0(sK26)
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| ~ aElementOf0(sK25,sdtpldt1(xI,xJ))
| aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t1:2)],[f_26_69]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t1:2]) ).
cnf(t28,plain,
( aElement0(sK26)
| aElementOf0(sK25,sdtpldt1(xI,xJ)) ),
inference(extension,[status(thm),parent(t26:2)],[f_26_100]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
( ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| ~ aElementOf0(sK24,sdtpldt1(xI,xJ))
| aElementOf0(sdtasdt0(sK26,sK24),sdtpldt1(xI,xJ))
| ~ aElement0(sK26) ),
inference(extension,[status(thm),parent(t28:2)],[f_26_69]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
$false,
inference(reduction,[status(thm),parent(t30:2)],[t30:2,t1:2]) ).
cnf(t33,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(extension,[status(thm),parent(t30:3)],[f_26_99]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t30:3]) ).
cnf(t35,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(extension,[status(thm),parent(t30:4)],[f_26_99]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t30:4]) ).
cnf(t37,plain,
aElementOf0(sK24,sdtpldt1(xI,xJ)),
inference(extension,[status(thm),parent(t26:3)],[f_26_99]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t26:3]) ).
cnf(t39,plain,
( ~ aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ))
| aElement0(sK26) ),
inference(extension,[status(thm),parent(t26:4)],[f_26_102]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t26:4]) ).
cnf(t41,plain,
aElementOf0(sdtpldt0(sK24,sK25),sdtpldt1(xI,xJ)),
inference(lemma_extension,[status(thm),parent(t39:2)],[l1:1]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG092+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n007.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 19 20:48:49 UTC 2026
% 0.09/0.38 % CPUTime :
% 88.33/88.64 % SZS status Theorem for theBenchmark
% 88.33/88.64 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------