%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COL074-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 12:09:05 PM UTC 2026
% Result : Unsatisfiable 0.13s 5.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL074-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n011.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Mon Sep 21 14:08:30 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 0.13/5.41 % Refutation found
% 0.13/5.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.41 fof(f1,negated_conjecture,(
% 0.13/5.41 (![X,Y]: (apply(apply(k,X),Y) = X ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f2,axiom,(
% 0.13/5.41 (![X,Y]: (apply(projection1,pair(X,Y)) = X ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f3,axiom,(
% 0.13/5.41 (![X,Y]: (apply(projection2,pair(X,Y)) = Y ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f6,negated_conjecture,(
% 0.13/5.41 (![X,Y,Z]: (apply(apply(apply(abstraction,X),Y),Z) = apply(apply(X,apply(k,Z)),apply(Y,Z)) ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f7,axiom,(
% 0.13/5.41 (![X]: (apply(eq,pair(X,X)) = projection1 ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f8,axiom,(
% 0.13/5.41 (![X,Y]: (( X = Y| apply(eq,pair(X,Y)) = projection2 ) ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f9,axiom,(
% 0.13/5.41 (![X,Y]: (( X = Y| apply(X,n(X,Y)) != apply(Y,n(X,Y)) ) ))),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f10,axiom,(
% 0.13/5.41 projection1 != projection2 ),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f11,axiom,(
% 0.13/5.41 apply(k,projection1) = k_projection1 ),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f12,axiom,(
% 0.13/5.41 apply(k,projection2) = k_projection2 ),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f13,axiom,(
% 0.13/5.41 s = apply(eq,pair(apply(k,s),apply(k,projection2))) ),
% 0.13/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.41 fof(f14,plain,(
% 0.13/5.41 ![X0,X1]: (apply(apply(k,X0),X1)=X0)),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/5.41 fof(f15,plain,(
% 0.13/5.41 ![X0,X1]: (apply(projection1,pair(X0,X1))=X0)),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/5.41 fof(f16,plain,(
% 0.13/5.41 ![X0,X1]: (apply(projection2,pair(X0,X1))=X1)),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/5.41 fof(f19,plain,(
% 0.13/5.41 ![X0,X1,X2]: (apply(apply(apply(abstraction,X0),X1),X2)=apply(apply(X0,apply(k,X2)),apply(X1,X2)))),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/5.41 fof(f20,plain,(
% 0.13/5.41 ![X0]: (apply(eq,pair(X0,X0))=projection1)),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/5.41 fof(f21,plain,(
% 0.13/5.41 ![X0,X1]: (X0=X1|apply(eq,pair(X0,X1))=projection2)),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/5.41 fof(f22,plain,(
% 0.13/5.41 ![X0,X1]: (X0=X1|~apply(X0,n(X0,X1))=apply(X1,n(X0,X1)))),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/5.41 fof(f23,plain,(
% 0.13/5.41 ~projection1=projection2),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/5.41 fof(f24,plain,(
% 0.13/5.41 apply(k,projection1)=k_projection1),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/5.41 fof(f25,plain,(
% 0.13/5.41 apply(k,projection2)=k_projection2),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/5.41 fof(f26,plain,(
% 0.13/5.41 s=apply(eq,pair(apply(k,s),apply(k,projection2)))),
% 0.13/5.41 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/5.41 fof(f27,plain,(
% 0.13/5.41 ![X0,X1]: (apply(apply(apply(abstraction,k),X0),X1)=apply(k,X1))),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f14,f19])).
% 0.13/5.41 fof(f314,plain,(
% 0.13/5.41 ![X0]: (apply(k_projection1,X0)=projection1)),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f24,f14])).
% 0.13/5.41 fof(f334,plain,(
% 0.13/5.41 ![X0]: (apply(k_projection2,X0)=projection2)),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f25,f14])).
% 0.13/5.41 fof(f357,plain,(
% 0.13/5.41 ![X0]: (X0=X0|projection1=projection2)),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f20,f21])).
% 0.13/5.41 fof(f361,definition,(
% 0.13/5.41 ![X0]: (sQ0_spl <=> (X0=X0))),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f364,definition,(
% 0.13/5.41 sQ1_spl <=> (projection1=projection2)),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f367,plain,(
% 0.13/5.41 sQ0_spl|sQ1_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f357,f361,f364])).
% 0.13/5.41 fof(f376,plain,(
% 0.13/5.41 ![X0]: (apply(apply(abstraction,k),X0)=k)),
% 0.13/5.41 inference(resolution,[status(thm)],[f22,f27])).
% 0.13/5.41 fof(f379,plain,(
% 0.13/5.41 ![X0]: (k_projection2=X0|~projection2=apply(X0,n(k_projection2,X0)))),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f334,f22])).
% 0.13/5.41 fof(f380,plain,(
% 0.13/5.41 ![X0]: (k_projection1=X0|~projection1=apply(X0,n(k_projection1,X0)))),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f314,f22])).
% 0.13/5.41 fof(f416,plain,(
% 0.13/5.41 k_projection2=k_projection1|~projection2=projection1),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f314,f379])).
% 0.13/5.41 fof(f417,plain,(
% 0.13/5.41 k_projection2=apply(abstraction,k)|~projection2=k),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f376,f379])).
% 0.13/5.41 fof(f433,definition,(
% 0.13/5.41 sQ4_spl <=> (k_projection2=k_projection1)),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f434,plain,(
% 0.13/5.41 k_projection2=k_projection1|~sQ4_spl),
% 0.13/5.41 inference(component_clause,[status(thm)],[f433])).
% 0.13/5.41 fof(f435,plain,(
% 0.13/5.41 ~k_projection2=k_projection1|sQ4_spl),
% 0.13/5.41 inference(component_clause,[status(thm)],[f433])).
% 0.13/5.41 fof(f436,plain,(
% 0.13/5.41 sQ4_spl|~sQ1_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f416,f433,f364])).
% 0.13/5.41 fof(f437,definition,(
% 0.13/5.41 sQ5_spl <=> (k_projection2=apply(abstraction,k))),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f438,plain,(
% 0.13/5.41 k_projection2=apply(abstraction,k)|~sQ5_spl),
% 0.13/5.41 inference(component_clause,[status(thm)],[f437])).
% 0.13/5.41 fof(f440,definition,(
% 0.13/5.41 sQ6_spl <=> (projection2=k)),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f443,plain,(
% 0.13/5.41 sQ5_spl|~sQ6_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f417,f437,f440])).
% 0.13/5.41 fof(f446,plain,(
% 0.13/5.41 ![X0]: (apply(k_projection2,X0)=projection1|~sQ4_spl)),
% 0.13/5.41 inference(backward_demodulation,[status(thm)],[f434,f314])).
% 0.13/5.41 fof(f448,plain,(
% 0.13/5.41 projection2=projection1|~sQ4_spl),
% 0.13/5.41 inference(forward_demodulation,[status(thm)],[f334,f446])).
% 0.13/5.41 fof(f449,plain,(
% 0.13/5.41 $false|~sQ4_spl),
% 0.13/5.41 inference(forward_subsumption_resolution,[status(thm)],[f448,f23])).
% 0.13/5.41 fof(f450,plain,(
% 0.13/5.41 ~sQ4_spl),
% 0.13/5.41 inference(contradiction_clause,[status(thm)],[f449])).
% 0.13/5.41 fof(f498,plain,(
% 0.13/5.41 s=apply(eq,pair(apply(k,s),k_projection2))),
% 0.13/5.41 inference(forward_demodulation,[status(thm)],[f25,f26])).
% 0.13/5.41 fof(f499,plain,(
% 0.13/5.41 s=projection2|apply(k,s)=k_projection2),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f21,f498])).
% 0.13/5.41 fof(f505,definition,(
% 0.13/5.41 sQ7_spl <=> (s=projection2)),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f506,plain,(
% 0.13/5.41 s=projection2|~sQ7_spl),
% 0.13/5.41 inference(component_clause,[status(thm)],[f505])).
% 0.13/5.41 fof(f508,definition,(
% 0.13/5.41 sQ8_spl <=> (apply(k,s)=k_projection2)),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f509,plain,(
% 0.13/5.41 apply(k,s)=k_projection2|~sQ8_spl),
% 0.13/5.41 inference(component_clause,[status(thm)],[f508])).
% 0.13/5.41 fof(f511,plain,(
% 0.13/5.41 sQ7_spl|sQ8_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f499,f505,f508])).
% 0.13/5.41 fof(f542,plain,(
% 0.13/5.41 ![X0]: (apply(k_projection2,X0)=k|~sQ5_spl)),
% 0.13/5.41 inference(backward_demodulation,[status(thm)],[f438,f376])).
% 0.13/5.41 fof(f549,plain,(
% 0.13/5.41 projection2=k|~sQ5_spl),
% 0.13/5.41 inference(forward_demodulation,[status(thm)],[f334,f542])).
% 0.13/5.41 fof(f570,plain,(
% 0.13/5.41 ![X0,X1]: (apply(apply(projection2,X0),X1)=X0|~sQ5_spl)),
% 0.13/5.41 inference(backward_demodulation,[status(thm)],[f549,f14])).
% 0.13/5.41 fof(f584,plain,(
% 0.13/5.41 ![X0,X1,X2]: (apply(X0,X1)=pair(X2,X0)|~sQ5_spl)),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f16,f570])).
% 0.13/5.41 fof(f594,plain,(
% 0.13/5.41 ![X0,X1,X2]: (projection2=pair(X0,eq)|X1=X2|~sQ5_spl)),
% 0.13/5.41 inference(paramodulation,[status(thm)],[f21,f584])).
% 0.13/5.41 fof(f625,definition,(
% 0.13/5.41 ![X0]: (sQ9_spl <=> (projection2=pair(X0,eq)))),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f626,plain,(
% 0.13/5.41 ![X0]: (projection2=pair(X0,eq)|~sQ9_spl)),
% 0.13/5.41 inference(component_clause,[status(thm)],[f625])).
% 0.13/5.41 fof(f628,definition,(
% 0.13/5.41 ![X1,X2]: (sQ10_spl <=> (X1=X2))),
% 0.13/5.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/5.41 fof(f629,plain,(
% 0.13/5.41 ![X0,X1]: (X0=X1|~sQ10_spl)),
% 0.13/5.41 inference(component_clause,[status(thm)],[f628])).
% 0.13/5.41 fof(f631,plain,(
% 0.13/5.41 sQ9_spl|sQ10_spl|~sQ5_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f594,f625,f628,f437])).
% 0.13/5.41 fof(f633,plain,(
% 0.13/5.41 $false|~sQ10_spl|sQ4_spl),
% 0.13/5.41 inference(backward_subsumption_resolution,[status(thm)],[f435,f629])).
% 0.13/5.41 fof(f635,plain,(
% 0.13/5.41 ~sQ10_spl|sQ4_spl),
% 0.13/5.41 inference(contradiction_clause,[status(thm)],[f633])).
% 0.13/5.42 fof(f646,plain,(
% 0.13/5.42 ![X0]: (apply(k_projection2,X0)=s|~sQ7_spl)),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f506,f334])).
% 0.13/5.42 fof(f687,plain,(
% 0.13/5.42 ![X0]: (apply(projection1,projection2)=X0|~sQ9_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f626,f15])).
% 0.13/5.42 fof(f688,plain,(
% 0.13/5.42 ![X0,X1]: (X0=X1|~sQ9_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f687,f687])).
% 0.13/5.42 fof(f690,plain,(
% 0.13/5.42 sQ10_spl|~sQ9_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f688,f628,f625])).
% 0.13/5.42 fof(f699,plain,(
% 0.13/5.42 k_projection1=apply(abstraction,k)|~projection1=k),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f376,f380])).
% 0.13/5.42 fof(f710,definition,(
% 0.13/5.42 sQ13_spl <=> (k_projection1=apply(abstraction,k))),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f711,plain,(
% 0.13/5.42 k_projection1=apply(abstraction,k)|~sQ13_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f710])).
% 0.13/5.42 fof(f713,definition,(
% 0.13/5.42 sQ14_spl <=> (projection1=k)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f716,plain,(
% 0.13/5.42 sQ13_spl|~sQ14_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f699,f710,f713])).
% 0.13/5.42 fof(f732,plain,(
% 0.13/5.42 ![X0]: (apply(k_projection1,X0)=k|~sQ13_spl)),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f711,f376])).
% 0.13/5.42 fof(f736,plain,(
% 0.13/5.42 projection1=k|~sQ13_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f314,f732])).
% 0.13/5.42 fof(f743,plain,(
% 0.13/5.42 ![X0,X1]: (apply(apply(projection1,X0),X1)=X0|~sQ13_spl)),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f736,f14])).
% 0.13/5.42 fof(f761,plain,(
% 0.13/5.42 ![X0,X1,X2]: (apply(X0,X1)=pair(X0,X2)|~sQ13_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f15,f743])).
% 0.13/5.42 fof(f769,plain,(
% 0.13/5.42 ![X0,X1]: (X0=pair(projection1,X1)|~sQ13_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f15,f761])).
% 0.13/5.42 fof(f789,plain,(
% 0.13/5.42 ![X0,X1]: (X0=X1|~sQ13_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f769,f769])).
% 0.13/5.42 fof(f793,plain,(
% 0.13/5.42 sQ10_spl|~sQ13_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f789,f628,f710])).
% 0.13/5.42 fof(f816,plain,(
% 0.13/5.42 ![X0]: (apply(k_projection2,X0)=s|~sQ8_spl)),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f509,f14])).
% 0.13/5.42 fof(f819,plain,(
% 0.13/5.42 s=projection2|~sQ8_spl),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f816,f334])).
% 0.13/5.42 fof(f825,definition,(
% 0.13/5.42 sQ18_spl <=> (projection1=s)),
% 0.13/5.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/5.42 fof(f827,plain,(
% 0.13/5.42 ~projection1=s|sQ18_spl),
% 0.13/5.42 inference(component_clause,[status(thm)],[f825])).
% 0.13/5.42 fof(f832,plain,(
% 0.13/5.42 k_projection1=k_projection2|~projection1=s|~sQ7_spl),
% 0.13/5.42 inference(paramodulation,[status(thm)],[f646,f380])).
% 0.13/5.42 fof(f836,plain,(
% 0.13/5.42 sQ4_spl|~sQ18_spl|~sQ7_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f832,f433,f825,f505])).
% 0.13/5.42 fof(f906,plain,(
% 0.13/5.42 sQ7_spl|~sQ8_spl),
% 0.13/5.42 inference(split_clause,[status(thm)],[f819,f505,f508])).
% 0.13/5.42 fof(f916,plain,(
% 0.13/5.42 s=projection2|~sQ7_spl),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f646,f334])).
% 0.13/5.42 fof(f976,plain,(
% 0.13/5.42 apply(k,s)=k_projection2|~sQ7_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f916,f25])).
% 0.13/5.42 fof(f1043,plain,(
% 0.13/5.42 s=apply(eq,pair(k_projection2,k_projection2))|~sQ7_spl),
% 0.13/5.42 inference(forward_demodulation,[status(thm)],[f976,f498])).
% 0.13/5.42 fof(f1216,plain,(
% 0.13/5.42 s=projection1|~sQ7_spl),
% 0.13/5.42 inference(backward_demodulation,[status(thm)],[f20,f1043])).
% 0.13/5.42 fof(f1223,plain,(
% 0.13/5.42 $false|sQ18_spl|~sQ7_spl),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f1216,f827])).
% 0.13/5.42 fof(f1224,plain,(
% 0.13/5.42 sQ18_spl|~sQ7_spl),
% 0.13/5.42 inference(contradiction_clause,[status(thm)],[f1223])).
% 0.13/5.42 fof(f1225,plain,(
% 0.13/5.42 $false),
% 0.13/5.42 inference(sat_refutation,[status(thm)],[f367,f436,f443,f450,f511,f631,f635,f690,f716,f793,f836,f906,f1224])).
% 0.13/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.44 % Elapsed time: 0.064701 seconds
% 0.13/5.44 % CPU time: 0.298873 seconds
% 0.13/5.44 % Total memory used: 108.530 MB
% 0.13/5.44 % Net memory used: 108.021 MB
%------------------------------------------------------------------------------