%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : RNG108+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 20:35:59 EDT 2022
% Result : Theorem 6.94s 7.13s
% Output : CNFRefutation 6.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of formulae : 121 ( 40 unt; 0 def)
% Number of atoms : 368 ( 130 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 399 ( 152 ~; 118 |; 103 &)
% ( 13 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 118 ( 0 sgn 68 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsC,axiom,
aElement0(sz00) ).
fof(mSortsC_01,axiom,
aElement0(sz10) ).
fof(mMulUnit,axiom,
! [W0] :
( aElement0(W0)
=> ( sdtasdt0(W0,sz10) = W0
& W0 = sdtasdt0(sz10,W0) ) ) ).
fof(mMulZero,axiom,
! [W0] :
( aElement0(W0)
=> ( sdtasdt0(W0,sz00) = sz00
& sz00 = sdtasdt0(sz00,W0) ) ) ).
fof(m__2091,hypothesis,
( aElement0(xa)
& aElement0(xb) ) ).
fof(m__2174,hypothesis,
( aSet0(xI)
& ! [W0] :
( aElementOf0(W0,xI)
=> ( ! [W1] :
( aElementOf0(W1,xI)
=> aElementOf0(sdtpldt0(W0,W1),xI) )
& ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xI) ) ) )
& aIdeal0(xI)
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( aElement0(W1)
& sdtasdt0(xa,W1) = W0 ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( aElement0(W1)
& sdtasdt0(xb,W1) = W0 ) )
& ! [W0] :
( aElementOf0(W0,xI)
<=> ? [W1,W2] :
( aElementOf0(W1,slsdtgt0(xa))
& aElementOf0(W2,slsdtgt0(xb))
& sdtpldt0(W1,W2) = W0 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ).
fof(m__,conjecture,
( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa )
| aElementOf0(xa,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xb)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = xb )
| aElementOf0(xb,slsdtgt0(xb)) ) ) ).
fof(subgoal_0,plain,
( ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
=> aElementOf0(sz00,slsdtgt0(xa)) ),
inference(strip,[],[m__]) ).
fof(subgoal_1,plain,
( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa ) )
=> aElementOf0(xa,slsdtgt0(xa)) ),
inference(strip,[],[m__]) ).
fof(subgoal_2,plain,
( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa )
| aElementOf0(xa,slsdtgt0(xa)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = sz00 ) )
=> aElementOf0(sz00,slsdtgt0(xb)) ),
inference(strip,[],[m__]) ).
fof(subgoal_3,plain,
( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa )
| aElementOf0(xa,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xb)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = xb ) )
=> aElementOf0(xb,slsdtgt0(xb)) ),
inference(strip,[],[m__]) ).
fof(negate_0_0,plain,
~ ( ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
=> aElementOf0(sz00,slsdtgt0(xa)) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
aElement0(sz00),
inference(canonicalize,[],[mSortsC]) ).
fof(normalize_0_1,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& aIdeal0(xI)
& aSet0(xI)
& ! [W0] :
( ~ aElementOf0(W0,xI)
| ( ! [W1] :
( ~ aElement0(W1)
| aElementOf0(sdtasdt0(W1,W0),xI) )
& ! [W1] :
( ~ aElementOf0(W1,xI)
| aElementOf0(sdtpldt0(W0,W1),xI) ) ) )
& ! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xa))
<=> ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) ) )
& ! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xb))
<=> ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) ) )
& ! [W0] :
( ~ aElementOf0(W0,xI)
<=> ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W1,slsdtgt0(xa))
| ~ aElementOf0(W2,slsdtgt0(xb)) ) ) ),
inference(canonicalize,[],[m__2174]) ).
fof(normalize_0_2,plain,
! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xa))
<=> ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) ) ),
inference(conjunct,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xa))
<=> ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) ) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [W0,W1] :
( ( ~ aElementOf0(W0,slsdtgt0(xa))
| sdtasdt0(xa,skolemFOFtoCNF_W1_2(W0)) = W0 )
& ( ~ aElementOf0(W0,slsdtgt0(xa))
| aElement0(skolemFOFtoCNF_W1_2(W0)) )
& ( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xa)) ) ),
inference(clausify,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [W0,W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xa)) ),
inference(conjunct,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
( aElement0(xa)
& aElement0(xb) ),
inference(canonicalize,[],[m__2091]) ).
fof(normalize_0_7,plain,
aElement0(xa),
inference(conjunct,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [W0] :
( ~ aElement0(W0)
| ( sdtasdt0(W0,sz00) = sz00
& sz00 = sdtasdt0(sz00,W0) ) ),
inference(canonicalize,[],[mMulZero]) ).
fof(normalize_0_9,plain,
! [W0] :
( ~ aElement0(W0)
| ( sdtasdt0(W0,sz00) = sz00
& sz00 = sdtasdt0(sz00,W0) ) ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [W0] :
( ( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 )
& ( ~ aElement0(W0)
| sz00 = sdtasdt0(sz00,W0) ) ),
inference(clausify,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [W0] :
( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 ),
inference(conjunct,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
( ~ aElementOf0(sz00,slsdtgt0(xa))
& ! [W0] :
( sdtasdt0(xa,W0) != sz00
| ~ aElement0(W0) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_13,plain,
~ aElementOf0(sz00,slsdtgt0(xa)),
inference(conjunct,[],[normalize_0_12]) ).
cnf(refute_0_0,plain,
aElement0(sz00),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xa)) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_2,plain,
( sdtasdt0(xa,W1) != sdtasdt0(xa,W1)
| ~ aElement0(W1)
| aElementOf0(sdtasdt0(xa,W1),slsdtgt0(xa)) ),
inference(subst,[],[refute_0_1:[bind(W0,$fot(sdtasdt0(xa,W1)))]]) ).
cnf(refute_0_3,plain,
sdtasdt0(xa,W1) = sdtasdt0(xa,W1),
introduced(tautology,[refl,[$fot(sdtasdt0(xa,W1))]]) ).
cnf(refute_0_4,plain,
( ~ aElement0(W1)
| aElementOf0(sdtasdt0(xa,W1),slsdtgt0(xa)) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xa,W1),sdtasdt0(xa,W1)) )],[refute_0_3,refute_0_2]) ).
cnf(refute_0_5,plain,
( ~ aElement0(sz00)
| aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa)) ),
inference(subst,[],[refute_0_4:[bind(W1,$fot(sz00))]]) ).
cnf(refute_0_6,plain,
aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa)),
inference(resolve,[$cnf( aElement0(sz00) )],[refute_0_0,refute_0_5]) ).
cnf(refute_0_7,plain,
aElement0(xa),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_8,plain,
( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 ),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_9,plain,
( ~ aElement0(xa)
| sdtasdt0(xa,sz00) = sz00 ),
inference(subst,[],[refute_0_8:[bind(W0,$fot(xa))]]) ).
cnf(refute_0_10,plain,
sdtasdt0(xa,sz00) = sz00,
inference(resolve,[$cnf( aElement0(xa) )],[refute_0_7,refute_0_9]) ).
cnf(refute_0_11,plain,
( sdtasdt0(xa,sz00) != sz00
| ~ aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa))
| aElementOf0(sz00,slsdtgt0(xa)) ),
introduced(tautology,[equality,[$cnf( aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa)) ),[0],$fot(sz00)]]) ).
cnf(refute_0_12,plain,
( ~ aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa))
| aElementOf0(sz00,slsdtgt0(xa)) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xa,sz00),sz00) )],[refute_0_10,refute_0_11]) ).
cnf(refute_0_13,plain,
aElementOf0(sz00,slsdtgt0(xa)),
inference(resolve,[$cnf( aElementOf0(sdtasdt0(xa,sz00),slsdtgt0(xa)) )],[refute_0_6,refute_0_12]) ).
cnf(refute_0_14,plain,
~ aElementOf0(sz00,slsdtgt0(xa)),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_15,plain,
$false,
inference(resolve,[$cnf( aElementOf0(sz00,slsdtgt0(xa)) )],[refute_0_13,refute_0_14]) ).
fof(negate_1_0,plain,
~ ( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa ) )
=> aElementOf0(xa,slsdtgt0(xa)) ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
( ~ aElementOf0(xa,slsdtgt0(xa))
& ( aElementOf0(sz00,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) )
& ! [W0] :
( sdtasdt0(xa,W0) != xa
| ~ aElement0(W0) ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
! [W0] :
( sdtasdt0(xa,W0) != xa
| ~ aElement0(W0) ),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
! [W0] :
( sdtasdt0(xa,W0) != xa
| ~ aElement0(W0) ),
inference(specialize,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
( aElement0(xa)
& aElement0(xb) ),
inference(canonicalize,[],[m__2091]) ).
fof(normalize_1_4,plain,
aElement0(xa),
inference(conjunct,[],[normalize_1_3]) ).
fof(normalize_1_5,plain,
! [W0] :
( ~ aElement0(W0)
| ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
inference(canonicalize,[],[mMulUnit]) ).
fof(normalize_1_6,plain,
! [W0] :
( ~ aElement0(W0)
| ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
inference(specialize,[],[normalize_1_5]) ).
fof(normalize_1_7,plain,
! [W0] :
( ( ~ aElement0(W0)
| W0 = sdtasdt0(sz10,W0) )
& ( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ) ),
inference(clausify,[],[normalize_1_6]) ).
fof(normalize_1_8,plain,
! [W0] :
( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ),
inference(conjunct,[],[normalize_1_7]) ).
fof(normalize_1_9,plain,
aElement0(sz10),
inference(canonicalize,[],[mSortsC_01]) ).
cnf(refute_1_0,plain,
( sdtasdt0(xa,W0) != xa
| ~ aElement0(W0) ),
inference(canonicalize,[],[normalize_1_2]) ).
cnf(refute_1_1,plain,
( sdtasdt0(xa,sz10) != xa
| ~ aElement0(sz10) ),
inference(subst,[],[refute_1_0:[bind(W0,$fot(sz10))]]) ).
cnf(refute_1_2,plain,
aElement0(xa),
inference(canonicalize,[],[normalize_1_4]) ).
cnf(refute_1_3,plain,
( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ),
inference(canonicalize,[],[normalize_1_8]) ).
cnf(refute_1_4,plain,
( ~ aElement0(xa)
| sdtasdt0(xa,sz10) = xa ),
inference(subst,[],[refute_1_3:[bind(W0,$fot(xa))]]) ).
cnf(refute_1_5,plain,
sdtasdt0(xa,sz10) = xa,
inference(resolve,[$cnf( aElement0(xa) )],[refute_1_2,refute_1_4]) ).
cnf(refute_1_6,plain,
( sdtasdt0(xa,sz10) != xa
| xa != xa
| sdtasdt0(xa,sz10) = xa ),
introduced(tautology,[equality,[$cnf( ~ $equal(sdtasdt0(xa,sz10),xa) ),[0],$fot(xa)]]) ).
cnf(refute_1_7,plain,
( xa != xa
| sdtasdt0(xa,sz10) = xa ),
inference(resolve,[$cnf( $equal(sdtasdt0(xa,sz10),xa) )],[refute_1_5,refute_1_6]) ).
cnf(refute_1_8,plain,
( xa != xa
| ~ aElement0(sz10) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xa,sz10),xa) )],[refute_1_7,refute_1_1]) ).
cnf(refute_1_9,plain,
xa = xa,
introduced(tautology,[refl,[$fot(xa)]]) ).
cnf(refute_1_10,plain,
~ aElement0(sz10),
inference(resolve,[$cnf( $equal(xa,xa) )],[refute_1_9,refute_1_8]) ).
cnf(refute_1_11,plain,
aElement0(sz10),
inference(canonicalize,[],[normalize_1_9]) ).
cnf(refute_1_12,plain,
$false,
inference(resolve,[$cnf( aElement0(sz10) )],[refute_1_11,refute_1_10]) ).
fof(negate_2_0,plain,
~ ( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa )
| aElementOf0(xa,slsdtgt0(xa)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = sz00 ) )
=> aElementOf0(sz00,slsdtgt0(xb)) ),
inference(negate,[],[subgoal_2]) ).
fof(normalize_2_0,plain,
( ~ aElementOf0(sz00,slsdtgt0(xb))
& ( aElementOf0(sz00,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) )
& ( aElementOf0(xa,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) ) )
& ! [W0] :
( sdtasdt0(xb,W0) != sz00
| ~ aElement0(W0) ) ),
inference(canonicalize,[],[negate_2_0]) ).
fof(normalize_2_1,plain,
! [W0] :
( sdtasdt0(xb,W0) != sz00
| ~ aElement0(W0) ),
inference(conjunct,[],[normalize_2_0]) ).
fof(normalize_2_2,plain,
! [W0] :
( sdtasdt0(xb,W0) != sz00
| ~ aElement0(W0) ),
inference(specialize,[],[normalize_2_1]) ).
fof(normalize_2_3,plain,
( aElement0(xa)
& aElement0(xb) ),
inference(canonicalize,[],[m__2091]) ).
fof(normalize_2_4,plain,
aElement0(xb),
inference(conjunct,[],[normalize_2_3]) ).
fof(normalize_2_5,plain,
! [W0] :
( ~ aElement0(W0)
| ( sdtasdt0(W0,sz00) = sz00
& sz00 = sdtasdt0(sz00,W0) ) ),
inference(canonicalize,[],[mMulZero]) ).
fof(normalize_2_6,plain,
! [W0] :
( ~ aElement0(W0)
| ( sdtasdt0(W0,sz00) = sz00
& sz00 = sdtasdt0(sz00,W0) ) ),
inference(specialize,[],[normalize_2_5]) ).
fof(normalize_2_7,plain,
! [W0] :
( ( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 )
& ( ~ aElement0(W0)
| sz00 = sdtasdt0(sz00,W0) ) ),
inference(clausify,[],[normalize_2_6]) ).
fof(normalize_2_8,plain,
! [W0] :
( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 ),
inference(conjunct,[],[normalize_2_7]) ).
fof(normalize_2_9,plain,
aElement0(sz00),
inference(canonicalize,[],[mSortsC]) ).
cnf(refute_2_0,plain,
( sdtasdt0(xb,W0) != sz00
| ~ aElement0(W0) ),
inference(canonicalize,[],[normalize_2_2]) ).
cnf(refute_2_1,plain,
( sdtasdt0(xb,sz00) != sz00
| ~ aElement0(sz00) ),
inference(subst,[],[refute_2_0:[bind(W0,$fot(sz00))]]) ).
cnf(refute_2_2,plain,
aElement0(xb),
inference(canonicalize,[],[normalize_2_4]) ).
cnf(refute_2_3,plain,
( ~ aElement0(W0)
| sdtasdt0(W0,sz00) = sz00 ),
inference(canonicalize,[],[normalize_2_8]) ).
cnf(refute_2_4,plain,
( ~ aElement0(xb)
| sdtasdt0(xb,sz00) = sz00 ),
inference(subst,[],[refute_2_3:[bind(W0,$fot(xb))]]) ).
cnf(refute_2_5,plain,
sdtasdt0(xb,sz00) = sz00,
inference(resolve,[$cnf( aElement0(xb) )],[refute_2_2,refute_2_4]) ).
cnf(refute_2_6,plain,
( sdtasdt0(xb,sz00) != sz00
| sz00 != sz00
| sdtasdt0(xb,sz00) = sz00 ),
introduced(tautology,[equality,[$cnf( ~ $equal(sdtasdt0(xb,sz00),sz00) ),[0],$fot(sz00)]]) ).
cnf(refute_2_7,plain,
( sz00 != sz00
| sdtasdt0(xb,sz00) = sz00 ),
inference(resolve,[$cnf( $equal(sdtasdt0(xb,sz00),sz00) )],[refute_2_5,refute_2_6]) ).
cnf(refute_2_8,plain,
( sz00 != sz00
| ~ aElement0(sz00) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xb,sz00),sz00) )],[refute_2_7,refute_2_1]) ).
cnf(refute_2_9,plain,
sz00 = sz00,
introduced(tautology,[refl,[$fot(sz00)]]) ).
cnf(refute_2_10,plain,
~ aElement0(sz00),
inference(resolve,[$cnf( $equal(sz00,sz00) )],[refute_2_9,refute_2_8]) ).
cnf(refute_2_11,plain,
aElement0(sz00),
inference(canonicalize,[],[normalize_2_9]) ).
cnf(refute_2_12,plain,
$false,
inference(resolve,[$cnf( aElement0(sz00) )],[refute_2_11,refute_2_10]) ).
fof(negate_3_0,plain,
~ ( ( ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xa,W0) = xa )
| aElementOf0(xa,slsdtgt0(xa)) )
& ( ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = sz00 )
| aElementOf0(sz00,slsdtgt0(xb)) )
& ~ ? [W0] :
( aElement0(W0)
& sdtasdt0(xb,W0) = xb ) )
=> aElementOf0(xb,slsdtgt0(xb)) ),
inference(negate,[],[subgoal_3]) ).
fof(normalize_3_0,plain,
aElement0(sz10),
inference(canonicalize,[],[mSortsC_01]) ).
fof(normalize_3_1,plain,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& aIdeal0(xI)
& aSet0(xI)
& ! [W0] :
( ~ aElementOf0(W0,xI)
| ( ! [W1] :
( ~ aElement0(W1)
| aElementOf0(sdtasdt0(W1,W0),xI) )
& ! [W1] :
( ~ aElementOf0(W1,xI)
| aElementOf0(sdtpldt0(W0,W1),xI) ) ) )
& ! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xa))
<=> ! [W1] :
( sdtasdt0(xa,W1) != W0
| ~ aElement0(W1) ) )
& ! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xb))
<=> ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) ) )
& ! [W0] :
( ~ aElementOf0(W0,xI)
<=> ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W1,slsdtgt0(xa))
| ~ aElementOf0(W2,slsdtgt0(xb)) ) ) ),
inference(canonicalize,[],[m__2174]) ).
fof(normalize_3_2,plain,
! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xb))
<=> ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) ) ),
inference(conjunct,[],[normalize_3_1]) ).
fof(normalize_3_3,plain,
! [W0] :
( ~ aElementOf0(W0,slsdtgt0(xb))
<=> ! [W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1) ) ),
inference(specialize,[],[normalize_3_2]) ).
fof(normalize_3_4,plain,
! [W0,W1] :
( ( ~ aElementOf0(W0,slsdtgt0(xb))
| sdtasdt0(xb,skolemFOFtoCNF_W1_3(W0)) = W0 )
& ( ~ aElementOf0(W0,slsdtgt0(xb))
| aElement0(skolemFOFtoCNF_W1_3(W0)) )
& ( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xb)) ) ),
inference(clausify,[],[normalize_3_3]) ).
fof(normalize_3_5,plain,
! [W0,W1] :
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xb)) ),
inference(conjunct,[],[normalize_3_4]) ).
fof(normalize_3_6,plain,
( aElement0(xa)
& aElement0(xb) ),
inference(canonicalize,[],[m__2091]) ).
fof(normalize_3_7,plain,
aElement0(xb),
inference(conjunct,[],[normalize_3_6]) ).
fof(normalize_3_8,plain,
! [W0] :
( ~ aElement0(W0)
| ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
inference(canonicalize,[],[mMulUnit]) ).
fof(normalize_3_9,plain,
! [W0] :
( ~ aElement0(W0)
| ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
inference(specialize,[],[normalize_3_8]) ).
fof(normalize_3_10,plain,
! [W0] :
( ( ~ aElement0(W0)
| W0 = sdtasdt0(sz10,W0) )
& ( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ) ),
inference(clausify,[],[normalize_3_9]) ).
fof(normalize_3_11,plain,
! [W0] :
( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ),
inference(conjunct,[],[normalize_3_10]) ).
fof(normalize_3_12,plain,
( ~ aElementOf0(xb,slsdtgt0(xb))
& ( aElementOf0(sz00,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) )
& ( aElementOf0(sz00,slsdtgt0(xb))
| ? [W0] :
( sdtasdt0(xb,W0) = sz00
& aElement0(W0) ) )
& ( aElementOf0(xa,slsdtgt0(xa))
| ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) ) )
& ! [W0] :
( sdtasdt0(xb,W0) != xb
| ~ aElement0(W0) ) ),
inference(canonicalize,[],[negate_3_0]) ).
fof(normalize_3_13,plain,
~ aElementOf0(xb,slsdtgt0(xb)),
inference(conjunct,[],[normalize_3_12]) ).
cnf(refute_3_0,plain,
aElement0(sz10),
inference(canonicalize,[],[normalize_3_0]) ).
cnf(refute_3_1,plain,
( sdtasdt0(xb,W1) != W0
| ~ aElement0(W1)
| aElementOf0(W0,slsdtgt0(xb)) ),
inference(canonicalize,[],[normalize_3_5]) ).
cnf(refute_3_2,plain,
( sdtasdt0(xb,W1) != sdtasdt0(xb,W1)
| ~ aElement0(W1)
| aElementOf0(sdtasdt0(xb,W1),slsdtgt0(xb)) ),
inference(subst,[],[refute_3_1:[bind(W0,$fot(sdtasdt0(xb,W1)))]]) ).
cnf(refute_3_3,plain,
sdtasdt0(xb,W1) = sdtasdt0(xb,W1),
introduced(tautology,[refl,[$fot(sdtasdt0(xb,W1))]]) ).
cnf(refute_3_4,plain,
( ~ aElement0(W1)
| aElementOf0(sdtasdt0(xb,W1),slsdtgt0(xb)) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xb,W1),sdtasdt0(xb,W1)) )],[refute_3_3,refute_3_2]) ).
cnf(refute_3_5,plain,
( ~ aElement0(sz10)
| aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb)) ),
inference(subst,[],[refute_3_4:[bind(W1,$fot(sz10))]]) ).
cnf(refute_3_6,plain,
aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb)),
inference(resolve,[$cnf( aElement0(sz10) )],[refute_3_0,refute_3_5]) ).
cnf(refute_3_7,plain,
aElement0(xb),
inference(canonicalize,[],[normalize_3_7]) ).
cnf(refute_3_8,plain,
( ~ aElement0(W0)
| sdtasdt0(W0,sz10) = W0 ),
inference(canonicalize,[],[normalize_3_11]) ).
cnf(refute_3_9,plain,
( ~ aElement0(xb)
| sdtasdt0(xb,sz10) = xb ),
inference(subst,[],[refute_3_8:[bind(W0,$fot(xb))]]) ).
cnf(refute_3_10,plain,
sdtasdt0(xb,sz10) = xb,
inference(resolve,[$cnf( aElement0(xb) )],[refute_3_7,refute_3_9]) ).
cnf(refute_3_11,plain,
( sdtasdt0(xb,sz10) != xb
| ~ aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb))
| aElementOf0(xb,slsdtgt0(xb)) ),
introduced(tautology,[equality,[$cnf( aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb)) ),[0],$fot(xb)]]) ).
cnf(refute_3_12,plain,
( ~ aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb))
| aElementOf0(xb,slsdtgt0(xb)) ),
inference(resolve,[$cnf( $equal(sdtasdt0(xb,sz10),xb) )],[refute_3_10,refute_3_11]) ).
cnf(refute_3_13,plain,
aElementOf0(xb,slsdtgt0(xb)),
inference(resolve,[$cnf( aElementOf0(sdtasdt0(xb,sz10),slsdtgt0(xb)) )],[refute_3_6,refute_3_12]) ).
cnf(refute_3_14,plain,
~ aElementOf0(xb,slsdtgt0(xb)),
inference(canonicalize,[],[normalize_3_13]) ).
cnf(refute_3_15,plain,
$false,
inference(resolve,[$cnf( aElementOf0(xb,slsdtgt0(xb)) )],[refute_3_13,refute_3_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : RNG108+4 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon May 30 07:50:49 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 6.94/7.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.94/7.13
% 6.94/7.13 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 6.94/7.14
%------------------------------------------------------------------------------