%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR215+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 : n006.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:07 AM UTC 2026
% Result : Theorem 56.22s 9.86s
% Output : CNFRefutation 56.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR215+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.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 01:32:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.22/9.86 % SZS status Theorem for theBenchmark.p
% 56.22/9.86 % SZS output start CNFRefutation for theBenchmark.p
% 56.22/9.86 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)))).
% 56.22/9.86 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)))).
% 56.22/9.86 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))))))))))))))))))).
% 56.22/9.86 fof(mergeA353, axiom, 'p$u$ud$u$usubclass'('c$u$uRelationalAttribute','c$u$uAttribute')).
% 56.22/9.86 fof(mergeA3437, axiom, 'p$u$ud$u$usubclass'('c$u$uPositionalAttribute','c$u$uRelationalAttribute')).
% 56.22/9.86 fof(mergeA3438, axiom, 'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute','c$u$uPositionalAttribute')).
% 56.22/9.86 fof(mergeA3441, axiom, 'p$u$ucontraryAttribute4'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest')).
% 56.22/9.86 fof(mergeA3444, axiom, 'p$u$ud$u$uinstance'('c$u$uEast','c$u$uDirectionalAttribute')).
% 56.22/9.86 fof(mergeA3445, axiom, 'p$u$ud$u$uinstance'('c$u$uWest','c$u$uDirectionalAttribute')).
% 56.22/9.86 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'))))).
% 56.22/9.86 fof(antonymPattern10007, conjecture, ! [X0] : ! [X1] : ((('p$u$ud$u$uinstance'(X0,'c$u$uObject') & 'p$u$ud$u$uinstance'(X1,'c$u$uObject')) => (('p$u$uattribute'(X0,'c$u$uNorth') & 'p$u$uattribute'(X1,'c$u$uSouth')) => X0 != X1)))).
% 56.22/9.86 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('p$u$ud$u$uinstance'(X0,'c$u$uObject') & 'p$u$ud$u$uinstance'(X1,'c$u$uObject')) => (('p$u$uattribute'(X0,'c$u$uNorth') & 'p$u$uattribute'(X1,'c$u$uSouth')) => X0 != X1))), inference(negate_conjecture, [status(cth)], [antonymPattern10007])).
% 56.22/9.86 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])).
% 56.22/9.86 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])).
% 56.22/9.86 cnf(c6, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uAttribute') | ~'p$u$ud$u$uinstance'(X1,'c$u$uAttribute') | ~'p$u$ucontraryAttribute4'(X2,X0,X1,X3) | ~'p$u$ud$u$uinstance'(X3,'c$u$uAttribute') | X4(X2,X0,X1,X3) | ~'p$u$ud$u$uinstance'(X2,'c$u$uAttribute'), inference(clausification, [status(esa)], [mergeA90])).
% 56.22/9.86 cnf(c53, plain, ~X0(X1,X2) | ~'p$u$ud$u$uinstance'(X3,'c$u$uObject') | ~'p$u$uattribute'(X3,X2) | ~'p$u$uattribute'(X3,X1), inference(clausification, [status(esa)], [mergeA90])).
% 56.22/9.86 cnf(c62, plain, ~X0(X1,X2,X3,X4) | X5(X1,X2), inference(clausification, [status(esa)], [mergeA90])).
% 56.22/9.86 cnf(c78, plain, 'p$u$ud$u$usubclass'('c$u$uRelationalAttribute','c$u$uAttribute'), inference(clausification, [status(esa)], [mergeA353])).
% 56.22/9.86 cnf(c90, plain, 'p$u$ud$u$usubclass'('c$u$uPositionalAttribute','c$u$uRelationalAttribute'), inference(clausification, [status(esa)], [mergeA3437])).
% 56.22/9.86 cnf(c91, plain, 'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute','c$u$uPositionalAttribute'), inference(clausification, [status(esa)], [mergeA3438])).
% 56.22/9.86 cnf(c94, plain, 'p$u$ucontraryAttribute4'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(clausification, [status(esa)], [mergeA3441])).
% 56.22/9.86 cnf(c98, plain, 'p$u$ud$u$uinstance'('c$u$uEast','c$u$uDirectionalAttribute'), inference(clausification, [status(esa)], [mergeA3444])).
% 56.22/9.86 cnf(c99, plain, 'p$u$ud$u$uinstance'('c$u$uWest','c$u$uDirectionalAttribute'), inference(clausification, [status(esa)], [mergeA3445])).
% 56.22/9.86 cnf(c117, plain, ~'p$u$uattribute'(X0,X1) | 'p$u$ud$u$uinstance'(X1,'c$u$uAttribute'), inference(clausification, [status(esa)], [typeA68])).
% 56.22/9.86 cnf(c125, plain, 'p$u$ud$u$uinstance'(sK112,'c$u$uObject'), inference(clausification, [status(esa)], [negated_conjecture])).
% 56.22/9.86 cnf(c127, plain, 'p$u$uattribute'(sK112,'c$u$uNorth'), inference(clausification, [status(esa)], [negated_conjecture])).
% 56.22/9.86 cnf(c128, plain, 'p$u$uattribute'(sK113,'c$u$uSouth'), inference(clausification, [status(esa)], [negated_conjecture])).
% 56.22/9.86 cnf(c129, plain, sK112 = sK113, inference(clausification, [status(esa)], [negated_conjecture])).
% 56.22/9.86 cnf(d0, plain, 'p$u$uattribute'(sK112,'c$u$uSouth'), inference(demodulation, [status(thm)], [c128,c129])).
% 56.22/9.86 cnf(d1, plain, ~'p$u$ud$u$uinstance'('c$u$uWest','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uEast','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uSouth','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uNorth','c$u$uAttribute') | 'Ts22'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(resolution, [status(thm)], [c94,c6])).
% 56.22/9.86 cnf(d2, plain, 'p$u$ud$u$uinstance'('c$u$uNorth','c$u$uAttribute'), inference(resolution, [status(thm)], [c117,c127])).
% 56.22/9.86 cnf(d3, plain, ~'p$u$ud$u$uinstance'('c$u$uSouth','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uEast','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uWest','c$u$uAttribute') | 'Ts22'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(resolution, [status(thm)], [d2,d1])).
% 56.22/9.86 cnf(d4, plain, 'p$u$ud$u$uinstance'('c$u$uSouth','c$u$uAttribute'), inference(resolution, [status(thm)], [c117,d0])).
% 56.22/9.86 cnf(d5, plain, ~'p$u$ud$u$uinstance'('c$u$uEast','c$u$uAttribute') | ~'p$u$ud$u$uinstance'('c$u$uWest','c$u$uAttribute') | 'Ts22'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(resolution, [status(thm)], [d4,d3])).
% 56.22/9.86 cnf(d6, plain, 'p$u$ud$u$usubclass'(X0,'c$u$uAttribute') | ~'p$u$ud$u$usubclass'(X0,'c$u$uRelationalAttribute'), inference(resolution, [status(thm)], [c78,c1])).
% 56.22/9.86 cnf(d7, plain, 'p$u$ud$u$usubclass'(X0,'c$u$uRelationalAttribute') | ~'p$u$ud$u$usubclass'(X0,'c$u$uPositionalAttribute'), inference(resolution, [status(thm)], [c90,c1])).
% 56.22/9.86 cnf(d8, plain, 'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute','c$u$uRelationalAttribute'), inference(resolution, [status(thm)], [d7,c91])).
% 56.22/9.86 cnf(d9, plain, 'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute','c$u$uAttribute'), inference(resolution, [status(thm)], [d8,d6])).
% 56.22/9.86 cnf(d10, plain, ~'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute',X0) | 'p$u$ud$u$uinstance'('c$u$uEast',X0), inference(resolution, [status(thm)], [c98,c3])).
% 56.22/9.86 cnf(d11, plain, 'p$u$ud$u$uinstance'('c$u$uEast','c$u$uAttribute'), inference(resolution, [status(thm)], [d10,d9])).
% 56.22/9.86 cnf(d12, plain, ~'p$u$ud$u$uinstance'('c$u$uWest','c$u$uAttribute') | 'Ts22'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(resolution, [status(thm)], [d11,d5])).
% 56.22/9.86 cnf(d13, plain, ~'p$u$ud$u$usubclass'('c$u$uDirectionalAttribute',X0) | 'p$u$ud$u$uinstance'('c$u$uWest',X0), inference(resolution, [status(thm)], [c99,c3])).
% 56.22/9.86 cnf(d14, plain, 'p$u$ud$u$uinstance'('c$u$uWest','c$u$uAttribute'), inference(resolution, [status(thm)], [d13,d9])).
% 56.22/9.86 cnf(d15, plain, 'Ts22'('c$u$uNorth','c$u$uSouth','c$u$uEast','c$u$uWest'), inference(resolution, [status(thm)], [d14,d12])).
% 56.22/9.86 cnf(d16, plain, 'Ts20'('c$u$uNorth','c$u$uSouth'), inference(resolution, [status(thm)], [d15,c62])).
% 56.22/9.86 cnf(d17, plain, ~'p$u$ud$u$uinstance'(X0,'c$u$uObject') | ~'p$u$uattribute'(X0,'c$u$uSouth') | ~'p$u$uattribute'(X0,'c$u$uNorth'), inference(resolution, [status(thm)], [d16,c53])).
% 56.22/9.86 cnf(d18, plain, ~'p$u$ud$u$uinstance'(sK112,'c$u$uObject') | ~'p$u$uattribute'(sK112,'c$u$uNorth'), inference(resolution, [status(thm)], [d17,d0])).
% 56.22/9.86 cnf(d19, plain, ~'p$u$uattribute'(sK112,'c$u$uNorth'), inference(resolution, [status(thm)], [c125,d18])).
% 56.22/9.86 cnf(d20, plain, $false, inference(resolution, [status(thm)], [c127,d19])).
% 56.22/9.86 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------