%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM440+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 : Tue Sep 29 12:24:19 PM UTC 2026
% Result : Theorem 0.19s 0.50s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 26
% Syntax : Number of formulae : 251 ( 13 unt; 24 def)
% Number of atoms : 1152 ( 29 equ)
% Maximal formula atoms : 64 ( 4 avg)
% Number of connectives : 1288 ( 387 ~; 484 |; 282 &)
% ( 83 <=>; 50 =>; 0 <=; 2 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 26 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 228 ( 0 sgn 202 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) )
& aSet0(xA)
& ! [X0] :
( aElementOf0(X0,xA)
=> aElementOf0(X0,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) )
& aSet0(xB)
& ! [X0] :
( aElementOf0(X0,xB)
=> aElementOf0(X0,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) )
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) ) )
& ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X0] :
( aElementOf0(X0,stldt0(xB))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xB) ) )
& ! [X0] :
( aElementOf0(X0,stldt0(xB))
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) ) )
& ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1826) ).
fof(f40,conjecture,
( ( ( aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) ) )
=> ( ( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xA))
=> aElementOf0(X0,cS1395) )
| aSubsetOf0(stldt0(xA),cS1395) ) ) )
& ( ( aSet0(stldt0(xB))
& ! [X0] :
( aElementOf0(X0,stldt0(xB))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xB) ) ) )
=> ( ( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xB))
=> aElementOf0(X0,cS1395) )
| aSubsetOf0(stldt0(xB),cS1395) ) ) )
& ( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X0] :
( aElementOf0(X0,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X0)
& ( aElementOf0(X0,xA)
| aElementOf0(X0,xB) ) ) ) )
=> ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X0] :
( aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xB))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xB) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X0)
& aElementOf0(X0,stldt0(xA))
& aElementOf0(X0,stldt0(xB)) ) )
| stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f41,negated_conjecture,
~ ( ( ( aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) ) )
=> ( ( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xA))
=> aElementOf0(X0,cS1395) )
| aSubsetOf0(stldt0(xA),cS1395) ) ) )
& ( ( aSet0(stldt0(xB))
& ! [X0] :
( aElementOf0(X0,stldt0(xB))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xB) ) ) )
=> ( ( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xB))
=> aElementOf0(X0,cS1395) )
| aSubsetOf0(stldt0(xB),cS1395) ) ) )
& ( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X0] :
( aElementOf0(X0,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X0)
& ( aElementOf0(X0,xA)
| aElementOf0(X0,xB) ) ) ) )
=> ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X0] :
( aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(xB))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xB) ) )
=> ( ! [X0] :
( aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X0)
& aElementOf0(X0,stldt0(xA))
& aElementOf0(X0,stldt0(xB)) ) )
| stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f43,plain,
( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) )
& aSet0(xA)
& ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X2] :
( aElementOf0(X2,cS1395)
<=> aInteger0(X2) )
& aSet0(xB)
& ! [X3] :
( aElementOf0(X3,xB)
=> aElementOf0(X3,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X4] :
( aElementOf0(X4,stldt0(xA))
<=> ( aInteger0(X4)
& ~ aElementOf0(X4,xA) ) )
& ! [X5] :
( aElementOf0(X5,stldt0(xA))
=> ? [X6] :
( aInteger0(X6)
& sz00 != X6
& aSet0(szAzrzSzezqlpdtcmdtrp0(X5,X6))
& ! [X7] :
( ( aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6))
=> ( aInteger0(X7)
& ? [X8] :
( aInteger0(X8)
& sdtasdt0(X6,X8) = sdtpldt0(X7,smndt0(X5)) )
& aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
& sdteqdtlpzmzozddtrp0(X7,X5,X6) ) )
& ( ( aInteger0(X7)
& ( ? [X9] :
( aInteger0(X9)
& sdtpldt0(X7,smndt0(X5)) = sdtasdt0(X6,X9) )
| aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
| sdteqdtlpzmzozddtrp0(X7,X5,X6) ) )
=> aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6)) ) )
& ! [X10] :
( aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(X5,X6))
=> aElementOf0(X10,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X5,X6),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X11] :
( aElementOf0(X11,stldt0(xB))
<=> ( aInteger0(X11)
& ~ aElementOf0(X11,xB) ) )
& ! [X12] :
( aElementOf0(X12,stldt0(xB))
=> ? [X13] :
( aInteger0(X13)
& sz00 != X13
& aSet0(szAzrzSzezqlpdtcmdtrp0(X12,X13))
& ! [X14] :
( ( aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13))
=> ( aInteger0(X14)
& ? [X15] :
( aInteger0(X15)
& sdtasdt0(X13,X15) = sdtpldt0(X14,smndt0(X12)) )
& aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
& sdteqdtlpzmzozddtrp0(X14,X12,X13) ) )
& ( ( aInteger0(X14)
& ( ? [X16] :
( aInteger0(X16)
& sdtpldt0(X14,smndt0(X12)) = sdtasdt0(X13,X16) )
| aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
| sdteqdtlpzmzozddtrp0(X14,X12,X13) ) )
=> aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13)) ) )
& ! [X17] :
( aElementOf0(X17,szAzrzSzezqlpdtcmdtrp0(X12,X13))
=> aElementOf0(X17,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X12,X13),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(rectify,[],[f39]) ).
fof(f44,plain,
~ ( ( ( aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) ) )
=> ( ( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) ) )
=> ( ! [X2] :
( aElementOf0(X2,stldt0(xA))
=> aElementOf0(X2,cS1395) )
| aSubsetOf0(stldt0(xA),cS1395) ) ) )
& ( ( aSet0(stldt0(xB))
& ! [X3] :
( aElementOf0(X3,stldt0(xB))
<=> ( aInteger0(X3)
& ~ aElementOf0(X3,xB) ) ) )
=> ( ( aSet0(cS1395)
& ! [X4] :
( aElementOf0(X4,cS1395)
<=> aInteger0(X4) ) )
=> ( ! [X5] :
( aElementOf0(X5,stldt0(xB))
=> aElementOf0(X5,cS1395) )
| aSubsetOf0(stldt0(xB),cS1395) ) ) )
& ( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X6] :
( aElementOf0(X6,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X6)
& ( aElementOf0(X6,xA)
| aElementOf0(X6,xB) ) ) ) )
=> ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X7] :
( aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X7)
& ~ aElementOf0(X7,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X8] :
( aElementOf0(X8,stldt0(xA))
<=> ( aInteger0(X8)
& ~ aElementOf0(X8,xA) ) )
=> ( ! [X9] :
( aElementOf0(X9,stldt0(xB))
<=> ( aInteger0(X9)
& ~ aElementOf0(X9,xB) ) )
=> ( ! [X10] :
( aElementOf0(X10,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X10)
& aElementOf0(X10,stldt0(xA))
& aElementOf0(X10,stldt0(xB)) ) )
| stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)) ) ) ) ) ) ),
inference(rectify,[],[f41]) ).
fof(f101,plain,
( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) )
& aSet0(xA)
& ! [X1] :
( aElementOf0(X1,cS1395)
| ~ aElementOf0(X1,xA) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X2] :
( aElementOf0(X2,cS1395)
<=> aInteger0(X2) )
& aSet0(xB)
& ! [X3] :
( aElementOf0(X3,cS1395)
| ~ aElementOf0(X3,xB) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X4] :
( aElementOf0(X4,stldt0(xA))
<=> ( aInteger0(X4)
& ~ aElementOf0(X4,xA) ) )
& ! [X5] :
( ? [X6] :
( aInteger0(X6)
& sz00 != X6
& aSet0(szAzrzSzezqlpdtcmdtrp0(X5,X6))
& ! [X7] :
( ( ( aInteger0(X7)
& ? [X8] :
( aInteger0(X8)
& sdtasdt0(X6,X8) = sdtpldt0(X7,smndt0(X5)) )
& aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
& sdteqdtlpzmzozddtrp0(X7,X5,X6) )
| ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6)) )
& ( aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6))
| ~ aInteger0(X7)
| ( ! [X9] :
( ~ aInteger0(X9)
| sdtpldt0(X7,smndt0(X5)) != sdtasdt0(X6,X9) )
& ~ aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
& ~ sdteqdtlpzmzozddtrp0(X7,X5,X6) ) ) )
& ! [X10] :
( aElementOf0(X10,stldt0(xA))
| ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(X5,X6)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X5,X6),stldt0(xA)) )
| ~ aElementOf0(X5,stldt0(xA)) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X11] :
( aElementOf0(X11,stldt0(xB))
<=> ( aInteger0(X11)
& ~ aElementOf0(X11,xB) ) )
& ! [X12] :
( ? [X13] :
( aInteger0(X13)
& sz00 != X13
& aSet0(szAzrzSzezqlpdtcmdtrp0(X12,X13))
& ! [X14] :
( ( ( aInteger0(X14)
& ? [X15] :
( aInteger0(X15)
& sdtasdt0(X13,X15) = sdtpldt0(X14,smndt0(X12)) )
& aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
& sdteqdtlpzmzozddtrp0(X14,X12,X13) )
| ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13)) )
& ( aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13))
| ~ aInteger0(X14)
| ( ! [X16] :
( ~ aInteger0(X16)
| sdtpldt0(X14,smndt0(X12)) != sdtasdt0(X13,X16) )
& ~ aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
& ~ sdteqdtlpzmzozddtrp0(X14,X12,X13) ) ) )
& ! [X17] :
( aElementOf0(X17,stldt0(xB))
| ~ aElementOf0(X17,szAzrzSzezqlpdtcmdtrp0(X12,X13)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X12,X13),stldt0(xB)) )
| ~ aElementOf0(X12,stldt0(xB)) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(ennf_transformation,[],[f43]) ).
fof(f102,plain,
( aSet0(cS1395)
& ! [X0] :
( aElementOf0(X0,cS1395)
<=> aInteger0(X0) )
& aSet0(xA)
& ! [X1] :
( aElementOf0(X1,cS1395)
| ~ aElementOf0(X1,xA) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X2] :
( aElementOf0(X2,cS1395)
<=> aInteger0(X2) )
& aSet0(xB)
& ! [X3] :
( aElementOf0(X3,cS1395)
| ~ aElementOf0(X3,xB) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X4] :
( aElementOf0(X4,stldt0(xA))
<=> ( aInteger0(X4)
& ~ aElementOf0(X4,xA) ) )
& ! [X5] :
( ? [X6] :
( aInteger0(X6)
& sz00 != X6
& aSet0(szAzrzSzezqlpdtcmdtrp0(X5,X6))
& ! [X7] :
( ( ( aInteger0(X7)
& ? [X8] :
( aInteger0(X8)
& sdtasdt0(X6,X8) = sdtpldt0(X7,smndt0(X5)) )
& aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
& sdteqdtlpzmzozddtrp0(X7,X5,X6) )
| ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6)) )
& ( aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X5,X6))
| ~ aInteger0(X7)
| ( ! [X9] :
( ~ aInteger0(X9)
| sdtpldt0(X7,smndt0(X5)) != sdtasdt0(X6,X9) )
& ~ aDivisorOf0(X6,sdtpldt0(X7,smndt0(X5)))
& ~ sdteqdtlpzmzozddtrp0(X7,X5,X6) ) ) )
& ! [X10] :
( aElementOf0(X10,stldt0(xA))
| ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(X5,X6)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X5,X6),stldt0(xA)) )
| ~ aElementOf0(X5,stldt0(xA)) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X11] :
( aElementOf0(X11,stldt0(xB))
<=> ( aInteger0(X11)
& ~ aElementOf0(X11,xB) ) )
& ! [X12] :
( ? [X13] :
( aInteger0(X13)
& sz00 != X13
& aSet0(szAzrzSzezqlpdtcmdtrp0(X12,X13))
& ! [X14] :
( ( ( aInteger0(X14)
& ? [X15] :
( aInteger0(X15)
& sdtasdt0(X13,X15) = sdtpldt0(X14,smndt0(X12)) )
& aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
& sdteqdtlpzmzozddtrp0(X14,X12,X13) )
| ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13)) )
& ( aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X12,X13))
| ~ aInteger0(X14)
| ( ! [X16] :
( ~ aInteger0(X16)
| sdtpldt0(X14,smndt0(X12)) != sdtasdt0(X13,X16) )
& ~ aDivisorOf0(X13,sdtpldt0(X14,smndt0(X12)))
& ~ sdteqdtlpzmzozddtrp0(X14,X12,X13) ) ) )
& ! [X17] :
( aElementOf0(X17,stldt0(xB))
| ~ aElementOf0(X17,szAzrzSzezqlpdtcmdtrp0(X12,X13)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X12,X13),stldt0(xB)) )
| ~ aElementOf0(X12,stldt0(xB)) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
( ( ? [X2] :
( ~ aElementOf0(X2,cS1395)
& aElementOf0(X2,stldt0(xA)) )
& ~ aSubsetOf0(stldt0(xA),cS1395)
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) ) )
| ( ? [X5] :
( ~ aElementOf0(X5,cS1395)
& aElementOf0(X5,stldt0(xB)) )
& ~ aSubsetOf0(stldt0(xB),cS1395)
& aSet0(cS1395)
& ! [X4] :
( aElementOf0(X4,cS1395)
<=> aInteger0(X4) )
& aSet0(stldt0(xB))
& ! [X3] :
( aElementOf0(X3,stldt0(xB))
<=> ( aInteger0(X3)
& ~ aElementOf0(X3,xB) ) ) )
| ( ? [X10] :
( aElementOf0(X10,stldt0(sdtbsmnsldt0(xA,xB)))
<~> ( aInteger0(X10)
& aElementOf0(X10,stldt0(xA))
& aElementOf0(X10,stldt0(xB)) ) )
& stldt0(sdtbsmnsldt0(xA,xB)) != sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [X9] :
( aElementOf0(X9,stldt0(xB))
<=> ( aInteger0(X9)
& ~ aElementOf0(X9,xB) ) )
& ! [X8] :
( aElementOf0(X8,stldt0(xA))
<=> ( aInteger0(X8)
& ~ aElementOf0(X8,xA) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X7] :
( aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X7)
& ~ aElementOf0(X7,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X6] :
( aElementOf0(X6,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X6)
& ( aElementOf0(X6,xA)
| aElementOf0(X6,xB) ) ) ) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f104,plain,
( ( ? [X2] :
( ~ aElementOf0(X2,cS1395)
& aElementOf0(X2,stldt0(xA)) )
& ~ aSubsetOf0(stldt0(xA),cS1395)
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(stldt0(xA))
& ! [X0] :
( aElementOf0(X0,stldt0(xA))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,xA) ) ) )
| ( ? [X5] :
( ~ aElementOf0(X5,cS1395)
& aElementOf0(X5,stldt0(xB)) )
& ~ aSubsetOf0(stldt0(xB),cS1395)
& aSet0(cS1395)
& ! [X4] :
( aElementOf0(X4,cS1395)
<=> aInteger0(X4) )
& aSet0(stldt0(xB))
& ! [X3] :
( aElementOf0(X3,stldt0(xB))
<=> ( aInteger0(X3)
& ~ aElementOf0(X3,xB) ) ) )
| ( ? [X10] :
( aElementOf0(X10,stldt0(sdtbsmnsldt0(xA,xB)))
<~> ( aInteger0(X10)
& aElementOf0(X10,stldt0(xA))
& aElementOf0(X10,stldt0(xB)) ) )
& stldt0(sdtbsmnsldt0(xA,xB)) != sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [X9] :
( aElementOf0(X9,stldt0(xB))
<=> ( aInteger0(X9)
& ~ aElementOf0(X9,xB) ) )
& ! [X8] :
( aElementOf0(X8,stldt0(xA))
<=> ( aInteger0(X8)
& ~ aElementOf0(X8,xA) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X7] :
( aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X7)
& ~ aElementOf0(X7,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X6] :
( aElementOf0(X6,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X6)
& ( aElementOf0(X6,xA)
| aElementOf0(X6,xB) ) ) ) ) ),
inference(flattening,[],[f103]) ).
fof(f233,plain,
! [X4] :
( ~ aElementOf0(X4,xA)
| ~ aElementOf0(X4,stldt0(xA)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f234,plain,
! [X4] :
( aInteger0(X4)
| ~ aElementOf0(X4,stldt0(xA)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f235,plain,
! [X4] :
( aElementOf0(X4,xA)
| ~ aInteger0(X4)
| aElementOf0(X4,stldt0(xA)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f239,plain,
! [X0] :
( ~ aInteger0(X0)
| aElementOf0(X0,cS1395) ),
inference(cnf_transformation,[],[f102]) ).
fof(f257,plain,
! [X6] :
( ~ sP25(X6)
| aElementOf0(X6,xA)
| aElementOf0(X6,xB) ),
inference(cnf_transformation,[],[f104]) ).
fof(f258,plain,
! [X6] :
( ~ aElementOf0(X6,xB)
| ~ aInteger0(X6)
| sP25(X6) ),
inference(cnf_transformation,[],[f104]) ).
fof(f259,plain,
! [X6] :
( ~ aElementOf0(X6,xA)
| ~ aInteger0(X6)
| sP25(X6) ),
inference(cnf_transformation,[],[f104]) ).
fof(f264,plain,
! [X3] :
( aInteger0(X3)
| ~ aElementOf0(X3,stldt0(xB))
| ~ sP21(X3) ),
inference(cnf_transformation,[],[f104]) ).
fof(f266,plain,
! [X10] :
( ~ aElementOf0(X10,stldt0(xB))
| ~ aElementOf0(X10,stldt0(xA))
| ~ aInteger0(X10)
| sP29(X10) ),
inference(cnf_transformation,[],[f104]) ).
fof(f267,plain,
! [X10] :
( aElementOf0(X10,stldt0(xB))
| ~ sP29(X10) ),
inference(cnf_transformation,[],[f104]) ).
fof(f268,plain,
! [X10] :
( aElementOf0(X10,stldt0(xA))
| ~ sP29(X10) ),
inference(cnf_transformation,[],[f104]) ).
fof(f269,plain,
! [X10] :
( aInteger0(X10)
| ~ sP29(X10) ),
inference(cnf_transformation,[],[f104]) ).
fof(f270,plain,
! [X9] :
( aElementOf0(X9,xB)
| ~ aInteger0(X9)
| sP28(X9) ),
inference(cnf_transformation,[],[f104]) ).
fof(f271,plain,
! [X9] :
( ~ aElementOf0(X9,xB)
| ~ sP28(X9) ),
inference(cnf_transformation,[],[f104]) ).
fof(f276,plain,
! [X7] :
( aElementOf0(X7,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(X7)
| sP26(X7) ),
inference(cnf_transformation,[],[f104]) ).
fof(f277,plain,
! [X7] :
( ~ aElementOf0(X7,sdtbsmnsldt0(xA,xB))
| ~ sP26(X7) ),
inference(cnf_transformation,[],[f104]) ).
fof(f278,plain,
! [X7] :
( aInteger0(X7)
| ~ sP26(X7) ),
inference(cnf_transformation,[],[f104]) ).
fof(f280,plain,
( aElementOf0(sK24,stldt0(xA))
| ~ sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f281,plain,
( ~ aElementOf0(sK24,cS1395)
| ~ sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f284,plain,
! [X5] :
( aElementOf0(X5,stldt0(xB))
| ~ sP23(X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f285,plain,
! [X5] :
( ~ aElementOf0(X5,cS1395)
| ~ sP23(X5) ),
inference(cnf_transformation,[],[f104]) ).
fof(f288,plain,
( sP29(sK19)
| aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f289,plain,
( ~ sP29(sK19)
| ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f298,plain,
! [X3] :
( sP29(sK19)
| aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f299,plain,
! [X3] :
( ~ sP29(sK19)
| ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f300,plain,
! [X9] :
( ~ sP28(X9)
| aElementOf0(X9,stldt0(xB))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f301,plain,
! [X9] :
( sP28(X9)
| ~ aElementOf0(X9,stldt0(xB))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f310,plain,
! [X3,X9] :
( ~ sP28(X9)
| aElementOf0(X9,stldt0(xB))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f311,plain,
! [X3,X9] :
( sP28(X9)
| ~ aElementOf0(X9,stldt0(xB))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f324,plain,
! [X7] :
( ~ sP26(X7)
| aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f325,plain,
! [X7] :
( sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f334,plain,
! [X3,X7] :
( ~ sP26(X7)
| aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f335,plain,
! [X3,X7] :
( sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f336,plain,
! [X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f337,plain,
! [X6] :
( sP25(X6)
| ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| sP23(sK20)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f346,plain,
! [X3,X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f347,plain,
! [X3,X6] :
( sP25(X6)
| ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| sP21(X3)
| sP18 ),
inference(cnf_transformation,[],[f104]) ).
fof(f516,plain,
! [X0] :
( aInteger0(X0)
| aElementOf0(X0,cS1395) ),
inference(consistent_polarity_flipping,[],[f239]) ).
fof(f519,plain,
! [X4] :
( aElementOf0(X4,xA)
| aInteger0(X4)
| aElementOf0(X4,stldt0(xA)) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f520,plain,
! [X4] :
( ~ aInteger0(X4)
| ~ aElementOf0(X4,stldt0(xA)) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f560,plain,
! [X3,X6] :
( sP25(X6)
| ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f347]) ).
fof(f561,plain,
! [X3,X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f570,plain,
! [X6] :
( sP25(X6)
| ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f571,plain,
! [X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f572,plain,
! [X3,X7] :
( ~ sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f573,plain,
! [X3,X7] :
( sP26(X7)
| aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f334]) ).
fof(f582,plain,
! [X7] :
( ~ sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f325]) ).
fof(f583,plain,
! [X7] :
( sP26(X7)
| aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f596,plain,
! [X3,X9] :
( ~ sP28(X9)
| ~ aElementOf0(X9,stldt0(xB))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f597,plain,
! [X3,X9] :
( sP28(X9)
| aElementOf0(X9,stldt0(xB))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f606,plain,
! [X9] :
( ~ sP28(X9)
| ~ aElementOf0(X9,stldt0(xB))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f301]) ).
fof(f607,plain,
! [X9] :
( sP28(X9)
| aElementOf0(X9,stldt0(xB))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f608,plain,
! [X3] :
( sP29(sK19)
| ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f299]) ).
fof(f609,plain,
! [X3] :
( ~ sP29(sK19)
| aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP21(X3)
| sP18 ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f618,plain,
( sP29(sK19)
| ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f289]) ).
fof(f619,plain,
( ~ sP29(sK19)
| aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP23(sK20)
| sP18 ),
inference(consistent_polarity_flipping,[],[f288]) ).
fof(f622,plain,
! [X5] :
( ~ aElementOf0(X5,cS1395)
| sP23(X5) ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f623,plain,
! [X5] :
( aElementOf0(X5,stldt0(xB))
| sP23(X5) ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f627,plain,
! [X7] :
( ~ aInteger0(X7)
| sP26(X7) ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f628,plain,
! [X7] :
( ~ aElementOf0(X7,sdtbsmnsldt0(xA,xB))
| sP26(X7) ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f629,plain,
! [X7] :
( ~ sP26(X7)
| aInteger0(X7)
| aElementOf0(X7,sdtbsmnsldt0(xA,xB)) ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f634,plain,
! [X9] :
( ~ aElementOf0(X9,xB)
| sP28(X9) ),
inference(consistent_polarity_flipping,[],[f271]) ).
fof(f635,plain,
! [X9] :
( ~ sP28(X9)
| aInteger0(X9)
| aElementOf0(X9,xB) ),
inference(consistent_polarity_flipping,[],[f270]) ).
fof(f636,plain,
! [X10] :
( ~ aInteger0(X10)
| sP29(X10) ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f637,plain,
! [X10] :
( aElementOf0(X10,stldt0(xA))
| sP29(X10) ),
inference(consistent_polarity_flipping,[],[f268]) ).
fof(f638,plain,
! [X10] :
( aElementOf0(X10,stldt0(xB))
| sP29(X10) ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f639,plain,
! [X10] :
( ~ aElementOf0(X10,stldt0(xB))
| ~ aElementOf0(X10,stldt0(xA))
| aInteger0(X10)
| ~ sP29(X10) ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f641,plain,
! [X3] :
( ~ aElementOf0(X3,stldt0(xB))
| ~ aInteger0(X3)
| sP21(X3) ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f645,plain,
! [X6] :
( ~ aElementOf0(X6,xA)
| aInteger0(X6)
| sP25(X6) ),
inference(consistent_polarity_flipping,[],[f259]) ).
fof(f646,plain,
! [X6] :
( ~ aElementOf0(X6,xB)
| aInteger0(X6)
| sP25(X6) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f648,definition,
( spl30_1
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f652,definition,
( spl30_2
<=> ! [X0] :
( ~ aElementOf0(X0,xA)
| ~ aElementOf0(X0,stldt0(xA)) ) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f653,plain,
( ! [X0] :
( ~ aElementOf0(X0,xA)
| ~ aElementOf0(X0,stldt0(xA)) )
| ~ spl30_2 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f656,definition,
( spl30_3
<=> ! [X0] :
( ~ aInteger0(X0)
| ~ aElementOf0(X0,stldt0(xA)) ) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
fof(f657,plain,
( ! [X0] :
( ~ aElementOf0(X0,stldt0(xA))
| ~ aInteger0(X0) )
| ~ spl30_3 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f660,definition,
( spl30_4
<=> ! [X0] :
( aElementOf0(X0,xA)
| aElementOf0(X0,stldt0(xA))
| aInteger0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
fof(f661,plain,
( ! [X0] :
( aElementOf0(X0,stldt0(xA))
| aElementOf0(X0,xA)
| aInteger0(X0) )
| ~ spl30_4 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f664,definition,
( spl30_5
<=> aElementOf0(sK24,stldt0(xA)) ),
introduced(definition,[new_symbols(definition,[spl30_5])],[avatar_definition]) ).
fof(f666,plain,
( aElementOf0(sK24,stldt0(xA))
| ~ spl30_5 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
( ~ spl30_1
| spl30_5 ),
inference(avatar_split_clause,[],[f280,f664,f648]) ).
fof(f669,definition,
( spl30_6
<=> aElementOf0(sK24,cS1395) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
fof(f671,plain,
( ~ aElementOf0(sK24,cS1395)
| spl30_6 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( ~ spl30_1
| ~ spl30_6 ),
inference(avatar_split_clause,[],[f281,f669,f648]) ).
fof(f674,definition,
( spl30_7
<=> ! [X1] :
( aInteger0(X1)
| aElementOf0(X1,cS1395) ) ),
introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition]) ).
fof(f675,plain,
( ! [X1] :
( aElementOf0(X1,cS1395)
| aInteger0(X1) )
| ~ spl30_7 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f682,definition,
( spl30_9
<=> sP23(sK20) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
fof(f684,plain,
( ~ sP23(sK20)
| spl30_9 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f686,definition,
( spl30_10
<=> aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB))) ),
introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition]) ).
fof(f687,plain,
( ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| spl30_10 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f688,plain,
( aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ spl30_10 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f690,definition,
( spl30_11
<=> sP29(sK19) ),
introduced(definition,[new_symbols(definition,[spl30_11])],[avatar_definition]) ).
fof(f691,plain,
( sP29(sK19)
| ~ spl30_11 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f693,plain,
( spl30_1
| ~ spl30_9
| spl30_10
| ~ spl30_11 ),
inference(avatar_split_clause,[],[f619,f690,f686,f682,f648]) ).
fof(f694,plain,
( spl30_1
| ~ spl30_9
| ~ spl30_10
| spl30_11 ),
inference(avatar_split_clause,[],[f618,f690,f686,f682,f648]) ).
fof(f719,definition,
( spl30_16
<=> ! [X3] : ~ sP21(X3) ),
introduced(definition,[new_symbols(definition,[spl30_16])],[avatar_definition]) ).
fof(f720,plain,
( ! [X3] : ~ sP21(X3)
| ~ spl30_16 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f721,plain,
( spl30_1
| spl30_16
| spl30_10
| ~ spl30_11 ),
inference(avatar_split_clause,[],[f609,f690,f686,f719,f648]) ).
fof(f722,plain,
( spl30_1
| spl30_16
| ~ spl30_10
| spl30_11 ),
inference(avatar_split_clause,[],[f608,f690,f686,f719,f648]) ).
fof(f724,definition,
( spl30_17
<=> ! [X9] :
( sP28(X9)
| aElementOf0(X9,stldt0(xB)) ) ),
introduced(definition,[new_symbols(definition,[spl30_17])],[avatar_definition]) ).
fof(f725,plain,
( ! [X9] :
( aElementOf0(X9,stldt0(xB))
| sP28(X9) )
| ~ spl30_17 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f726,plain,
( spl30_1
| ~ spl30_9
| spl30_17 ),
inference(avatar_split_clause,[],[f607,f724,f682,f648]) ).
fof(f728,definition,
( spl30_18
<=> ! [X9] :
( ~ sP28(X9)
| ~ aElementOf0(X9,stldt0(xB)) ) ),
introduced(definition,[new_symbols(definition,[spl30_18])],[avatar_definition]) ).
fof(f729,plain,
( ! [X9] :
( ~ sP28(X9)
| ~ aElementOf0(X9,stldt0(xB)) )
| ~ spl30_18 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f730,plain,
( spl30_1
| ~ spl30_9
| spl30_18 ),
inference(avatar_split_clause,[],[f606,f728,f682,f648]) ).
fof(f739,plain,
( spl30_1
| spl30_16
| spl30_17 ),
inference(avatar_split_clause,[],[f597,f724,f719,f648]) ).
fof(f740,plain,
( spl30_1
| spl30_16
| spl30_18 ),
inference(avatar_split_clause,[],[f596,f728,f719,f648]) ).
fof(f760,definition,
( spl30_21
<=> ! [X7] :
( sP26(X7)
| aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB))) ) ),
introduced(definition,[new_symbols(definition,[spl30_21])],[avatar_definition]) ).
fof(f761,plain,
( ! [X7] :
( aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
| sP26(X7) )
| ~ spl30_21 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f762,plain,
( spl30_1
| ~ spl30_9
| spl30_21 ),
inference(avatar_split_clause,[],[f583,f760,f682,f648]) ).
fof(f764,definition,
( spl30_22
<=> ! [X7] :
( ~ sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB))) ) ),
introduced(definition,[new_symbols(definition,[spl30_22])],[avatar_definition]) ).
fof(f765,plain,
( ! [X7] :
( ~ sP26(X7)
| ~ aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB))) )
| ~ spl30_22 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f766,plain,
( spl30_1
| ~ spl30_9
| spl30_22 ),
inference(avatar_split_clause,[],[f582,f764,f682,f648]) ).
fof(f775,plain,
( spl30_1
| spl30_16
| spl30_21 ),
inference(avatar_split_clause,[],[f573,f760,f719,f648]) ).
fof(f776,plain,
( spl30_1
| spl30_16
| spl30_22 ),
inference(avatar_split_clause,[],[f572,f764,f719,f648]) ).
fof(f778,definition,
( spl30_23
<=> ! [X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB)) ) ),
introduced(definition,[new_symbols(definition,[spl30_23])],[avatar_definition]) ).
fof(f779,plain,
( ! [X6] :
( ~ sP25(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB)) )
| ~ spl30_23 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f780,plain,
( spl30_1
| ~ spl30_9
| spl30_23 ),
inference(avatar_split_clause,[],[f571,f778,f682,f648]) ).
fof(f782,definition,
( spl30_24
<=> ! [X6] :
( sP25(X6)
| ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB)) ) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
fof(f783,plain,
( ! [X6] :
( ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| sP25(X6) )
| ~ spl30_24 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f784,plain,
( spl30_1
| ~ spl30_9
| spl30_24 ),
inference(avatar_split_clause,[],[f570,f782,f682,f648]) ).
fof(f793,plain,
( spl30_1
| spl30_16
| spl30_23 ),
inference(avatar_split_clause,[],[f561,f778,f719,f648]) ).
fof(f794,plain,
( spl30_1
| spl30_16
| spl30_24 ),
inference(avatar_split_clause,[],[f560,f782,f719,f648]) ).
fof(f836,plain,
spl30_2,
inference(avatar_split_clause,[],[f233,f652]) ).
fof(f837,plain,
spl30_3,
inference(avatar_split_clause,[],[f520,f656]) ).
fof(f838,plain,
spl30_4,
inference(avatar_split_clause,[],[f519,f660]) ).
fof(f839,plain,
spl30_7,
inference(avatar_split_clause,[],[f516,f674]) ).
fof(f861,plain,
( ! [X0] :
( sP23(X0)
| aInteger0(X0) )
| ~ spl30_7 ),
inference(resolution,[],[f675,f622]) ).
fof(f862,plain,
( aInteger0(sK20)
| ~ spl30_7
| spl30_9 ),
inference(resolution,[],[f861,f684]) ).
fof(f872,plain,
( ! [X3] :
( ~ aInteger0(X3)
| ~ aElementOf0(X3,stldt0(xB)) )
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f641,f720]) ).
fof(f873,plain,
( ~ aElementOf0(sK20,stldt0(xB))
| ~ spl30_7
| spl30_9
| ~ spl30_16 ),
inference(resolution,[],[f872,f862]) ).
fof(f875,plain,
( sP23(sK20)
| ~ spl30_7
| spl30_9
| ~ spl30_16 ),
inference(resolution,[],[f873,f623]) ).
fof(f876,plain,
( $false
| ~ spl30_7
| spl30_9
| ~ spl30_16 ),
inference(forward_subsumption_resolution,[],[f875,f684]) ).
fof(f877,plain,
( ~ spl30_7
| spl30_9
| ~ spl30_16 ),
inference(avatar_contradiction_clause,[],[f876]) ).
fof(f879,plain,
( sP26(sK19)
| spl30_10
| ~ spl30_21 ),
inference(resolution,[],[f761,f687]) ).
fof(f880,plain,
( aInteger0(sK19)
| aElementOf0(sK19,sdtbsmnsldt0(xA,xB))
| spl30_10
| ~ spl30_21 ),
inference(resolution,[],[f879,f629]) ).
fof(f883,definition,
( spl30_34
<=> aElementOf0(sK19,sdtbsmnsldt0(xA,xB)) ),
introduced(definition,[new_symbols(definition,[spl30_34])],[avatar_definition]) ).
fof(f885,plain,
( aElementOf0(sK19,sdtbsmnsldt0(xA,xB))
| ~ spl30_34 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f887,definition,
( spl30_35
<=> aInteger0(sK19) ),
introduced(definition,[new_symbols(definition,[spl30_35])],[avatar_definition]) ).
fof(f888,plain,
( ~ aInteger0(sK19)
| spl30_35 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f889,plain,
( aInteger0(sK19)
| ~ spl30_35 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f897,definition,
( spl30_36
<=> aElementOf0(sK19,stldt0(xB)) ),
introduced(definition,[new_symbols(definition,[spl30_36])],[avatar_definition]) ).
fof(f899,plain,
( ~ aElementOf0(sK19,stldt0(xB))
| spl30_36 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f901,definition,
( spl30_37
<=> aElementOf0(sK19,stldt0(xA)) ),
introduced(definition,[new_symbols(definition,[spl30_37])],[avatar_definition]) ).
fof(f903,plain,
( ~ aElementOf0(sK19,stldt0(xA))
| spl30_37 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f906,plain,
( sP28(sK19)
| ~ spl30_17
| spl30_36 ),
inference(resolution,[],[f899,f725]) ).
fof(f907,plain,
( sP29(sK19)
| spl30_36 ),
inference(resolution,[],[f899,f638]) ).
fof(f910,definition,
( spl30_38
<=> aElementOf0(sK19,xB) ),
introduced(definition,[new_symbols(definition,[spl30_38])],[avatar_definition]) ).
fof(f912,plain,
( aElementOf0(sK19,xB)
| ~ spl30_38 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f914,plain,
( aElementOf0(sK19,xA)
| aInteger0(sK19)
| ~ spl30_4
| spl30_37 ),
inference(resolution,[],[f903,f661]) ).
fof(f916,plain,
( sP29(sK19)
| spl30_37 ),
inference(resolution,[],[f903,f637]) ).
fof(f918,definition,
( spl30_39
<=> aElementOf0(sK19,xA) ),
introduced(definition,[new_symbols(definition,[spl30_39])],[avatar_definition]) ).
fof(f920,plain,
( aElementOf0(sK19,xA)
| ~ spl30_39 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f921,plain,
( spl30_35
| spl30_39
| ~ spl30_4
| spl30_37 ),
inference(avatar_split_clause,[],[f914,f901,f660,f918,f887]) ).
fof(f925,plain,
( ~ aElementOf0(sK19,stldt0(xA))
| ~ spl30_2
| ~ spl30_39 ),
inference(resolution,[],[f920,f653]) ).
fof(f926,plain,
( aInteger0(sK19)
| sP25(sK19)
| ~ spl30_39 ),
inference(resolution,[],[f920,f645]) ).
fof(f929,definition,
( spl30_40
<=> sP25(sK19) ),
introduced(definition,[new_symbols(definition,[spl30_40])],[avatar_definition]) ).
fof(f931,plain,
( sP25(sK19)
| ~ spl30_40 ),
inference(avatar_component_clause,[],[f929]) ).
fof(f932,plain,
( spl30_40
| spl30_35
| ~ spl30_39 ),
inference(avatar_split_clause,[],[f926,f918,f887,f929]) ).
fof(f933,plain,
( aElementOf0(sK19,sdtbsmnsldt0(xA,xB))
| ~ spl30_23
| ~ spl30_40 ),
inference(resolution,[],[f931,f779]) ).
fof(f937,plain,
( spl30_34
| ~ spl30_23
| ~ spl30_40 ),
inference(avatar_split_clause,[],[f933,f929,f778,f883]) ).
fof(f940,plain,
( sP25(sK19)
| ~ spl30_24
| ~ spl30_34 ),
inference(resolution,[],[f885,f783]) ).
fof(f941,plain,
( sP26(sK19)
| ~ spl30_34 ),
inference(resolution,[],[f885,f628]) ).
fof(f943,plain,
( ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ spl30_22
| ~ spl30_34 ),
inference(resolution,[],[f941,f765]) ).
fof(f946,plain,
( spl30_11
| spl30_37 ),
inference(avatar_split_clause,[],[f916,f901,f690]) ).
fof(f947,plain,
( ~ spl30_10
| ~ spl30_22
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f943,f883,f764,f686]) ).
fof(f948,plain,
( ~ spl30_37
| ~ spl30_2
| ~ spl30_39 ),
inference(avatar_split_clause,[],[f925,f918,f652,f901]) ).
fof(f953,plain,
( aInteger0(sK19)
| sP25(sK19)
| ~ spl30_38 ),
inference(resolution,[],[f912,f646]) ).
fof(f954,plain,
( sP28(sK19)
| ~ spl30_38 ),
inference(resolution,[],[f912,f634]) ).
fof(f957,plain,
( spl30_40
| ~ spl30_24
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f940,f883,f782,f929]) ).
fof(f994,plain,
( sP29(sK19)
| ~ spl30_35 ),
inference(resolution,[],[f889,f636]) ).
fof(f997,plain,
( sP26(sK19)
| ~ spl30_35 ),
inference(resolution,[],[f889,f627]) ).
fof(f1002,plain,
( spl30_11
| spl30_36 ),
inference(avatar_split_clause,[],[f907,f897,f690]) ).
fof(f1003,plain,
( spl30_11
| ~ spl30_35 ),
inference(avatar_split_clause,[],[f994,f887,f690]) ).
fof(f1102,plain,
( aInteger0(sK19)
| aElementOf0(sK19,xB)
| ~ spl30_17
| spl30_36 ),
inference(resolution,[],[f906,f635]) ).
fof(f1343,plain,
( ~ aElementOf0(sK19,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ spl30_22
| ~ spl30_35 ),
inference(resolution,[],[f997,f765]) ).
fof(f1344,plain,
( $false
| ~ spl30_10
| ~ spl30_22
| ~ spl30_35 ),
inference(forward_subsumption_resolution,[],[f1343,f688]) ).
fof(f1345,plain,
( ~ spl30_10
| ~ spl30_22
| ~ spl30_35 ),
inference(avatar_contradiction_clause,[],[f1344]) ).
fof(f1348,plain,
( spl30_40
| spl30_35
| ~ spl30_38 ),
inference(avatar_split_clause,[],[f953,f910,f887,f929]) ).
fof(f1350,plain,
( ! [X10] :
( ~ sP29(X10)
| ~ aElementOf0(X10,stldt0(xA))
| ~ aElementOf0(X10,stldt0(xB)) )
| ~ spl30_3 ),
inference(forward_subsumption_resolution,[],[f639,f657]) ).
fof(f1506,plain,
( aElementOf0(sK19,xA)
| aElementOf0(sK19,xB)
| ~ spl30_40 ),
inference(resolution,[],[f931,f257]) ).
fof(f1508,plain,
( spl30_38
| spl30_39
| ~ spl30_40 ),
inference(avatar_split_clause,[],[f1506,f929,f918,f910]) ).
fof(f1534,plain,
( ~ aElementOf0(sK19,stldt0(xB))
| ~ spl30_18
| ~ spl30_38 ),
inference(resolution,[],[f954,f729]) ).
fof(f1537,plain,
( ~ spl30_36
| ~ spl30_18
| ~ spl30_38 ),
inference(avatar_split_clause,[],[f1534,f910,f728,f897]) ).
fof(f1539,plain,
( ~ aElementOf0(sK19,stldt0(xA))
| ~ aElementOf0(sK19,stldt0(xB))
| ~ spl30_3
| ~ spl30_11 ),
inference(resolution,[],[f691,f1350]) ).
fof(f1540,plain,
( ~ spl30_36
| ~ spl30_37
| ~ spl30_3
| ~ spl30_11 ),
inference(avatar_split_clause,[],[f1539,f690,f656,f901,f897]) ).
fof(f1541,plain,
( aElementOf0(sK19,xB)
| ~ spl30_17
| spl30_35
| spl30_36 ),
inference(forward_subsumption_resolution,[],[f1102,f888]) ).
fof(f1542,plain,
( spl30_38
| ~ spl30_17
| spl30_35
| spl30_36 ),
inference(avatar_split_clause,[],[f1541,f897,f887,f724,f910]) ).
fof(f1543,plain,
( aElementOf0(sK19,sdtbsmnsldt0(xA,xB))
| spl30_10
| ~ spl30_21
| spl30_35 ),
inference(forward_subsumption_resolution,[],[f880,f888]) ).
fof(f1548,plain,
( spl30_34
| spl30_10
| ~ spl30_21
| spl30_35 ),
inference(avatar_split_clause,[],[f1543,f887,f760,f686,f883]) ).
fof(f1551,plain,
( aInteger0(sK24)
| spl30_6
| ~ spl30_7 ),
inference(resolution,[],[f671,f675]) ).
fof(f1552,plain,
( ~ aInteger0(sK24)
| ~ spl30_3
| ~ spl30_5 ),
inference(resolution,[],[f666,f657]) ).
fof(f1598,plain,
( $false
| ~ spl30_3
| ~ spl30_5
| spl30_6
| ~ spl30_7 ),
inference(forward_subsumption_resolution,[],[f1552,f1551]) ).
fof(f1599,plain,
( ~ spl30_3
| ~ spl30_5
| spl30_6
| ~ spl30_7 ),
inference(avatar_contradiction_clause,[],[f1598]) ).
cnf(s4,plain,
( ~ spl30_1
| spl30_5 ),
inference(sat_conversion,[],[f667]) ).
cnf(s5,plain,
( ~ spl30_1
| ~ spl30_6 ),
inference(sat_conversion,[],[f672]) ).
cnf(s8,plain,
( spl30_1
| ~ spl30_9
| spl30_10
| ~ spl30_11 ),
inference(sat_conversion,[],[f693]) ).
cnf(s9,plain,
( spl30_1
| ~ spl30_9
| ~ spl30_10
| spl30_11 ),
inference(sat_conversion,[],[f694]) ).
cnf(s18,plain,
( spl30_1
| spl30_10
| ~ spl30_11
| spl30_16 ),
inference(sat_conversion,[],[f721]) ).
cnf(s19,plain,
( spl30_1
| ~ spl30_10
| spl30_11
| spl30_16 ),
inference(sat_conversion,[],[f722]) ).
cnf(s20,plain,
( spl30_1
| ~ spl30_9
| spl30_17 ),
inference(sat_conversion,[],[f726]) ).
cnf(s21,plain,
( spl30_1
| ~ spl30_9
| spl30_18 ),
inference(sat_conversion,[],[f730]) ).
cnf(s30,plain,
( spl30_1
| spl30_16
| spl30_17 ),
inference(sat_conversion,[],[f739]) ).
cnf(s31,plain,
( spl30_1
| spl30_16
| spl30_18 ),
inference(sat_conversion,[],[f740]) ).
cnf(s44,plain,
( spl30_1
| ~ spl30_9
| spl30_21 ),
inference(sat_conversion,[],[f762]) ).
cnf(s45,plain,
( spl30_1
| ~ spl30_9
| spl30_22 ),
inference(sat_conversion,[],[f766]) ).
cnf(s54,plain,
( spl30_1
| spl30_16
| spl30_21 ),
inference(sat_conversion,[],[f775]) ).
cnf(s55,plain,
( spl30_1
| spl30_16
| spl30_22 ),
inference(sat_conversion,[],[f776]) ).
cnf(s56,plain,
( spl30_1
| ~ spl30_9
| spl30_23 ),
inference(sat_conversion,[],[f780]) ).
cnf(s57,plain,
( spl30_1
| ~ spl30_9
| spl30_24 ),
inference(sat_conversion,[],[f784]) ).
cnf(s66,plain,
( spl30_1
| spl30_16
| spl30_23 ),
inference(sat_conversion,[],[f793]) ).
cnf(s67,plain,
( spl30_1
| spl30_16
| spl30_24 ),
inference(sat_conversion,[],[f794]) ).
cnf(s89,plain,
spl30_2,
inference(sat_conversion,[],[f836]) ).
cnf(s90,plain,
spl30_3,
inference(sat_conversion,[],[f837]) ).
cnf(s91,plain,
spl30_4,
inference(sat_conversion,[],[f838]) ).
cnf(s92,plain,
spl30_7,
inference(sat_conversion,[],[f839]) ).
cnf(s103,plain,
( ~ spl30_7
| spl30_9
| ~ spl30_16 ),
inference(sat_conversion,[],[f877]) ).
cnf(s107,plain,
( ~ spl30_4
| spl30_35
| spl30_37
| spl30_39 ),
inference(sat_conversion,[],[f921]) ).
cnf(s109,plain,
( spl30_35
| ~ spl30_39
| spl30_40 ),
inference(sat_conversion,[],[f932]) ).
cnf(s111,plain,
( ~ spl30_23
| spl30_34
| ~ spl30_40 ),
inference(sat_conversion,[],[f937]) ).
cnf(s113,plain,
( spl30_11
| spl30_37 ),
inference(sat_conversion,[],[f946]) ).
cnf(s114,plain,
( ~ spl30_10
| ~ spl30_22
| ~ spl30_34 ),
inference(sat_conversion,[],[f947]) ).
cnf(s115,plain,
( ~ spl30_2
| ~ spl30_37
| ~ spl30_39 ),
inference(sat_conversion,[],[f948]) ).
cnf(s118,plain,
( ~ spl30_24
| ~ spl30_34
| spl30_40 ),
inference(sat_conversion,[],[f957]) ).
cnf(s129,plain,
( spl30_11
| spl30_36 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s131,plain,
( spl30_11
| ~ spl30_35 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s153,plain,
( ~ spl30_10
| ~ spl30_22
| ~ spl30_35 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s159,plain,
( spl30_35
| ~ spl30_38
| spl30_40 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s168,plain,
( spl30_38
| spl30_39
| ~ spl30_40 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s172,plain,
( ~ spl30_18
| ~ spl30_36
| ~ spl30_38 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s174,plain,
( ~ spl30_3
| ~ spl30_11
| ~ spl30_36
| ~ spl30_37 ),
inference(sat_conversion,[],[f1540]) ).
cnf(s175,plain,
( ~ spl30_17
| spl30_35
| spl30_36
| spl30_38 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s178,plain,
( spl30_10
| ~ spl30_21
| spl30_34
| spl30_35 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s184,plain,
( ~ spl30_3
| ~ spl30_5
| spl30_6
| ~ spl30_7 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s186,plain,
( spl30_10
| spl30_16
| spl30_1 ),
inference(rat,[],[s168,s118,s115,s172,s178,s113,s129,s131,s18,s31,s67,s54,s89]) ).
cnf(s187,plain,
( spl30_16
| spl30_1 ),
inference(rat,[],[s174,s107,s175,s109,s159,s111,s19,s114,s153,s186,s55,s66,s30,s91,s90]) ).
cnf(s188,plain,
( spl30_10
| spl30_1 ),
inference(rat,[],[s168,s118,s115,s172,s178,s113,s129,s131,s8,s57,s44,s21,s103,s187,s89,s92]) ).
cnf(s189,plain,
( ~ spl30_9
| spl30_1 ),
inference(rat,[],[s174,s107,s175,s109,s159,s111,s9,s114,s153,s188,s20,s45,s56,s91,s90]) ).
cnf(s190,plain,
spl30_1,
inference(rat,[],[s189,s103,s187,s92]) ).
cnf(s192,plain,
~ spl30_6,
inference(rat,[],[s5,s190]) ).
cnf(s193,plain,
spl30_5,
inference(rat,[],[s4,s190]) ).
cnf(s194,plain,
$false,
inference(rat,[],[s184,s92,s90,s192,s193]) ).
fof(f1600,plain,
$false,
inference(avatar_sat_refutation,[],[s194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM440+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 % Computer : n008.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 19:56:10 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.50 % (1563780)Will run a generic schedule for satisfiability detection.
% 0.19/0.50 % (1563789)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3114974558:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.50 % (1563786)% WARNING: option uhcvi not known.
% 0.19/0.50 % (1563790)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3942277011:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.50 % (1563785)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3607595495_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.50 % (1563786)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3291360819:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.50 % (1563787)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1786697982:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.50 % (1563788)dis+10_1_sil=32000:sp=arity:random_seed=1411190764:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.50 % (1563791)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=495644464:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.50 % TRYING [1]
% 0.19/0.50 % TRYING [2]
% 0.19/0.50 % TRYING [3]
% 0.19/0.50 % (1563786) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1563780-1563786"...
% 0.19/0.50 % (1563786)...printing done.
% 0.19/0.50 % (1563786)Refutation found. Thanks to Tanya!
% 0.19/0.50 % SZS status Theorem for theBenchmark
% 0.19/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.51 % (1563786)------------------------------
% 0.19/0.51 % (1563786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.51 % (1563786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.51 % (1563786)CaDiCaL version: 2.1.3
% 0.19/0.51 % (1563786)Termination reason: Refutation
% 0.19/0.51 % (1563786)Time elapsed: 0.027 s
% 0.19/0.51 % (1563786)Peak memory usage: 13 MB
% 0.19/0.51 % (1563786)Instructions burned: 40 (million)
% 0.19/0.51 % (1563780)Success in time 0.063 s
% 0.19/0.51 % Vampire exiting
%------------------------------------------------------------------------------