%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR191+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:06 AM UTC 2026
% Result : Theorem 76.17s 19.04s
% Output : CNFRefutation 76.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR191+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.40 % Computer : n018.cluster.edu
% 0.10/0.40 % Model : x86_64 x86_64
% 0.10/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.40 % Memory : 8046.5625MB
% 0.10/0.40 % OS : Linux 6.8.0-71-generic
% 0.10/0.40 % CPULimit : 300
% 0.10/0.40 % WCLimit : 300
% 0.10/0.40 % DateTime : Sun Sep 27 01:31:08 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.10/0.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 76.17/19.04 % SZS status Theorem for theBenchmark.p
% 76.17/19.04 % SZS output start CNFRefutation for theBenchmark.p
% 76.17/19.04 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.17/19.04 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.17/19.04 fof(mergeA182, axiom, 'p$u$ud$u$usubclass'('c$u$uSelfConnectedObject','c$u$uObject')).
% 76.17/19.04 fof(mergeA226, axiom, 'p$u$ud$u$usubclass'('c$u$uSubstance','c$u$uSelfConnectedObject')).
% 76.17/19.04 fof(mergeA2894, axiom, 'p$u$ud$u$usubclass'('c$u$uMineral','c$u$uSubstance')).
% 76.17/19.04 fof(mergeA3561, axiom, 'p$u$ucontraryAttribute4'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma')).
% 76.17/19.04 fof(mergeA3566, axiom, 'p$u$usubAttribute'('c$u$uLiquid','c$u$uFluid')).
% 76.17/19.04 fof(mergeA3567, axiom, ! [X0] : (('p$u$ud$u$uinstance'(X0,'c$u$uSolution') => 'p$u$uattribute'(X0,'c$u$uLiquid')))).
% 76.17/19.04 fof(mergeA3569, axiom, 'p$u$usubAttribute'('c$u$uGas','c$u$uFluid')).
% 76.17/19.04 fof(mergeA3572, axiom, 'p$u$usubAttribute'('c$u$uPlasma','c$u$uFluid')).
% 76.17/19.04 fof(miloA258, axiom, 'p$u$ud$u$usubclass'('c$u$uPetroleumProduct','c$u$uOil')).
% 76.17/19.04 fof(miloA261, axiom, 'p$u$ud$u$usubclass'('c$u$uFossilFuel','c$u$uPetroleumProduct')).
% 76.17/19.04 fof(miloA1360, axiom, 'p$u$ud$u$usubclass'('c$u$uOil','c$u$uSolution')).
% 76.17/19.04 fof(miloA2590, axiom, ! [X0] : (('p$u$ud$u$uinstance'(X0,'c$u$uRock') => 'p$u$uattribute'(X0,'c$u$uSolid')))).
% 76.17/19.04 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.17/19.04 fof(typeA68, axiom, ! [X0] : ! [X1] : (('p$u$uattribute'(X0,X1) => ('p$u$ud$u$uinstance'(X1,'c$u$uAttribute') & 'p$u$ud$u$uinstance'(X0,'c$u$uObject'))))).
% 76.17/19.04 fof(negatedMultipleMapping0150, conjecture, ~? [X0] : (('p$u$ud$u$uinstance'(X0,'c$u$uFossilFuel') & ('p$u$ud$u$uinstance'(X0,'c$u$uMineral') & 'p$u$ud$u$uinstance'(X0,'c$u$uRock'))))).
% 76.17/19.04 fof(negated_conjecture, negated_conjecture, ~~? [X0] : (('p$u$ud$u$uinstance'(X0,'c$u$uFossilFuel') & ('p$u$ud$u$uinstance'(X0,'c$u$uMineral') & 'p$u$ud$u$uinstance'(X0,'c$u$uRock')))), inference(negate_conjecture, [status(cth)], [negatedMultipleMapping0150])).
% 76.17/19.04 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.17/19.04 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.17/19.04 cnf(c60, 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.17/19.04 cnf(c64, plain, ~X0(X1,X2,X3,X4) | X5(X1,X2), inference(clausification, [status(esa)], [mergeA90])).
% 76.17/19.04 cnf(c82, plain, 'p$u$ud$u$usubclass'('c$u$uSelfConnectedObject','c$u$uObject'), inference(clausification, [status(esa)], [mergeA182])).
% 76.17/19.04 cnf(c83, plain, 'p$u$ud$u$usubclass'('c$u$uSubstance','c$u$uSelfConnectedObject'), inference(clausification, [status(esa)], [mergeA226])).
% 76.17/19.04 cnf(c145, plain, 'p$u$ud$u$usubclass'('c$u$uMineral','c$u$uSubstance'), inference(clausification, [status(esa)], [mergeA2894])).
% 76.17/19.04 cnf(c169, plain, 'p$u$ucontraryAttribute4'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(clausification, [status(esa)], [mergeA3561])).
% 76.17/19.04 cnf(c173, plain, 'p$u$usubAttribute'('c$u$uLiquid','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3566])).
% 76.17/19.04 cnf(c174, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uSolution') | 'p$u$uattribute'(X0,'c$u$uLiquid'), inference(clausification, [status(esa)], [mergeA3567])).
% 76.17/19.04 cnf(c176, plain, 'p$u$usubAttribute'('c$u$uGas','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3569])).
% 76.17/19.04 cnf(c181, plain, 'p$u$usubAttribute'('c$u$uPlasma','c$u$uFluid'), inference(clausification, [status(esa)], [mergeA3572])).
% 76.17/19.04 cnf(c183, plain, 'p$u$ud$u$usubclass'('c$u$uPetroleumProduct','c$u$uOil'), inference(clausification, [status(esa)], [miloA258])).
% 76.17/19.04 cnf(c186, plain, 'p$u$ud$u$usubclass'('c$u$uFossilFuel','c$u$uPetroleumProduct'), inference(clausification, [status(esa)], [miloA261])).
% 76.17/19.04 cnf(c224, plain, 'p$u$ud$u$usubclass'('c$u$uOil','c$u$uSolution'), inference(clausification, [status(esa)], [miloA1360])).
% 76.17/19.04 cnf(c246, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uRock') | 'p$u$uattribute'(X0,'c$u$uSolid'), inference(clausification, [status(esa)], [miloA2590])).
% 76.17/19.04 cnf(c301, plain, ~'p$u$usubAttribute'(X0,X1) | 'p$u$ud$u$uinstance'(X0,'c$u$uAttribute'), inference(clausification, [status(esa)], [typeA2])).
% 76.17/19.04 cnf(c309, plain, ~'p$u$uattribute'(X0,X1) | 'p$u$ud$u$uinstance'(X1,'c$u$uAttribute'), inference(clausification, [status(esa)], [typeA68])).
% 76.17/19.04 cnf(c325, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uFossilFuel'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.17/19.04 cnf(c326, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uMineral'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.17/19.04 cnf(c327, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uRock'), inference(clausification, [status(esa)], [negated_conjecture])).
% 76.17/19.04 cnf(d0, plain, ~'p$u$ud$u$usubclass'('c$u$uFossilFuel',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [c3,c325])).
% 76.17/19.04 cnf(d1, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uPetroleumProduct'), inference(resolution, [status(thm)], [c186,d0])).
% 76.17/19.04 cnf(d2, plain, ~'p$u$ud$u$usubclass'('c$u$uPetroleumProduct',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [d1,c3])).
% 76.17/19.04 cnf(d3, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uOil'), inference(resolution, [status(thm)], [d2,c183])).
% 76.17/19.04 cnf(d4, plain, ~'p$u$ud$u$usubclass'('c$u$uOil',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [d3,c3])).
% 76.17/19.04 cnf(d5, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uSolution'), inference(resolution, [status(thm)], [c224,d4])).
% 76.17/19.04 cnf(d6, plain, 'p$u$uattribute'(sK226,'c$u$uLiquid'), inference(resolution, [status(thm)], [c174,d5])).
% 76.17/19.04 cnf(d7, 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)], [c169,c9])).
% 76.17/19.04 cnf(d8, plain, 'p$u$ud$u$uinstance'('c$u$uGas','c$u$uAttribute'), inference(resolution, [status(thm)], [c301,c176])).
% 76.17/19.04 cnf(d9, 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)], [d8,d7])).
% 76.17/19.04 cnf(d10, plain, 'p$u$ud$u$uinstance'('c$u$uPlasma','c$u$uAttribute'), inference(resolution, [status(thm)], [c301,c181])).
% 76.17/19.04 cnf(d11, 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)], [d10,d9])).
% 76.17/19.04 cnf(d12, plain, 'p$u$ud$u$uinstance'('c$u$uLiquid','c$u$uAttribute'), inference(resolution, [status(thm)], [c301,c173])).
% 76.17/19.04 cnf(d13, 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)], [d12,d11])).
% 76.17/19.04 cnf(d14, plain, 'p$u$uattribute'(sK226,'c$u$uSolid'), inference(resolution, [status(thm)], [c246,c327])).
% 76.17/19.04 cnf(d15, plain, 'p$u$ud$u$uinstance'('c$u$uSolid','c$u$uAttribute'), inference(resolution, [status(thm)], [c309,d14])).
% 76.17/19.04 cnf(d16, plain, 'Ts26'('c$u$uSolid','c$u$uLiquid','c$u$uGas','c$u$uPlasma'), inference(resolution, [status(thm)], [d15,d13])).
% 76.17/19.04 cnf(d17, plain, 'Ts25'('c$u$uSolid','c$u$uLiquid'), inference(resolution, [status(thm)], [d16,c64])).
% 76.17/19.04 cnf(d18, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uObject') | ~'p$u$uattribute'(X0,'c$u$uLiquid') | ~'p$u$uattribute'(X0,'c$u$uSolid'), inference(resolution, [status(thm)], [d17,c60])).
% 76.17/19.04 cnf(d19, plain, ~'p$u$ud$u$uinstance'(sK226,'c$u$uObject') | ~'p$u$uattribute'(sK226,'c$u$uSolid'), inference(resolution, [status(thm)], [d18,d6])).
% 76.17/19.04 cnf(d20, plain, ~'p$u$ud$u$usubclass'('c$u$uMineral',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [c3,c326])).
% 76.17/19.04 cnf(d21, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uSubstance'), inference(resolution, [status(thm)], [c145,d20])).
% 76.17/19.04 cnf(d22, plain, ~'p$u$ud$u$usubclass'('c$u$uSubstance',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [d21,c3])).
% 76.17/19.04 cnf(d23, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uSelfConnectedObject'), inference(resolution, [status(thm)], [d22,c83])).
% 76.17/19.04 cnf(d24, plain, ~'p$u$ud$u$usubclass'('c$u$uSelfConnectedObject',X0) | 'p$u$ud$u$uinstance'(sK226,X0), inference(resolution, [status(thm)], [d23,c3])).
% 76.17/19.04 cnf(d25, plain, 'p$u$ud$u$uinstance'(sK226,'c$u$uObject'), inference(resolution, [status(thm)], [d24,c82])).
% 76.17/19.04 cnf(d26, plain, ~'p$u$uattribute'(sK226,'c$u$uSolid'), inference(resolution, [status(thm)], [d25,d19])).
% 76.17/19.04 cnf(d27, plain, $false, inference(resolution, [status(thm)], [d14,d26])).
% 76.17/19.04 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------