%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : COL006-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:12:01 PM UTC 2026
% Result : Unsatisfiable 283.59s 104.57s
% Output : CNFRefutation 283.99s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_194)
% Comments :
%------------------------------------------------------------------------------
cnf(s_definition,axiom,
apply(apply(apply(s,X1),X2),X3) = apply(apply(X1,X3),apply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s_definition) ).
cnf(prove_fixed_point,negated_conjecture,
apply(X1,f(X1)) != apply(f(X1),apply(X1,f(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_fixed_point) ).
cnf(k_definition,axiom,
apply(apply(k,X1),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_definition) ).
cnf(i_0_3,axiom,
apply(apply(apply(s,X1),X2),X3) = apply(apply(X1,X3),apply(X2,X3)),
s_definition,
[final] ).
cnf(i_0_4,negated_conjecture,
apply(X1,f(X1)) != apply(f(X1),apply(X1,f(X1))),
prove_fixed_point,
[final] ).
cnf(i_0_5,axiom,
apply(apply(k,X1),X2) = X1,
k_definition,
[final] ).
cnf(i_0_6,axiom,
X1 = X1 ).
cnf(i_0_7,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_8,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_9,axiom,
( X1 != X2
| apply(X1,X3) = apply(X2,X3) ) ).
cnf(i_0_10,axiom,
( X1 != X2
| apply(X3,X1) = apply(X3,X2) ) ).
cnf(i_0_196,plain,
apply(apply(s,apply(apply(k,s),X1)),apply(apply(k,X2),X3)) != X2,
inference(scs_inference,[],[i_0_194,i_0_7]) ).
cnf(i_0_197,plain,
apply(apply(s,s),apply(apply(k,X1),X2)) != apply(apply(apply(s,apply(s,k)),apply(k,X1)),X3),
inference(scs_inference,[],[i_0_148,i_0_194,i_0_126,i_0_7,i_0_8]) ).
cnf(i_0_199,plain,
apply(apply(apply(s,apply(s,k)),apply(k,X1)),X2) != apply(apply(s,s),apply(apply(k,X1),X3)),
inference(scs_inference,[],[i_0_197,i_0_7]) ).
cnf(i_0_200,plain,
apply(apply(s,s),X1) != apply(apply(apply(s,k),X2),X1),
inference(scs_inference,[],[i_0_170,i_0_197,i_0_155,i_0_7,i_0_8]) ).
cnf(i_0_258,plain,
apply(apply(s,apply(apply(k,s),X1)),apply(apply(k,X2),X3)) != X2,
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_203,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(s,s),X2),
inference(scs_inference,[],[i_0_200,i_0_7]) ).
cnf(i_0_204,plain,
apply(apply(k,apply(apply(s,s),X1)),X2) != apply(apply(apply(s,k),X3),X1),
inference(scs_inference,[],[i_0_11,i_0_200,i_0_7,i_0_8]) ).
cnf(i_0_206,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(k,apply(apply(s,s),X2)),X3),
inference(scs_inference,[],[i_0_204,i_0_7]) ).
cnf(i_0_207,plain,
apply(apply(k,X1),X2) != apply(apply(apply(s,k),X3),apply(apply(s,s),apply(k,apply(X1,s)))),
inference(scs_inference,[],[i_0_11,i_0_160,i_0_204,i_0_7,i_0_8]) ).
cnf(i_0_443,plain,
apply(apply(apply(s,k),X1),apply(apply(k,X2),X3)) != apply(apply(s,s),X2),
inference(scs_inference,[],[i_0_35,i_0_203,i_0_8]) ).
cnf(i_0_444,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(s,s),X2),
inference(rename_variables,[],[i_0_203]) ).
cnf(i_0_209,plain,
apply(apply(apply(s,k),X1),apply(apply(s,s),apply(k,apply(X2,s)))) != apply(apply(k,X2),X3),
inference(scs_inference,[],[i_0_207,i_0_7]) ).
cnf(i_0_210,plain,
apply(apply(apply(s,k),X1),apply(apply(apply(s,k),X2),X3)) != apply(apply(s,s),X3),
inference(scs_inference,[],[i_0_203,i_0_182,i_0_207,i_0_7,i_0_8]) ).
cnf(i_0_445,plain,
apply(apply(s,s),X1) != apply(apply(apply(s,k),X2),apply(apply(k,X1),X3)),
inference(scs_inference,[],[i_0_443,i_0_7]) ).
cnf(i_0_212,plain,
apply(apply(s,s),X1) != apply(apply(apply(s,k),X2),apply(apply(apply(s,k),X3),X1)),
inference(scs_inference,[],[i_0_210,i_0_7]) ).
cnf(i_0_213,plain,
apply(apply(k,apply(apply(s,s),X1)),X2) != apply(apply(k,X1),X3),
inference(scs_inference,[],[i_0_11,i_0_210,i_0_139,i_0_7,i_0_8]) ).
cnf(i_0_446,plain,
apply(apply(s,s),apply(apply(k,X1),X2)) != apply(apply(apply(s,k),X3),apply(apply(k,X1),X4)),
inference(scs_inference,[],[i_0_445,i_0_126,i_0_8]) ).
cnf(i_0_215,plain,
apply(apply(k,X1),X2) != apply(apply(k,apply(apply(s,s),X1)),X3),
inference(scs_inference,[],[i_0_213,i_0_7]) ).
cnf(i_0_216,plain,
apply(apply(s,s),X1) != apply(apply(apply(s,k),X2),apply(apply(k,X1),X2)),
inference(scs_inference,[],[i_0_94,i_0_133,i_0_213,i_0_7,i_0_8]) ).
cnf(i_0_219,plain,
apply(apply(apply(s,k),X1),apply(apply(k,X2),X1)) != apply(apply(s,s),X2),
inference(scs_inference,[],[i_0_216,i_0_7]) ).
cnf(i_0_220,plain,
apply(apply(k,apply(apply(k,X1),X2)),X3) != apply(apply(s,s),X1),
inference(scs_inference,[],[i_0_11,i_0_216,i_0_144,i_0_7,i_0_8]) ).
cnf(i_0_222,plain,
apply(apply(s,s),X1) != apply(apply(k,apply(apply(k,X1),X2)),X3),
inference(scs_inference,[],[i_0_220,i_0_7]) ).
cnf(i_0_223,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(s,s),apply(apply(k,X2),X3)),
inference(scs_inference,[],[i_0_220,i_0_74,i_0_199,i_0_7,i_0_8]) ).
cnf(i_0_225,plain,
apply(apply(s,s),apply(apply(k,X1),X2)) != apply(apply(apply(s,k),X3),X1),
inference(scs_inference,[],[i_0_223,i_0_7]) ).
cnf(i_0_226,plain,
apply(apply(k,X1),X2) != apply(apply(s,s),apply(k,apply(X1,s))),
inference(scs_inference,[],[i_0_11,i_0_223,i_0_90,i_0_7,i_0_8]) ).
cnf(i_0_228,plain,
apply(apply(s,s),apply(k,apply(X1,s))) != apply(apply(k,X1),X2),
inference(scs_inference,[],[i_0_226,i_0_7]) ).
cnf(i_0_229,plain,
apply(apply(k,apply(apply(k,X1),X2)),X3) != apply(apply(s,s),apply(k,apply(X1,s))),
inference(scs_inference,[],[i_0_11,i_0_226,i_0_7,i_0_8]) ).
cnf(i_0_246,plain,
apply(apply(s,s),apply(apply(k,X1),X2)) != apply(apply(apply(s,k),X3),X1),
inference(rename_variables,[],[i_0_225]) ).
cnf(i_0_231,plain,
apply(apply(s,s),apply(k,apply(X1,s))) != apply(apply(k,apply(apply(k,X1),X2)),X3),
inference(scs_inference,[],[i_0_229,i_0_7]) ).
cnf(i_0_232,plain,
apply(apply(k,X1),X2) != apply(k,apply(apply(s,s),apply(X1,X3))),
inference(scs_inference,[],[i_0_11,i_0_229,i_0_82,i_0_7,i_0_8]) ).
cnf(i_0_234,plain,
apply(k,apply(apply(s,s),apply(X1,X2))) != apply(apply(k,X1),X3),
inference(scs_inference,[],[i_0_232,i_0_7]) ).
cnf(i_0_235,plain,
apply(apply(apply(apply(s,k),X1),apply(s,s)),apply(k,apply(X2,s))) != apply(apply(k,X2),X3),
inference(scs_inference,[],[i_0_228,i_0_232,i_0_183,i_0_7,i_0_8]) ).
cnf(i_0_386,plain,
apply(apply(apply(s,k),X1),X2) != apply(k,apply(apply(s,s),apply(X2,X3))),
inference(scs_inference,[],[i_0_18,i_0_232,i_0_8]) ).
cnf(i_0_387,plain,
apply(apply(k,X1),X2) != apply(k,apply(apply(s,s),apply(X1,X3))),
inference(rename_variables,[],[i_0_232]) ).
cnf(i_0_237,plain,
apply(apply(k,X1),X2) != apply(apply(apply(apply(s,k),X3),apply(s,s)),apply(k,apply(X1,s))),
inference(scs_inference,[],[i_0_235,i_0_7]) ).
cnf(i_0_238,plain,
apply(apply(apply(s,apply(apply(s,k),X1)),k),apply(s,s)) != apply(apply(k,s),X2),
inference(scs_inference,[],[i_0_12,i_0_235,i_0_7,i_0_8]) ).
cnf(i_0_239,plain,
apply(apply(apply(apply(s,k),X1),apply(s,s)),apply(k,apply(X2,s))) != apply(apply(k,X2),X3),
inference(rename_variables,[],[i_0_235]) ).
cnf(i_0_389,plain,
apply(apply(k,apply(apply(k,X1),X2)),X3) != apply(k,apply(apply(s,s),apply(X1,X4))),
inference(scs_inference,[],[i_0_386,i_0_69,i_0_8]) ).
cnf(i_0_241,plain,
apply(apply(k,s),X1) != apply(apply(apply(s,apply(apply(s,k),X2)),k),apply(s,s)),
inference(scs_inference,[],[i_0_238,i_0_7]) ).
cnf(i_0_242,plain,
apply(k,apply(apply(apply(k,apply(s,s)),X1),apply(X2,X3))) != apply(apply(k,X2),X4),
inference(scs_inference,[],[i_0_234,i_0_136,i_0_238,i_0_7,i_0_8]) ).
cnf(i_0_253,plain,
apply(apply(k,X1),X2) != apply(apply(apply(apply(s,k),X3),apply(s,s)),apply(k,apply(X1,s))),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_424,plain,
apply(apply(k,X1),X2) != apply(apply(apply(apply(s,k),X3),apply(s,s)),apply(k,apply(X1,s))),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_441,plain,
apply(apply(k,X1),X2) != apply(apply(apply(apply(s,k),X3),apply(s,s)),apply(k,apply(X1,s))),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_244,plain,
apply(apply(k,X1),X2) != apply(k,apply(apply(apply(k,apply(s,s)),X3),apply(X1,X4))),
inference(scs_inference,[],[i_0_242,i_0_7]) ).
cnf(i_0_245,plain,
apply(apply(apply(s,s),apply(k,X1)),s) != apply(apply(apply(s,k),X2),X1),
inference(scs_inference,[],[i_0_12,i_0_225,i_0_242,i_0_7,i_0_8]) ).
cnf(i_0_248,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(apply(s,s),apply(k,X2)),s),
inference(scs_inference,[],[i_0_245,i_0_7]) ).
cnf(i_0_249,plain,
apply(apply(apply(s,k),X1),apply(apply(k,X2),apply(apply(k,X1),X3))) != apply(apply(s,s),X2),
inference(scs_inference,[],[i_0_219,i_0_245,i_0_131,i_0_7,i_0_8]) ).
cnf(i_0_269,plain,
apply(apply(k,X1),X2) != apply(k,apply(apply(apply(k,apply(s,s)),X3),apply(X1,X4))),
inference(rename_variables,[],[i_0_244]) ).
cnf(i_0_251,plain,
apply(apply(s,s),X1) != apply(apply(apply(s,k),X2),apply(apply(k,X1),apply(apply(k,X2),X3))),
inference(scs_inference,[],[i_0_249,i_0_7]) ).
cnf(i_0_252,plain,
apply(apply(apply(s,k),X1),X2) != apply(apply(apply(apply(s,k),X3),apply(s,s)),apply(k,apply(X2,s))),
inference(scs_inference,[],[i_0_12,i_0_237,i_0_249,i_0_7,i_0_8]) ).
cnf(i_0_255,plain,
apply(apply(apply(apply(s,k),X1),apply(s,s)),apply(k,apply(X2,s))) != apply(apply(apply(s,k),X3),X2),
inference(scs_inference,[],[i_0_252,i_0_7]) ).
cnf(i_0_256,plain,
apply(apply(apply(s,s),apply(k,X1)),apply(apply(k,s),X2)) != X1,
inference(scs_inference,[],[i_0_12,i_0_196,i_0_252,i_0_7,i_0_8]) ).
cnf(i_0_259,plain,
X1 != apply(apply(apply(s,s),apply(k,X1)),apply(apply(k,s),X2)),
inference(scs_inference,[],[i_0_256,i_0_7]) ).
cnf(i_0_260,plain,
apply(apply(apply(s,apply(s,s)),apply(k,s)),apply(k,X1)) != X1,
inference(scs_inference,[],[i_0_12,i_0_256,i_0_7,i_0_8]) ).
cnf(i_0_261,plain,
apply(apply(apply(s,s),apply(k,X1)),apply(apply(k,s),X2)) != X1,
inference(rename_variables,[],[i_0_256]) ).
cnf(i_0_315,plain,
apply(apply(apply(apply(s,k),X1),apply(s,s)),apply(k,apply(X2,s))) != apply(apply(apply(s,k),X3),X2),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_263,plain,
X1 != apply(apply(apply(s,apply(s,s)),apply(k,s)),apply(k,X1)),
inference(scs_inference,[],[i_0_260,i_0_7]) ).
cnf(i_0_264,plain,
apply(apply(apply(s,apply(s,apply(s,s))),k),apply(k,s)) != apply(k,s),
inference(scs_inference,[],[i_0_12,i_0_260,i_0_7,i_0_8]) ).
cnf(c_0_226,axiom,
apply(apply(apply(s,X1),X2),X3) = apply(apply(X1,X3),apply(X2,X3)),
i_0_3 ).
cnf(c_0_227,axiom,
apply(apply(k,X1),X2) = X1,
i_0_5 ).
cnf(c_0_228,plain,
apply(apply(s,s),X1) != apply(apply(k,apply(apply(k,X1),X2)),X3),
i_0_222 ).
cnf(c_0_229,plain,
apply(apply(apply(s,apply(k,X1)),X2),X3) = apply(X1,apply(X2,X3)),
inference(spm,[status(thm)],[c_0_226,c_0_227]) ).
cnf(c_0_230,plain,
apply(apply(s,s),X1) != X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_228,c_0_227]),c_0_227]) ).
cnf(c_0_231,plain,
apply(apply(apply(s,apply(s,apply(k,X1))),X2),X3) = apply(X1,apply(X3,apply(X2,X3))),
inference(spm,[status(thm)],[c_0_226,c_0_229]) ).
cnf(c_0_232,plain,
apply(apply(apply(s,apply(s,apply(k,apply(s,s)))),X1),X2) != apply(X2,apply(X1,X2)),
inference(spm,[status(thm)],[c_0_230,c_0_231]) ).
cnf(c_0_233,plain,
apply(apply(apply(s,k),X1),X2) = X2,
inference(spm,[status(thm)],[c_0_227,c_0_226]) ).
cnf(c_0_234,plain,
apply(apply(apply(s,apply(s,apply(k,apply(s,s)))),apply(apply(s,k),X1)),X2) != apply(X2,X2),
inference(spm,[status(thm)],[c_0_232,c_0_233]) ).
cnf(c_0_235,plain,
$false,
inference(er,[status(thm)],[c_0_234]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COL006-1 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n004.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 16:13:32 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 283.59/104.57 % Version : CSE_E---1.7
% 283.59/104.57 % Problem : theBenchmark.p
% 283.59/104.57 % SZS status Unsatisfiable for theBenchmark.p
% 283.59/104.57 % SZS output start CNFRefutation
% See solution above
% 283.99/104.95 % Total time : 100.616s
%------------------------------------------------------------------------------