%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : COL074-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 06:56:52 AM UTC 2026
% Result : Unsatisfiable 16.55s 7.71s
% Output : CNFRefutation 16.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of clauses : 29 ( 23 unt; 5 nHn; 17 RR)
% Number of literals : 35 ( 34 equ; 4 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 21 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(k_definition,negated_conjecture,
apply(apply(k,X0),X1) = X0 ).
cnf(pairwise_application,axiom,
apply(pair(X0,X1),X2) = pair(apply(X0,X2),apply(X1,X2)) ).
cnf(equality,axiom,
apply(eq,pair(X0,X0)) = projection1 ).
cnf(extensionality1,axiom,
( apply(eq,pair(X0,X1)) = projection2
| X0 = X1 ) ).
cnf(different_projections,axiom,
projection1 != projection2 ).
cnf(k_projection2,axiom,
apply(k,projection2) = 'k$uprojection2' ).
cnf(self_referential,axiom,
s = apply(eq,pair(apply(k,s),apply(k,projection2))) ).
cnf(c0,plain,
apply(apply(k,X0),X1) = X0,
inference(clausification,[status(esa)],[k_definition]) ).
cnf(c4,plain,
apply(pair(X0,X1),X2) = pair(apply(X0,X2),apply(X1,X2)),
inference(clausification,[status(esa)],[pairwise_application]) ).
cnf(c6,plain,
apply(eq,pair(X0,X0)) = projection1,
inference(clausification,[status(esa)],[equality]) ).
cnf(c7,plain,
( apply(eq,pair(X0,X1)) = projection2
| X0 = X1 ),
inference(clausification,[status(esa)],[extensionality1]) ).
cnf(c9,plain,
projection1 != projection2,
inference(clausification,[status(esa)],[different_projections]) ).
cnf(c11,plain,
apply(k,projection2) = 'k$uprojection2',
inference(clausification,[status(esa)],[k_projection2]) ).
cnf(c12,plain,
s = apply(eq,pair(apply(k,s),apply(k,projection2))),
inference(clausification,[status(esa)],[self_referential]) ).
cnf(d0,plain,
apply(eq,apply(pair(X0,X0),X1)) = projection1,
inference(superposition,[status(thm)],[c4,c6]) ).
cnf(d1,plain,
apply(pair(X0,k),projection2) = pair(apply(X0,projection2),'k$uprojection2'),
inference(superposition,[status(thm)],[c11,c4]) ).
cnf(d2,plain,
apply('k$uprojection2',X0) = projection2,
inference(superposition,[status(thm)],[c11,c0]) ).
cnf(d3,plain,
s = apply(eq,pair(apply(k,s),'k$uprojection2')),
inference(demodulation,[status(thm)],[c12,c11]) ).
cnf(d4,plain,
( apply(k,s) = 'k$uprojection2'
| s = projection2 ),
inference(superposition,[status(thm)],[d3,c7]) ).
cnf(d5,plain,
( s = projection2
| apply('k$uprojection2',X0) = s ),
inference(superposition,[status(thm)],[d4,c0]) ).
cnf(d6,plain,
( s = projection2
| projection2 = s ),
inference(demodulation,[status(thm)],[d5,d2]) ).
cnf(d7,plain,
( s = projection2
| projection2 != projection2 ),
inference(equality_factoring,[status(thm)],[d6]) ).
cnf(d8,plain,
s = projection2,
inference(equality_resolution,[status(thm)],[d7]) ).
cnf(d9,plain,
projection2 = apply(eq,pair(apply(k,s),'k$uprojection2')),
inference(demodulation,[status(thm)],[d3,d8]) ).
cnf(d10,plain,
projection2 = apply(eq,pair(apply(k,projection2),'k$uprojection2')),
inference(demodulation,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
projection2 = apply(eq,apply(pair(k,k),projection2)),
inference(demodulation,[status(thm)],[d10,d1]) ).
cnf(d12,plain,
projection2 = projection1,
inference(demodulation,[status(thm)],[d11,d0]) ).
cnf(d13,plain,
projection2 != projection2,
inference(demodulation,[status(thm)],[c9,d12]) ).
cnf(d14,plain,
$false,
inference(equality_resolution,[status(thm)],[d13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL074-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.59 % Computer : n010.cluster.edu
% 0.12/5.59 % Model : x86_64 x86_64
% 0.12/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.59 % Memory : 8046.5625MB
% 0.12/5.59 % OS : Linux 6.8.0-71-generic
% 0.12/5.59 % CPULimit : 300
% 0.12/5.59 % WCLimit : 300
% 0.12/5.59 % DateTime : Sat Sep 26 23:12:06 UTC 2026
% 0.12/5.59 % CPUTime :
% 0.12/5.59 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.55/7.71 % SZS status Unsatisfiable for theBenchmark.p
% 16.55/7.71 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------