%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 02:01:16 PM UTC 2026
% Result : Theorem 3.28s 0.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ133+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n016.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 03:56:53 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 3.28/0.97 % Refutation found
% 3.28/0.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.28/0.97 % SZS output start CNFRefutation for theBenchmark
% 3.28/0.97 fof(f1,axiom,(
% 3.28/0.97 ( queens_p=> (! [I,J] :( ( le(s(n0),I)& le(I,n)& le(s(I),J)& le(J,n) )=> ( p(I) != p(J)& plus(p(I),I) != plus(p(J),J)& minus(p(I),I) != minus(p(J),J) ) ) )) ),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f3,axiom,(
% 3.28/0.97 ( (! [I,J] :( ( le(s(n0),I)& le(I,n)& le(s(I),J)& le(J,n)& ( le(s(I),J)<=> le(s(perm(J)),perm(I)) ) )=> ( q(I) != q(J)& plus(q(I),I) != plus(q(J),J)& minus(q(I),I) != minus(q(J),J) ) ))=> queens_q ) ),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f4,conjecture,(
% 3.28/0.97 ( ( queens_p& (! [I] : q(I) = p(perm(I)) ))=> queens_q ) ),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f5,negated_conjecture,(
% 3.28/0.97 ~(( ( queens_p& (! [I] : q(I) = p(perm(I)) ))=> queens_q ) )),
% 3.28/0.97 inference(negated_conjecture,[status(cth)],[f4])).
% 3.28/0.97 fof(f6,axiom,(
% 3.28/0.97 (! [I] :( ( le(s(n0),I)& le(I,n) )=> ( le(s(n0),perm(I))& le(perm(I),n) ) ) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f7,axiom,(
% 3.28/0.97 (! [J,I] : minus(I,J) = minus(perm(J),perm(I)) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f8,axiom,(
% 3.28/0.97 (! [X,Y,Z] :( ( le(X,Y)& le(Y,Z) )=> le(X,Z) ) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f9,axiom,(
% 3.28/0.97 (! [X] : le(X,s(X)) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f10,axiom,(
% 3.28/0.97 (! [I,J,K,L] :( plus(I,J) = plus(K,L)<=> minus(I,K) = minus(L,J) ) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f11,axiom,(
% 3.28/0.97 (! [I,J,K,L] :( minus(I,J) = minus(K,L)<=> minus(I,K) = minus(J,L) ) )),
% 3.28/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.28/0.97 fof(f12,plain,(
% 3.28/0.97 ~queens_p|(![I,J]: ((((~le(s(n0),I)|~le(I,n))|~le(s(I),J))|~le(J,n))|((~p(I)=p(J)&~plus(p(I),I)=plus(p(J),J))&~minus(p(I),I)=minus(p(J),J))))),
% 3.28/0.97 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 3.28/0.97 fof(f13,plain,(
% 3.28/0.97 ![X0,X1]: (~queens_p|~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f12])).
% 3.28/0.97 fof(f14,plain,(
% 3.28/0.97 ![X0,X1]: (~queens_p|~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~plus(p(X0),X0)=plus(p(X1),X1))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f12])).
% 3.28/0.97 fof(f15,plain,(
% 3.28/0.97 ![X0,X1]: (~queens_p|~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~minus(p(X0),X0)=minus(p(X1),X1))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f12])).
% 3.28/0.97 fof(f18,plain,(
% 3.28/0.97 (?[I,J]: (((((le(s(n0),I)&le(I,n))&le(s(I),J))&le(J,n))&(le(s(I),J)<=>le(s(perm(J)),perm(I))))&((q(I)=q(J)|plus(q(I),I)=plus(q(J),J))|minus(q(I),I)=minus(q(J),J))))|queens_q),
% 3.28/0.97 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 3.28/0.97 fof(f19,plain,(
% 3.28/0.97 (?[I,J]: (((((le(s(n0),I)&le(I,n))&le(s(I),J))&le(J,n))&((~le(s(I),J)|le(s(perm(J)),perm(I)))&(le(s(I),J)|~le(s(perm(J)),perm(I)))))&((q(I)=q(J)|plus(q(I),I)=plus(q(J),J))|minus(q(I),I)=minus(q(J),J))))|queens_q),
% 3.28/0.97 inference(NNF_transformation,[status(thm)],[f18])).
% 3.28/0.97 fof(f20,plain,(
% 3.28/0.97 (((((le(s(n0),sK0_skl)&le(sK0_skl,n))&le(s(sK0_skl),sK1_skl))&le(sK1_skl,n))&((~le(s(sK0_skl),sK1_skl)|le(s(perm(sK1_skl)),perm(sK0_skl)))&(le(s(sK0_skl),sK1_skl)|~le(s(perm(sK1_skl)),perm(sK0_skl)))))&((q(sK0_skl)=q(sK1_skl)|plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl))|minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl)))|queens_q),
% 3.28/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(I,sK0_skl),skolemize(J,sK1_skl)],[f19])).
% 3.28/0.97 fof(f21,plain,(
% 3.28/0.97 le(s(n0),sK0_skl)|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f22,plain,(
% 3.28/0.97 le(sK0_skl,n)|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f23,plain,(
% 3.28/0.97 le(s(sK0_skl),sK1_skl)|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f24,plain,(
% 3.28/0.97 le(sK1_skl,n)|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f25,plain,(
% 3.28/0.97 ~le(s(sK0_skl),sK1_skl)|le(s(perm(sK1_skl)),perm(sK0_skl))|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f27,plain,(
% 3.28/0.97 q(sK0_skl)=q(sK1_skl)|plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl)|minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl)|queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f20])).
% 3.28/0.97 fof(f28,plain,(
% 3.28/0.97 ((queens_p&(![I]: q(I)=p(perm(I))))&~queens_q)),
% 3.28/0.97 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.28/0.97 fof(f29,plain,(
% 3.28/0.97 queens_p),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f28])).
% 3.28/0.97 fof(f30,plain,(
% 3.28/0.97 ![X0]: (q(X0)=p(perm(X0)))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f28])).
% 3.28/0.97 fof(f31,plain,(
% 3.28/0.97 ~queens_q),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f28])).
% 3.28/0.97 fof(f32,plain,(
% 3.28/0.97 ![I]: ((~le(s(n0),I)|~le(I,n))|(le(s(n0),perm(I))&le(perm(I),n)))),
% 3.28/0.97 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 3.28/0.97 fof(f33,plain,(
% 3.28/0.97 ![X0]: (~le(s(n0),X0)|~le(X0,n)|le(s(n0),perm(X0)))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f32])).
% 3.28/0.97 fof(f34,plain,(
% 3.28/0.97 ![X0]: (~le(s(n0),X0)|~le(X0,n)|le(perm(X0),n))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f32])).
% 3.28/0.97 fof(f35,plain,(
% 3.28/0.97 ![X0,X1]: (minus(X0,X1)=minus(perm(X1),perm(X0)))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f7])).
% 3.28/0.97 fof(f36,plain,(
% 3.28/0.97 ![X,Y,Z]: ((~le(X,Y)|~le(Y,Z))|le(X,Z))),
% 3.28/0.97 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.28/0.97 fof(f37,plain,(
% 3.28/0.97 ![X,Z]: ((![Y]: (~le(X,Y)|~le(Y,Z)))|le(X,Z))),
% 3.28/0.97 inference(miniscoping,[status(thm)],[f36])).
% 3.28/0.97 fof(f38,plain,(
% 3.28/0.97 ![X0,X1,X2]: (~le(X0,X1)|~le(X1,X2)|le(X0,X2))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f37])).
% 3.28/0.97 fof(f39,plain,(
% 3.28/0.97 ![X0]: (le(X0,s(X0)))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f9])).
% 3.28/0.97 fof(f40,plain,(
% 3.28/0.97 ![I,J,K,L]: ((~plus(I,J)=plus(K,L)|minus(I,K)=minus(L,J))&(plus(I,J)=plus(K,L)|~minus(I,K)=minus(L,J)))),
% 3.28/0.97 inference(NNF_transformation,[status(thm)],[f10])).
% 3.28/0.97 fof(f41,plain,(
% 3.28/0.97 (![I,J,K,L]: (~plus(I,J)=plus(K,L)|minus(I,K)=minus(L,J)))&(![I,J,K,L]: (plus(I,J)=plus(K,L)|~minus(I,K)=minus(L,J)))),
% 3.28/0.97 inference(miniscoping,[status(thm)],[f40])).
% 3.28/0.97 fof(f42,plain,(
% 3.28/0.97 ![X0,X1,X2,X3]: (~plus(X0,X1)=plus(X2,X3)|minus(X0,X2)=minus(X3,X1))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f41])).
% 3.28/0.97 fof(f43,plain,(
% 3.28/0.97 ![X0,X1,X2,X3]: (plus(X0,X1)=plus(X2,X3)|~minus(X0,X2)=minus(X3,X1))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f41])).
% 3.28/0.97 fof(f44,plain,(
% 3.28/0.97 ![I,J,K,L]: ((~minus(I,J)=minus(K,L)|minus(I,K)=minus(J,L))&(minus(I,J)=minus(K,L)|~minus(I,K)=minus(J,L)))),
% 3.28/0.97 inference(NNF_transformation,[status(thm)],[f11])).
% 3.28/0.97 fof(f45,plain,(
% 3.28/0.97 (![I,J,K,L]: (~minus(I,J)=minus(K,L)|minus(I,K)=minus(J,L)))&(![I,J,K,L]: (minus(I,J)=minus(K,L)|~minus(I,K)=minus(J,L)))),
% 3.28/0.97 inference(miniscoping,[status(thm)],[f44])).
% 3.28/0.97 fof(f46,plain,(
% 3.28/0.97 ![X0,X1,X2,X3]: (~minus(X0,X1)=minus(X2,X3)|minus(X0,X2)=minus(X1,X3))),
% 3.28/0.97 inference(cnf_transformation,[status(thm)],[f45])).
% 3.28/0.97 fof(f48,definition,(
% 3.28/0.97 sQ0_spl <=> (queens_p)),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f50,plain,(
% 3.28/0.97 ~queens_p|sQ0_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f48])).
% 3.28/0.97 fof(f51,definition,(
% 3.28/0.97 ![X0,X1]: (sQ1_spl <=> (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f52,plain,(
% 3.28/0.97 ![X0,X1]: (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1)|~sQ1_spl)),
% 3.28/0.97 inference(component_clause,[status(thm)],[f51])).
% 3.28/0.97 fof(f54,plain,(
% 3.28/0.97 ~sQ0_spl|sQ1_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f13,f48,f51])).
% 3.28/0.97 fof(f55,definition,(
% 3.28/0.97 ![X0,X1]: (sQ2_spl <=> (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~plus(p(X0),X0)=plus(p(X1),X1)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f56,plain,(
% 3.28/0.97 ![X0,X1]: (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~plus(p(X0),X0)=plus(p(X1),X1)|~sQ2_spl)),
% 3.28/0.97 inference(component_clause,[status(thm)],[f55])).
% 3.28/0.97 fof(f58,plain,(
% 3.28/0.97 ~sQ0_spl|sQ2_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f14,f48,f55])).
% 3.28/0.97 fof(f59,definition,(
% 3.28/0.97 ![X0,X1]: (sQ3_spl <=> (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~minus(p(X0),X0)=minus(p(X1),X1)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f60,plain,(
% 3.28/0.97 ![X0,X1]: (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~minus(p(X0),X0)=minus(p(X1),X1)|~sQ3_spl)),
% 3.28/0.97 inference(component_clause,[status(thm)],[f59])).
% 3.28/0.97 fof(f62,plain,(
% 3.28/0.97 ~sQ0_spl|sQ3_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f15,f48,f59])).
% 3.28/0.97 fof(f63,definition,(
% 3.28/0.97 sQ4_spl <=> (le(s(n0),sK0_skl))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f64,plain,(
% 3.28/0.97 le(s(n0),sK0_skl)|~sQ4_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f63])).
% 3.28/0.97 fof(f66,definition,(
% 3.28/0.97 sQ5_spl <=> (queens_q)),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f67,plain,(
% 3.28/0.97 queens_q|~sQ5_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f66])).
% 3.28/0.97 fof(f69,plain,(
% 3.28/0.97 sQ4_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f21,f63,f66])).
% 3.28/0.97 fof(f70,definition,(
% 3.28/0.97 sQ6_spl <=> (le(sK0_skl,n))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f73,plain,(
% 3.28/0.97 sQ6_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f22,f70,f66])).
% 3.28/0.97 fof(f74,definition,(
% 3.28/0.97 sQ7_spl <=> (le(s(sK0_skl),sK1_skl))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f75,plain,(
% 3.28/0.97 le(s(sK0_skl),sK1_skl)|~sQ7_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f74])).
% 3.28/0.97 fof(f77,plain,(
% 3.28/0.97 sQ7_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f23,f74,f66])).
% 3.28/0.97 fof(f78,definition,(
% 3.28/0.97 sQ8_spl <=> (le(sK1_skl,n))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f81,plain,(
% 3.28/0.97 sQ8_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f24,f78,f66])).
% 3.28/0.97 fof(f82,definition,(
% 3.28/0.97 sQ9_spl <=> (le(s(perm(sK1_skl)),perm(sK0_skl)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f83,plain,(
% 3.28/0.97 le(s(perm(sK1_skl)),perm(sK0_skl))|~sQ9_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f82])).
% 3.28/0.97 fof(f85,plain,(
% 3.28/0.97 ~sQ7_spl|sQ9_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f25,f74,f82,f66])).
% 3.28/0.97 fof(f87,definition,(
% 3.28/0.97 sQ10_spl <=> (q(sK0_skl)=q(sK1_skl))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f88,plain,(
% 3.28/0.97 q(sK0_skl)=q(sK1_skl)|~sQ10_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f87])).
% 3.28/0.97 fof(f90,definition,(
% 3.28/0.97 sQ11_spl <=> (plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f91,plain,(
% 3.28/0.97 plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl)|~sQ11_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f90])).
% 3.28/0.97 fof(f93,definition,(
% 3.28/0.97 sQ12_spl <=> (minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f94,plain,(
% 3.28/0.97 minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl)|~sQ12_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f93])).
% 3.28/0.97 fof(f96,plain,(
% 3.28/0.97 sQ10_spl|sQ11_spl|sQ12_spl|sQ5_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f27,f87,f90,f93,f66])).
% 3.28/0.97 fof(f97,plain,(
% 3.28/0.97 $false|~sQ5_spl),
% 3.28/0.97 inference(forward_subsumption_resolution,[status(thm)],[f67,f31])).
% 3.28/0.97 fof(f98,plain,(
% 3.28/0.97 ~sQ5_spl),
% 3.28/0.97 inference(contradiction_clause,[status(thm)],[f97])).
% 3.28/0.97 fof(f99,plain,(
% 3.28/0.97 $false|sQ0_spl),
% 3.28/0.97 inference(forward_subsumption_resolution,[status(thm)],[f50,f29])).
% 3.28/0.97 fof(f100,plain,(
% 3.28/0.97 sQ0_spl),
% 3.28/0.97 inference(contradiction_clause,[status(thm)],[f99])).
% 3.28/0.97 fof(f124,plain,(
% 3.28/0.97 ~le(sK0_skl,n)|le(perm(sK0_skl),n)|~sQ4_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f34,f64])).
% 3.28/0.97 fof(f126,definition,(
% 3.28/0.97 sQ18_spl <=> (le(perm(sK0_skl),n))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f129,plain,(
% 3.28/0.97 ~sQ6_spl|sQ18_spl|~sQ4_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f124,f70,f126,f63])).
% 3.28/0.97 fof(f152,plain,(
% 3.28/0.97 ~le(s(n0),perm(sK1_skl))|~le(perm(sK1_skl),n)|~le(perm(sK0_skl),n)|~p(perm(sK1_skl))=p(perm(sK0_skl))|~sQ1_spl|~sQ9_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f52,f83])).
% 3.28/0.97 fof(f169,definition,(
% 3.28/0.97 sQ26_spl <=> (le(s(n0),perm(sK1_skl)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f172,definition,(
% 3.28/0.97 sQ27_spl <=> (le(perm(sK1_skl),n))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f175,definition,(
% 3.28/0.97 sQ28_spl <=> (p(perm(sK1_skl))=p(perm(sK0_skl)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f177,plain,(
% 3.28/0.97 ~p(perm(sK1_skl))=p(perm(sK0_skl))|sQ28_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f175])).
% 3.28/0.97 fof(f178,plain,(
% 3.28/0.97 ~sQ26_spl|~sQ27_spl|~sQ18_spl|~sQ28_spl|~sQ1_spl|~sQ9_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f152,f169,f172,f126,f175,f51,f82])).
% 3.28/0.97 fof(f199,plain,(
% 3.28/0.97 ~q(sK1_skl)=p(perm(sK0_skl))|sQ28_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f177])).
% 3.28/0.97 fof(f200,plain,(
% 3.28/0.97 ~q(sK1_skl)=q(sK0_skl)|sQ28_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f199])).
% 3.28/0.97 fof(f207,plain,(
% 3.28/0.97 ![X0]: (~le(sK0_skl,X0)|le(s(n0),X0)|~sQ4_spl)),
% 3.28/0.97 inference(resolution,[status(thm)],[f38,f64])).
% 3.28/0.97 fof(f209,plain,(
% 3.28/0.97 ![X0,X1]: (~le(s(X0),X1)|le(X0,X1))),
% 3.28/0.97 inference(resolution,[status(thm)],[f38,f39])).
% 3.28/0.97 fof(f227,plain,(
% 3.28/0.97 ![X0,X1,X2,X3]: (plus(X0,perm(X1))=plus(X2,perm(X3))|~minus(X0,X2)=minus(X1,X3))),
% 3.28/0.97 inference(paramodulation,[status(thm)],[f35,f43])).
% 3.28/0.97 fof(f232,plain,(
% 3.28/0.97 ~le(s(n0),perm(sK1_skl))|~le(perm(sK1_skl),n)|~le(perm(sK0_skl),n)|~plus(p(perm(sK1_skl)),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl))|~sQ2_spl|~sQ9_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f56,f83])).
% 3.28/0.97 fof(f249,definition,(
% 3.28/0.97 sQ37_spl <=> (plus(p(perm(sK1_skl)),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f251,plain,(
% 3.28/0.97 ~plus(p(perm(sK1_skl)),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl))|sQ37_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f249])).
% 3.28/0.97 fof(f252,plain,(
% 3.28/0.97 ~sQ26_spl|~sQ27_spl|~sQ18_spl|~sQ37_spl|~sQ2_spl|~sQ9_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f232,f169,f172,f126,f249,f55,f82])).
% 3.28/0.97 fof(f267,plain,(
% 3.28/0.97 ~plus(q(sK1_skl),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl))|sQ37_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f251])).
% 3.28/0.97 fof(f268,plain,(
% 3.28/0.97 ~plus(q(sK1_skl),perm(sK1_skl))=plus(q(sK0_skl),perm(sK0_skl))|sQ37_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f267])).
% 3.28/0.97 fof(f272,plain,(
% 3.28/0.97 ~le(s(n0),perm(sK1_skl))|~le(perm(sK1_skl),n)|~le(perm(sK0_skl),n)|~minus(p(perm(sK1_skl)),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl))|~sQ3_spl|~sQ9_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f60,f83])).
% 3.28/0.97 fof(f289,definition,(
% 3.28/0.97 sQ44_spl <=> (minus(p(perm(sK1_skl)),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl)))),
% 3.28/0.97 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 3.28/0.97 fof(f291,plain,(
% 3.28/0.97 ~minus(p(perm(sK1_skl)),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl))|sQ44_spl),
% 3.28/0.97 inference(component_clause,[status(thm)],[f289])).
% 3.28/0.97 fof(f292,plain,(
% 3.28/0.97 ~sQ26_spl|~sQ27_spl|~sQ18_spl|~sQ44_spl|~sQ3_spl|~sQ9_spl),
% 3.28/0.97 inference(split_clause,[status(thm)],[f272,f169,f172,f126,f289,f59,f82])).
% 3.28/0.97 fof(f307,plain,(
% 3.28/0.97 ~minus(q(sK1_skl),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl))|sQ44_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f291])).
% 3.28/0.97 fof(f308,plain,(
% 3.28/0.97 ~minus(q(sK1_skl),perm(sK1_skl))=minus(q(sK0_skl),perm(sK0_skl))|sQ44_spl),
% 3.28/0.97 inference(forward_demodulation,[status(thm)],[f30,f307])).
% 3.28/0.97 fof(f333,plain,(
% 3.28/0.97 minus(q(sK0_skl),q(sK1_skl))=minus(sK0_skl,sK1_skl)|~sQ12_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f46,f94])).
% 3.28/0.97 fof(f344,plain,(
% 3.28/0.97 ![X0,X1,X2,X3]: (~minus(X0,X1)=minus(X2,X3)|minus(X0,perm(X3))=minus(X1,perm(X2)))),
% 3.28/0.97 inference(paramodulation,[status(thm)],[f35,f46])).
% 3.28/0.97 fof(f517,plain,(
% 3.28/0.97 le(sK0_skl,sK1_skl)|~sQ7_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f209,f75])).
% 3.28/0.97 fof(f534,plain,(
% 3.28/0.97 le(s(n0),sK1_skl)|~sQ7_spl|~sQ4_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f517,f207])).
% 3.28/0.97 fof(f594,plain,(
% 3.28/0.97 ~le(sK1_skl,n)|le(perm(sK1_skl),n)|~sQ7_spl|~sQ4_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f534,f34])).
% 3.28/0.97 fof(f595,plain,(
% 3.28/0.97 ~le(sK1_skl,n)|le(s(n0),perm(sK1_skl))|~sQ7_spl|~sQ4_spl),
% 3.28/0.97 inference(resolution,[status(thm)],[f534,f33])).
% 3.28/0.98 fof(f617,plain,(
% 3.28/0.98 ~sQ8_spl|sQ27_spl|~sQ7_spl|~sQ4_spl),
% 3.28/0.98 inference(split_clause,[status(thm)],[f594,f78,f172,f74,f63])).
% 3.28/0.98 fof(f618,plain,(
% 3.28/0.98 ~sQ8_spl|sQ26_spl|~sQ7_spl|~sQ4_spl),
% 3.28/0.98 inference(split_clause,[status(thm)],[f595,f78,f169,f74,f63])).
% 3.28/0.98 fof(f671,definition,(
% 3.28/0.98 sQ87_spl <=> (minus(q(sK0_skl),sK0_skl)=minus(q(sK0_skl),sK0_skl))),
% 3.28/0.98 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 3.28/0.98 fof(f673,plain,(
% 3.28/0.98 ~minus(q(sK0_skl),sK0_skl)=minus(q(sK0_skl),sK0_skl)|sQ87_spl),
% 3.28/0.98 inference(component_clause,[status(thm)],[f671])).
% 3.28/0.98 fof(f685,plain,(
% 3.28/0.98 $false|sQ87_spl),
% 3.28/0.98 inference(trivial_equality_resolution,[status(thm)],[f673])).
% 3.28/0.98 fof(f686,plain,(
% 3.28/0.98 sQ87_spl),
% 3.28/0.98 inference(contradiction_clause,[status(thm)],[f685])).
% 3.28/0.98 fof(f689,plain,(
% 3.28/0.98 $false|sQ28_spl|~sQ10_spl),
% 3.28/0.98 inference(forward_subsumption_resolution,[status(thm)],[f88,f200])).
% 3.28/0.98 fof(f690,plain,(
% 3.28/0.98 sQ28_spl|~sQ10_spl),
% 3.28/0.98 inference(contradiction_clause,[status(thm)],[f689])).
% 3.28/0.98 fof(f1250,plain,(
% 3.28/0.98 plus(q(sK0_skl),perm(sK0_skl))=plus(q(sK1_skl),perm(sK1_skl))|~sQ12_spl),
% 3.28/0.98 inference(resolution,[status(thm)],[f333,f227])).
% 3.28/0.98 fof(f1525,definition,(
% 3.28/0.98 sQ157_spl <=> (plus(sK1_skl,sK1_skl)=plus(sK1_skl,sK1_skl))),
% 3.28/0.98 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 3.28/0.98 fof(f1527,plain,(
% 3.28/0.98 ~plus(sK1_skl,sK1_skl)=plus(sK1_skl,sK1_skl)|sQ157_spl),
% 3.28/0.98 inference(component_clause,[status(thm)],[f1525])).
% 3.28/0.98 fof(f1548,plain,(
% 3.28/0.98 $false|sQ157_spl),
% 3.28/0.98 inference(trivial_equality_resolution,[status(thm)],[f1527])).
% 3.28/0.98 fof(f1549,plain,(
% 3.28/0.98 sQ157_spl),
% 3.28/0.98 inference(contradiction_clause,[status(thm)],[f1548])).
% 3.28/0.98 fof(f1550,plain,(
% 3.28/0.98 minus(q(sK0_skl),q(sK1_skl))=minus(sK1_skl,sK0_skl)|~sQ11_spl),
% 3.28/0.98 inference(resolution,[status(thm)],[f91,f42])).
% 3.28/0.98 fof(f1571,plain,(
% 3.28/0.98 minus(q(sK0_skl),perm(sK0_skl))=minus(q(sK1_skl),perm(sK1_skl))|~sQ11_spl),
% 3.28/0.98 inference(resolution,[status(thm)],[f1550,f344])).
% 3.28/0.98 fof(f1595,plain,(
% 3.28/0.98 $false|sQ44_spl|~sQ11_spl),
% 3.28/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1571,f308])).
% 3.28/0.98 fof(f1596,plain,(
% 3.28/0.98 sQ44_spl|~sQ11_spl),
% 3.28/0.98 inference(contradiction_clause,[status(thm)],[f1595])).
% 3.28/0.98 fof(f1604,plain,(
% 3.28/0.98 $false|sQ37_spl|~sQ12_spl),
% 3.28/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1250,f268])).
% 3.28/0.98 fof(f1605,plain,(
% 3.28/0.98 sQ37_spl|~sQ12_spl),
% 3.28/0.98 inference(contradiction_clause,[status(thm)],[f1604])).
% 3.28/0.98 fof(f1606,plain,(
% 3.28/0.98 $false),
% 3.28/0.98 inference(sat_refutation,[status(thm)],[f54,f58,f62,f69,f73,f77,f81,f85,f96,f98,f100,f129,f178,f252,f292,f617,f618,f686,f690,f1549,f1596,f1605])).
% 3.28/0.98 % SZS output end CNFRefutation for theBenchmark.p
% 3.28/1.00 % Elapsed time: 0.533397 seconds
% 3.28/1.00 % CPU time: 3.820207 seconds
% 3.28/1.00 % Total memory used: 135.410 MB
% 3.28/1.00 % Net memory used: 131.054 MB
%------------------------------------------------------------------------------