%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR230+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:05:09 AM UTC 2026
% Result : Theorem 96.15s 21.25s
% Output : CNFRefutation 96.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 15
% Syntax : Number of formulae : 81 ( 29 unt; 0 def)
% Number of atoms : 184 ( 23 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 187 ( 84 ~; 83 |; 14 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 83 ( 4 sgn 13 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(predefinitionsA8,axiom,
! [X0,X1,X2] :
( ( 'p$u$ud$u$usubclass'(X1,X2)
& 'p$u$ud$u$usubclass'(X0,X1) )
=> 'p$u$ud$u$usubclass'(X0,X2) ) ).
fof(predefinitionsA12,axiom,
! [X0,X1,X2] :
( ( 'p$u$ud$u$usubclass'(X1,X2)
& 'p$u$ud$u$uinstance'(X0,X1) )
=> 'p$u$ud$u$uinstance'(X0,X2) ) ).
fof(predefinitionsA15,axiom,
! [X0,X1] :
( 'p$u$ud$u$udisjoint'(X0,X1)
<=> ! [X2] :
( ~ 'p$u$ud$u$uinstance'(X2,X1)
| ~ 'p$u$ud$u$uinstance'(X2,X0) ) ) ).
fof(mergeA176,axiom,
! [X0] :
( 'p$u$ud$u$usubclass'(X0,'c$u$uEntity')
=> ? [X1] : 'p$u$ud$u$uinstance'(X1,X0) ) ).
fof(mergeA178,axiom,
'p$u$ud$u$usubclass'('c$u$uPhysical','c$u$uEntity') ).
fof(mergeA181,axiom,
'p$u$ud$u$usubclass'('c$u$uObject','c$u$uPhysical') ).
fof(mergeA312,axiom,
'p$u$ud$u$usubclass'('c$u$uAgent','c$u$uObject') ).
fof(mergeA2906,axiom,
'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uAgent') ).
fof(mergeA2907,axiom,
'p$u$ud$u$udisjoint'('c$u$uOrganism','c$u$uArtifact') ).
fof(mergeA3134,axiom,
'p$u$ud$u$usubclass'('c$u$uArtifact','c$u$uObject') ).
fof(mergeA3169,axiom,
'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uArtifact') ).
fof(mergeA3681,axiom,
'p$u$ud$u$usubclass'('c$u$uDevelopmentalAttribute','c$u$uBiologicalAttribute') ).
fof(mergeA3688,axiom,
! [X0] :
( 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
=> ? [X1] :
( 'p$u$uattribute'(X0,X1)
& 'p$u$ud$u$uinstance'(X1,'c$u$uDevelopmentalAttribute') ) ) ).
fof(typeA68,axiom,
! [X0,X1] :
( 'p$u$uattribute'(X0,X1)
=> ( 'p$u$ud$u$uinstance'(X0,'c$u$uObject')
& 'p$u$ud$u$uinstance'(X1,'c$u$uAttribute') ) ) ).
fof(antonymPattern32292,conjecture,
? [X0,X1] :
( X0 != X1
& ? [X2] :
( 'p$u$uattribute'(X0,X2)
& 'p$u$ud$u$uinstance'(X2,'c$u$uBiologicalAttribute')
& 'p$u$ud$u$uinstance'(X2,'c$u$uAttribute') )
& 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
& 'p$u$ud$u$uinstance'(X0,'c$u$uObject') ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] :
( X0 != X1
& ? [X2] :
( 'p$u$uattribute'(X0,X2)
& 'p$u$ud$u$uinstance'(X2,'c$u$uBiologicalAttribute')
& 'p$u$ud$u$uinstance'(X2,'c$u$uAttribute') )
& 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
& 'p$u$ud$u$uinstance'(X0,'c$u$uObject') ),
inference(negate_conjecture,[status(cth)],[antonymPattern32292]) ).
cnf(c1,plain,
( 'p$u$ud$u$usubclass'(X0,X2)
| ~ 'p$u$ud$u$usubclass'(X1,X2)
| ~ 'p$u$ud$u$usubclass'(X0,X1) ),
inference(clausification,[status(esa)],[predefinitionsA8]) ).
cnf(c3,plain,
( 'p$u$ud$u$uinstance'(X0,X2)
| ~ 'p$u$ud$u$usubclass'(X1,X2)
| ~ 'p$u$ud$u$uinstance'(X0,X1) ),
inference(clausification,[status(esa)],[predefinitionsA12]) ).
cnf(c4,plain,
( ~ 'p$u$ud$u$uinstance'(X2,X1)
| ~ 'p$u$ud$u$uinstance'(X2,X0)
| ~ 'p$u$ud$u$udisjoint'(X0,X1) ),
inference(clausification,[status(esa)],[predefinitionsA15]) ).
cnf(c5,plain,
( 'p$u$ud$u$uinstance'(sK12(X0,X1),X0)
| 'p$u$ud$u$udisjoint'(X0,X1) ),
inference(clausification,[status(esa)],[predefinitionsA15]) ).
cnf(c6,plain,
( 'p$u$ud$u$uinstance'(sK12(X0,X1),X1)
| 'p$u$ud$u$udisjoint'(X0,X1) ),
inference(clausification,[status(esa)],[predefinitionsA15]) ).
cnf(c74,plain,
( 'p$u$ud$u$uinstance'(sK78(X0),X0)
| ~ 'p$u$ud$u$usubclass'(X0,'c$u$uEntity') ),
inference(clausification,[status(esa)],[mergeA176]) ).
cnf(c77,plain,
'p$u$ud$u$usubclass'('c$u$uPhysical','c$u$uEntity'),
inference(clausification,[status(esa)],[mergeA178]) ).
cnf(c79,plain,
'p$u$ud$u$usubclass'('c$u$uObject','c$u$uPhysical'),
inference(clausification,[status(esa)],[mergeA181]) ).
cnf(c109,plain,
'p$u$ud$u$usubclass'('c$u$uAgent','c$u$uObject'),
inference(clausification,[status(esa)],[mergeA312]) ).
cnf(c209,plain,
'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uAgent'),
inference(clausification,[status(esa)],[mergeA2906]) ).
cnf(c210,plain,
'p$u$ud$u$udisjoint'('c$u$uOrganism','c$u$uArtifact'),
inference(clausification,[status(esa)],[mergeA2907]) ).
cnf(c240,plain,
'p$u$ud$u$usubclass'('c$u$uArtifact','c$u$uObject'),
inference(clausification,[status(esa)],[mergeA3134]) ).
cnf(c247,plain,
'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uArtifact'),
inference(clausification,[status(esa)],[mergeA3169]) ).
cnf(c295,plain,
'p$u$ud$u$usubclass'('c$u$uDevelopmentalAttribute','c$u$uBiologicalAttribute'),
inference(clausification,[status(esa)],[mergeA3681]) ).
cnf(c300,plain,
( 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uDevelopmentalAttribute')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism') ),
inference(clausification,[status(esa)],[mergeA3688]) ).
cnf(c301,plain,
( 'p$u$uattribute'(X0,sK182(X0))
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism') ),
inference(clausification,[status(esa)],[mergeA3688]) ).
cnf(c370,plain,
( 'p$u$ud$u$uinstance'(X1,'c$u$uAttribute')
| ~ 'p$u$uattribute'(X0,X1) ),
inference(clausification,[status(esa)],[typeA68]) ).
cnf(c396,plain,
( ~ 'p$u$ud$u$uinstance'(X2,'c$u$uObject')
| ~ 'p$u$uattribute'(X2,X1)
| ~ 'p$u$ud$u$uinstance'(X1,'c$u$uBiologicalAttribute')
| X2 = X0
| ~ 'p$u$ud$u$uinstance'(X1,'c$u$uAttribute')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( 'p$u$ud$u$uinstance'(sK78(X0),X1)
| ~ 'p$u$ud$u$usubclass'(X0,X1)
| ~ 'p$u$ud$u$usubclass'(X0,'c$u$uEntity') ),
inference(resolution,[status(thm)],[c74,c3]) ).
cnf(d1,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uAttribute') ),
inference(resolution,[status(thm)],[c370,c301]) ).
cnf(d2,plain,
( ~ 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
| ~ 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uBiologicalAttribute')
| ~ 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uAttribute')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uObject')
| X0 = X1
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism') ),
inference(resolution,[status(thm)],[c301,c396]) ).
cnf(d3,plain,
( 'p$u$ud$u$uinstance'(sK182(X0),X1)
| ~ 'p$u$ud$u$usubclass'('c$u$uDevelopmentalAttribute',X1)
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism') ),
inference(resolution,[status(thm)],[c300,c3]) ).
cnf(d4,plain,
( ~ 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uAttribute')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
| X0 = X1
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$usubclass'('c$u$uDevelopmentalAttribute','c$u$uBiologicalAttribute') ),
inference(resolution,[status(thm)],[d3,d2]) ).
cnf(d5,plain,
( ~ 'p$u$ud$u$uinstance'(sK182(X0),'c$u$uAttribute')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
| X0 = X1 ),
inference(resolution,[status(thm)],[c295,d4]) ).
cnf(d6,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
| X0 = X1 ),
inference(resolution,[status(thm)],[d5,d1]) ).
cnf(d7,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uEntity')
| ~ 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| sK78('c$u$uOrganism') = X0 ),
inference(resolution,[status(thm)],[d6,c74]) ).
cnf(d8,plain,
( ~ 'p$u$ud$u$usubclass'(X0,'c$u$uPhysical')
| 'p$u$ud$u$usubclass'(X0,'c$u$uEntity') ),
inference(resolution,[status(thm)],[c77,c1]) ).
cnf(d9,plain,
( ~ 'p$u$ud$u$usubclass'(X0,'c$u$uObject')
| 'p$u$ud$u$usubclass'(X0,'c$u$uPhysical') ),
inference(resolution,[status(thm)],[c79,c1]) ).
cnf(d10,plain,
( ~ 'p$u$ud$u$usubclass'(X0,'c$u$uAgent')
| 'p$u$ud$u$usubclass'(X0,'c$u$uObject') ),
inference(resolution,[status(thm)],[c109,c1]) ).
cnf(d11,plain,
'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uObject'),
inference(resolution,[status(thm)],[d10,c209]) ).
cnf(d12,plain,
'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uPhysical'),
inference(resolution,[status(thm)],[d11,d9]) ).
cnf(d13,plain,
'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uEntity'),
inference(resolution,[status(thm)],[d12,d8]) ).
cnf(d14,plain,
( ~ 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| sK78('c$u$uOrganism') = X0 ),
inference(resolution,[status(thm)],[d13,d7]) ).
cnf(d15,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uEntity')
| ~ 'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uObject')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| sK78('c$u$uOrganism') = X0 ),
inference(resolution,[status(thm)],[d14,d0]) ).
cnf(d16,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| ~ 'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uEntity')
| sK78('c$u$uOrganism') = X0 ),
inference(resolution,[status(thm)],[d11,d15]) ).
cnf(d17,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| sK78('c$u$uOrganism') = X0 ),
inference(resolution,[status(thm)],[d13,d16]) ).
cnf(d18,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity')
| sK78('c$u$uOrganism') = sK78('c$u$uFabric') ),
inference(resolution,[status(thm)],[d17,c74]) ).
cnf(d19,plain,
( ~ 'p$u$ud$u$usubclass'(X0,'c$u$uArtifact')
| 'p$u$ud$u$usubclass'(X0,'c$u$uObject') ),
inference(resolution,[status(thm)],[c240,c1]) ).
cnf(d20,plain,
'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uObject'),
inference(resolution,[status(thm)],[d19,c247]) ).
cnf(d21,plain,
'p$u$ud$u$usubclass'('c$u$uObject','c$u$uEntity'),
inference(resolution,[status(thm)],[d8,c79]) ).
cnf(d22,plain,
( ~ 'p$u$ud$u$usubclass'(X0,'c$u$uObject')
| 'p$u$ud$u$usubclass'(X0,'c$u$uEntity') ),
inference(resolution,[status(thm)],[d21,c1]) ).
cnf(d23,plain,
'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity'),
inference(resolution,[status(thm)],[d22,d20]) ).
cnf(d24,plain,
sK78('c$u$uOrganism') = sK78('c$u$uFabric'),
inference(resolution,[status(thm)],[d23,d18]) ).
cnf(d25,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity')
| 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uFabric') ),
inference(superposition,[status(thm)],[d24,c74]) ).
cnf(d26,plain,
'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uFabric'),
inference(resolution,[status(thm)],[d23,d25]) ).
cnf(d27,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uOrganism')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uArtifact') ),
inference(resolution,[status(thm)],[c210,c4]) ).
cnf(d28,plain,
( 'p$u$ud$u$udisjoint'(X0,'c$u$uArtifact')
| ~ 'p$u$ud$u$uinstance'(sK12(X0,'c$u$uArtifact'),'c$u$uOrganism') ),
inference(resolution,[status(thm)],[d27,c6]) ).
cnf(d29,plain,
( 'p$u$ud$u$uinstance'(sK12(X0,X1),X2)
| ~ 'p$u$ud$u$usubclass'(X0,X2)
| 'p$u$ud$u$udisjoint'(X0,X1) ),
inference(resolution,[status(thm)],[c5,c3]) ).
cnf(d30,plain,
( 'p$u$ud$u$udisjoint'('c$u$uFabric',X0)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric',X0) ),
inference(resolution,[status(thm)],[d17,c5]) ).
cnf(d31,plain,
( ~ 'p$u$ud$u$uinstance'(X1,'c$u$uFabric')
| ~ 'p$u$ud$u$uinstance'(X1,X0)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric',X0) ),
inference(resolution,[status(thm)],[d30,c4]) ).
cnf(d32,plain,
( 'p$u$ud$u$udisjoint'('c$u$uFabric',X1)
| ~ 'p$u$ud$u$uinstance'(sK12('c$u$uFabric',X1),X0)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric',X0) ),
inference(resolution,[status(thm)],[d31,c5]) ).
cnf(d33,plain,
( 'p$u$ud$u$udisjoint'('c$u$uFabric',X1)
| ~ 'p$u$ud$u$usubclass'('c$u$uFabric',X0)
| 'p$u$ud$u$udisjoint'('c$u$uFabric',X1)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric',X0) ),
inference(resolution,[status(thm)],[d32,d29]) ).
cnf(d34,plain,
( 'p$u$ud$u$udisjoint'('c$u$uFabric',X0)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric','c$u$uArtifact') ),
inference(resolution,[status(thm)],[d33,c247]) ).
cnf(d35,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| ~ 'p$u$ud$u$uinstance'(X0,X1)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric','c$u$uArtifact') ),
inference(resolution,[status(thm)],[d34,c4]) ).
cnf(d36,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity')
| ~ 'p$u$ud$u$uinstance'(sK78('c$u$uFabric'),X0)
| sK78('c$u$uOrganism') = sK12('c$u$uFabric','c$u$uArtifact') ),
inference(resolution,[status(thm)],[d35,c74]) ).
cnf(d37,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity')
| ~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uEntity')
| sK78('c$u$uOrganism') = sK12('c$u$uFabric','c$u$uArtifact') ),
inference(resolution,[status(thm)],[d36,c74]) ).
cnf(d38,plain,
sK78('c$u$uOrganism') = sK12('c$u$uFabric','c$u$uArtifact'),
inference(resolution,[status(thm)],[d23,d37]) ).
cnf(d39,plain,
( 'p$u$ud$u$udisjoint'('c$u$uFabric','c$u$uArtifact')
| ~ 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uOrganism') ),
inference(superposition,[status(thm)],[d38,d28]) ).
cnf(d40,plain,
( ~ 'p$u$ud$u$usubclass'('c$u$uOrganism','c$u$uEntity')
| 'p$u$ud$u$udisjoint'('c$u$uFabric','c$u$uArtifact') ),
inference(resolution,[status(thm)],[d39,c74]) ).
cnf(d41,plain,
'p$u$ud$u$udisjoint'('c$u$uFabric','c$u$uArtifact'),
inference(resolution,[status(thm)],[d13,d40]) ).
cnf(d42,plain,
( ~ 'p$u$ud$u$uinstance'(X0,'c$u$uFabric')
| ~ 'p$u$ud$u$uinstance'(X0,'c$u$uArtifact') ),
inference(resolution,[status(thm)],[d41,c4]) ).
cnf(d43,plain,
~ 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),'c$u$uArtifact'),
inference(resolution,[status(thm)],[d42,d26]) ).
cnf(d44,plain,
( 'p$u$ud$u$uinstance'(sK78('c$u$uOrganism'),X0)
| ~ 'p$u$ud$u$usubclass'('c$u$uFabric',X0) ),
inference(resolution,[status(thm)],[d26,c3]) ).
cnf(d45,plain,
~ 'p$u$ud$u$usubclass'('c$u$uFabric','c$u$uArtifact'),
inference(resolution,[status(thm)],[d44,d43]) ).
cnf(d46,plain,
$false,
inference(resolution,[status(thm)],[c247,d45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR230+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n003.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 27 01:36:57 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 96.15/21.25 % SZS status Theorem for theBenchmark.p
% 96.15/21.25 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------