%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX222-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 03:13:50 PM UTC 2026
% Result : Unsatisfiable 0.18s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX222-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n001.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 10:40:59 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 0.18/0.59 % Refutation found
% 0.18/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.59 fof(f2,axiom,(
% 0.18/0.59 (![X,Z,X3,Tx3]: (aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f3,axiom,(
% 0.18/0.59 notb(btrue) = bfalse ),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f6,axiom,(
% 0.18/0.59 (![Z,Xs]: (index(cons(Z,Xs),zero) = just(Z) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f8,axiom,(
% 0.18/0.59 (![Q]: (andb(btrue,Q) = Q ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f13,axiom,(
% 0.18/0.59 (![E]: (nf(lam(E)) = nf(E) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f14,axiom,(
% 0.18/0.59 (![X4]: (nf(var(X4)) = btrue ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f16,axiom,(
% 0.18/0.59 (![X,E,Tx2,T1]: (tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f20,axiom,(
% 0.18/0.59 (![X,X3,Z]: (tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f21,axiom,(
% 0.18/0.59 (![X]: (sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))) ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f52,axiom,(
% 0.18/0.59 (![X]: (eq(X,X) = btrue ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f55,axiom,(
% 0.18/0.59 (![X]: (eq4(X,X) = btrue ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f56,negated_conjecture,(
% 0.18/0.59 (![X]: (eq4(sat_synth_nf_k(X),bfalse) != btrue ))),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f58,plain,(
% 0.18/0.59 ![X0,X1,X2,X3]: (aux(X0,X1,X2,just(X3))=eq(X3,X1))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f2])).
% 0.18/0.59 fof(f59,plain,(
% 0.18/0.59 notb(btrue)=bfalse),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f3])).
% 0.18/0.59 fof(f62,plain,(
% 0.18/0.59 ![X0,X1]: (index(cons(X0,X1),zero)=just(X0))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f6])).
% 0.18/0.59 fof(f64,plain,(
% 0.18/0.59 ![X0]: (andb(btrue,X0)=X0)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.59 fof(f69,plain,(
% 0.18/0.59 ![X0]: (nf(lam(X0))=nf(X0))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f13])).
% 0.18/0.59 fof(f70,plain,(
% 0.18/0.59 ![X0]: (nf(var(X0))=btrue)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f14])).
% 0.18/0.59 fof(f72,plain,(
% 0.18/0.59 ![X0,X1,X2,X3]: (tc(X0,lam(X1),arr(X2,X3))=tc(cons(X2,X0),X1,X3))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f16])).
% 0.18/0.59 fof(f76,plain,(
% 0.18/0.59 ![X0,X1,X2]: (tc(X0,var(X1),X2)=aux(X0,X2,X1,index(X0,X1)))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f20])).
% 0.18/0.59 fof(f77,plain,(
% 0.18/0.59 ![X0]: (sat_synth_nf_k(X0)=notb(andb(nf(X0),tc(nil,X0,arr(a,arr(b,b))))))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f21])).
% 0.18/0.59 fof(f113,plain,(
% 0.18/0.59 ![X0]: (eq(X0,X0)=btrue)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f52])).
% 0.18/0.59 fof(f116,plain,(
% 0.18/0.59 ![X0]: (eq4(X0,X0)=btrue)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.59 fof(f117,plain,(
% 0.18/0.59 ![X0]: (~eq4(sat_synth_nf_k(X0),bfalse)=btrue)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f56])).
% 0.18/0.59 fof(f172,plain,(
% 0.18/0.59 ![X0]: (sat_synth_nf_k(lam(X0))=notb(andb(nf(X0),tc(nil,lam(X0),arr(a,arr(b,b))))))),
% 0.18/0.59 inference(paramodulation,[status(thm)],[f69,f77])).
% 0.18/0.59 fof(f180,plain,(
% 0.18/0.59 ![X0]: (sat_synth_nf_k(lam(X0))=notb(andb(nf(X0),tc(cons(a,nil),X0,arr(b,b)))))),
% 0.18/0.59 inference(forward_demodulation,[status(thm)],[f72,f172])).
% 0.18/0.59 fof(f181,plain,(
% 0.18/0.59 ![X0]: (sat_synth_nf_k(lam(lam(X0)))=notb(andb(nf(X0),tc(cons(a,nil),lam(X0),arr(b,b)))))),
% 0.18/0.59 inference(paramodulation,[status(thm)],[f69,f180])).
% 0.18/0.59 fof(f187,plain,(
% 0.18/0.59 ![X0]: (sat_synth_nf_k(lam(lam(X0)))=notb(andb(nf(X0),tc(cons(b,cons(a,nil)),X0,b))))),
% 0.18/0.59 inference(forward_demodulation,[status(thm)],[f72,f181])).
% 0.18/0.59 fof(f211,plain,(
% 0.18/0.59 ![X0,X1,X2]: (tc(cons(X0,X1),var(zero),X2)=aux(cons(X0,X1),X2,zero,just(X0)))),
% 0.18/0.59 inference(paramodulation,[status(thm)],[f62,f76])).
% 0.18/0.59 fof(f213,plain,(
% 0.18/0.59 ![X0,X1,X2]: (tc(cons(X0,X1),var(zero),X2)=eq(X0,X2))),
% 0.18/0.59 inference(forward_demodulation,[status(thm)],[f58,f211])).
% 0.18/0.59 fof(f770,plain,(
% 0.18/0.59 sat_synth_nf_k(lam(lam(var(zero))))=notb(andb(nf(var(zero)),eq(b,b)))),
% 0.18/0.59 inference(paramodulation,[status(thm)],[f213,f187])).
% 0.25/0.60 fof(f775,plain,(
% 0.25/0.60 sat_synth_nf_k(lam(lam(var(zero))))=notb(andb(btrue,eq(b,b)))),
% 0.25/0.60 inference(forward_demodulation,[status(thm)],[f70,f770])).
% 0.25/0.60 fof(f776,plain,(
% 0.25/0.60 sat_synth_nf_k(lam(lam(var(zero))))=notb(eq(b,b))),
% 0.25/0.60 inference(forward_demodulation,[status(thm)],[f64,f775])).
% 0.25/0.60 fof(f777,plain,(
% 0.25/0.60 sat_synth_nf_k(lam(lam(var(zero))))=notb(btrue)),
% 0.25/0.60 inference(forward_demodulation,[status(thm)],[f113,f776])).
% 0.25/0.60 fof(f778,plain,(
% 0.25/0.60 sat_synth_nf_k(lam(lam(var(zero))))=bfalse),
% 0.25/0.60 inference(forward_demodulation,[status(thm)],[f59,f777])).
% 0.25/0.60 fof(f928,plain,(
% 0.25/0.60 ~eq4(bfalse,bfalse)=btrue),
% 0.25/0.60 inference(paramodulation,[status(thm)],[f778,f117])).
% 0.25/0.60 fof(f929,plain,(
% 0.25/0.60 ~btrue=btrue),
% 0.25/0.60 inference(forward_demodulation,[status(thm)],[f116,f928])).
% 0.25/0.60 fof(f930,plain,(
% 0.25/0.60 $false),
% 0.25/0.60 inference(trivial_equality_resolution,[status(thm)],[f929])).
% 0.25/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.61 % Elapsed time: 0.153002 seconds
% 0.25/0.61 % CPU time: 0.946133 seconds
% 0.25/0.61 % Total memory used: 85.533 MB
% 0.25/0.61 % Net memory used: 85.031 MB
%------------------------------------------------------------------------------