%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR216+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 : n017.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:08 AM UTC 2026
% Result : Theorem 76.02s 14.74s
% Output : CNFRefutation 76.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR216+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 01:28:04 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 76.02/14.74 % SZS status Theorem for theBenchmark.p
% 76.02/14.74 % SZS output start CNFRefutation for theBenchmark.p
% 76.02/14.74 fof(predefinitionsA8, axiom, ! [X0] : ! [X1] : ! [X2] : ((('p$u$ud$u$usubclass'(X0,X1) & 'p$u$ud$u$usubclass'(X1,X2)) => 'p$u$ud$u$usubclass'(X0,X2)))).
% 76.02/14.74 fof(predefinitionsA12, axiom, ! [X0] : ! [X1] : ! [X2] : ((('p$u$ud$u$uinstance'(X0,X1) & 'p$u$ud$u$usubclass'(X1,X2)) => 'p$u$ud$u$uinstance'(X0,X2)))).
% 76.02/14.74 fof(mergeA90, axiom, (! [X0] : ! [X1] : ((('p$u$ud$u$uinstance'(X1,'c$u$uAttribute') & 'p$u$ud$u$uinstance'(X0,'c$u$uAttribute')) => ('p$u$ucontraryAttribute2'(X0,X1) <=> (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X0)) => ~'p$u$uattribute'(X2,X1))) & ! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X1)) => ~'p$u$uattribute'(X2,X0))))))) & ! [X0] : ! [X1] : ! [X3] : ! [X4] : ((('p$u$ud$u$uinstance'(X4,'c$u$uAttribute') & ('p$u$ud$u$uinstance'(X3,'c$u$uAttribute') & ('p$u$ud$u$uinstance'(X1,'c$u$uAttribute') & 'p$u$ud$u$uinstance'(X0,'c$u$uAttribute')))) => ('p$u$ucontraryAttribute4'(X0,X1,X3,X4) <=> (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X0)) => ~'p$u$uattribute'(X2,X1))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X1)) => ~'p$u$uattribute'(X2,X0))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X0)) => ~'p$u$uattribute'(X2,X3))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X3)) => ~'p$u$uattribute'(X2,X0))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X0)) => ~'p$u$uattribute'(X2,X4))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X4)) => ~'p$u$uattribute'(X2,X0))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X1)) => ~'p$u$uattribute'(X2,X3))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X3)) => ~'p$u$uattribute'(X2,X1))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X1)) => ~'p$u$uattribute'(X2,X4))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X4)) => ~'p$u$uattribute'(X2,X1))) & (! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X3)) => ~'p$u$uattribute'(X2,X4))) & ! [X2] : ((('p$u$ud$u$uinstance'(X2,'c$u$uObject') & 'p$u$uattribute'(X2,X4)) => ~'p$u$uattribute'(X2,X3))))))))))))))))))).
% 76.02/14.74 fof(mergeA351, axiom, 'p$u$ud$u$usubclass'('c$u$uInternalAttribute','c$u$uAttribute')).
% 76.02/14.74 fof(mergeA3560, axiom, 'p$u$ud$u$usubclass'('c$u$uPhysicalState','c$u$uInternalAttribute')).
% 76.02/14.74 fof(mergeA3561, axiom, 'p$u$ucontraryAttribute4'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma')).
% 76.02/14.74 fof(mergeA3563, axiom, 'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uPhysicalState')).
% 76.02/14.74 fof(mergeA3566, axiom, 'p$u$usubAttribute'('c$u$uLiquid','c$u$uFluid')).
% 76.02/14.74 fof(mergeA3569, axiom, 'p$u$usubAttribute'('c$u$uGas','c$u$uFluid')).
% 76.02/14.74 fof(mergeA3572, axiom, 'p$u$usubAttribute'('c$u$uPlasma','c$u$uFluid')).
% 76.02/14.74 fof(typeA2, axiom, ! [X0] : ! [X1] : (('p$u$usubAttribute'(X0,X1) => ('p$u$ud$u$uinstance'(X1,'c$u$uAttribute') & 'p$u$ud$u$uinstance'(X0,'c$u$uAttribute'))))).
% 76.02/14.74 fof(antonymPattern10048, conjecture, ! [X0] : ! [X1] : ((('p$u$ud$u$uinstance'(X1,'c$u$uObject') & 'p$u$ud$u$uinstance'(X0,'c$u$uObject')) => (('p$u$uattribute'(X1,'c$u$uGas') & 'p$u$uattribute'(X0,'c$u$uLiquid')) => X0 != X1)))).
% 76.02/14.74 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('p$u$ud$u$uinstance'(X1,'c$u$uObject') & 'p$u$ud$u$uinstance'(X0,'c$u$uObject')) => (('p$u$uattribute'(X1,'c$u$uGas') & 'p$u$uattribute'(X0,'c$u$uLiquid')) => X0 != X1))), inference(negate_conjecture, [status(cth)], [antonymPattern10048])).
% 76.02/14.74 cnf(c1, plain, ~'p$u$ud$u$usubclass'(X0,X1) | ~'p$u$ud$u$usubclass'(X1,X2) | 'p$u$ud$u$usubclass'(X0,X2), inference(clausification, [status(esa)], [predefinitionsA8])).
% 76.02/14.74 cnf(c3, plain, ~'p$u$ud$u$uinstance'(X0,X1) | ~'p$u$ud$u$usubclass'(X1,X2) | 'p$u$ud$u$uinstance'(X0,X2), inference(clausification, [status(esa)], [predefinitionsA12])).
% 76.02/14.74 cnf(c9, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uAttribute') | X1(X2,X3,X0,X4) | ~'p$u$ud$u$uinstance'(X4,'c$u$uAttribute') | ~'p$u$ucontraryAttribute4'(X2,X3,X0,X4) | ~'p$u$ud$u$uinstance'(X3,'c$u$uAttribute') | ~'p$u$ud$u$uinstance'(X2,'c$u$uAttribute'), inference(clausification, [status(esa)], [mergeA90])).
% 76.02/14.74 cnf(c36, plain, ~X0(X1,X2) | ~'p$u$ud$u$uinstance'(X3,'c$u$uObject') | ~'p$u$uattribute'(X3,X1) | ~'p$u$uattribute'(X3,X2), inference(clausification, [status(esa)], [mergeA90])).
% 76.02/14.74 cnf(c70, plain, ~X0(X1,X2,X3,X4) | X5(X2,X3), inference(clausification, [status(esa)], [mergeA90])).
% 76.02/14.74 cnf(c122, plain, 'p$u$ud$u$usubclass'('c$u$uInternalAttribute','c$u$uAttribute'), inference(clausification, [status(esa)], [mergeA351])).
% 76.02/14.74 cnf(c245, plain, 'p$u$ud$u$usubclass'('c$u$uPhysicalState','c$u$uInternalAttribute'), inference(clausification, [status(esa)], [mergeA3560])).
% 76.02/14.74 cnf(c246, plain, 'p$u$ucontraryAttribute4'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(clausification, [status(esa)], [mergeA3561])).
% 76.02/14.74 cnf(c247, plain, 'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uPhysicalState'), inference(clausification, [status(esa)], [mergeA3563])).
% 76.02/14.74 cnf(c250, plain, 'p$u$usubAttribute'('c$u$uLiquid','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3566])).
% 76.02/14.74 cnf(c253, plain, 'p$u$usubAttribute'('c$u$uGas','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3569])).
% 76.02/14.74 cnf(c258, plain, 'p$u$usubAttribute'('c$u$uPlasma','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3572])).
% 76.02/14.74 cnf(c463, plain, ~'p$u$usubAttribute'(X0,X1) | 'p$u$ud$u$uinstance'(X0,'c$u$uAttribute'), inference(clausification, [status(esa)], [typeA2])).
% 76.02/14.74 cnf(c498, plain, 'p$u$ud$u$uinstance'(sK384,'c$u$uObject'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.02/14.74 cnf(c500, plain, 'p$u$uattribute'(sK384,'c$u$uGas'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.02/14.74 cnf(c501, plain, 'p$u$uattribute'(sK383,'c$u$uLiquid'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.02/14.74 cnf(c502, plain, sK383 = sK384, inference(clausification, [status(esa)], [negated_conjecture])).
% 76.02/14.74 cnf(d0, plain, ~'p$u$ud$u$uinstance'('c$u$uPlasma','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uGas','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uLiquid','c$u$uAttribute') | 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [c246,c9])).
% 76.02/14.74 cnf(d1, plain, 'p$u$ud$u$uinstance'('c$u$uGas','c$u$uAttribute'), inference(resolution, [status(thm)], [c463,c253])).
% 76.02/14.74 cnf(d2, plain, ~'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uLiquid','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uPlasma','c$u$uAttribute') | 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [d1,d0])).
% 76.02/14.74 cnf(d3, plain, 'p$u$ud$u$uinstance'('c$u$uPlasma','c$u$uAttribute'), inference(resolution, [status(thm)], [c463,c258])).
% 76.02/14.74 cnf(d4, plain, ~'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uLiquid','c$u$uAttribute') | 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [d3,d2])).
% 76.02/14.74 cnf(d5, plain, 'p$u$ud$u$uinstance'('c$u$uLiquid','c$u$uAttribute'), inference(resolution, [status(thm)], [c463,c250])).
% 76.02/14.74 cnf(d6, plain, ~'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute') | 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [d5,d4])).
% 76.02/14.74 cnf(d7, plain, 'p$u$ud$u$usubclass'(X0,'c$u$uAttribute') | ~'p$u$ud$u$usubclass'(X0,'c$u$uInternalAttribute'), inference(resolution, [status(thm)], [c122,c1])).
% 76.02/14.74 cnf(d8, plain, 'p$u$ud$u$usubclass'('c$u$uPhysicalState','c$u$uAttribute'), inference(resolution, [status(thm)], [d7,c245])).
% 76.02/14.74 cnf(d9, plain, ~'p$u$ud$u$usubclass'('c$u$uPhysicalState',X0) | 'p$u$ud$u$uinstance'('c$u$uSolid',X0), inference(resolution, [status(thm)], [c247,c3])).
% 76.02/14.74 cnf(d10, plain, 'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute'), inference(resolution, [status(thm)], [d9,d8])).
% 76.02/14.74 cnf(d11, plain, 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [d10,d6])).
% 76.02/14.74 cnf(d12, plain, 'Ts19'('c$u$uLiquid','c$u$uGas'), inference(resolution, [status(thm)], [d11,c70])).
% 76.02/14.74 cnf(d13, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uObject') | ~'p$u$uattribute'(X0,'c$u$uLiquid') | ~'p$u$uattribute'(X0,'c$u$uGas'), inference(resolution, [status(thm)], [d12,c36])).
% 76.02/14.74 cnf(d14, plain, ~'p$u$ud$u$uinstance'(sK384,'c$u$uObject') | ~'p$u$uattribute'(sK384,'c$u$uLiquid'), inference(resolution, [status(thm)], [d13,c500])).
% 76.02/14.74 cnf(d15, plain, ~'p$u$uattribute'(sK384,'c$u$uLiquid'), inference(resolution, [status(thm)], [c498,d14])).
% 76.02/14.74 cnf(d16, plain, 'p$u$uattribute'(sK384,'c$u$uLiquid'), inference(demodulation, [status(thm)], [c501,c502])).
% 76.02/14.74 cnf(d17, plain, $false, inference(resolution, [status(thm)], [d16,d15])).
% 76.02/14.74 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------