%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ133+1 : 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 : n013.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 0.47s 0.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PUZ133+1 : 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.17/0.43 % Computer : n013.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 03:51:37 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 0.47/0.90 % Refutation found
% 0.47/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.47/0.90 % SZS output start CNFRefutation for theBenchmark
% 0.47/0.90 fof(f1,axiom,(
% 0.47/0.90 ( 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) ) ) )) ),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f3,axiom,(
% 0.47/0.90 ( (! [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 ) ),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f4,conjecture,(
% 0.47/0.90 ( ( queens_p& (! [I] : q(I) = p(perm(I)) ))=> queens_q ) ),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f5,negated_conjecture,(
% 0.47/0.90 ~(( ( queens_p& (! [I] : q(I) = p(perm(I)) ))=> queens_q ) )),
% 0.47/0.90 inference(negated_conjecture,[status(cth)],[f4])).
% 0.47/0.90 fof(f6,axiom,(
% 0.47/0.90 (! [I] :( ( le(s(n0),I)& le(I,n) )=> ( le(s(n0),perm(I))& le(perm(I),n) ) ) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f7,axiom,(
% 0.47/0.90 (! [J,I] : minus(I,J) = minus(perm(J),perm(I)) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f8,axiom,(
% 0.47/0.90 (! [X,Y,Z] :( ( le(X,Y)& le(Y,Z) )=> le(X,Z) ) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f9,axiom,(
% 0.47/0.90 (! [X] : le(X,s(X)) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f10,axiom,(
% 0.47/0.90 (! [I,J,K,L] :( plus(I,J) = plus(K,L)<=> minus(I,K) = minus(L,J) ) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f11,axiom,(
% 0.47/0.90 (! [I,J,K,L] :( minus(I,J) = minus(K,L)<=> minus(I,K) = minus(J,L) ) )),
% 0.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/0.90 fof(f12,plain,(
% 0.47/0.90 ~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))))),
% 0.47/0.90 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.47/0.90 fof(f13,plain,(
% 0.47/0.90 ![X0,X1]: (~queens_p|~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f12])).
% 0.47/0.90 fof(f14,plain,(
% 0.47/0.90 ![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))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f12])).
% 0.47/0.90 fof(f15,plain,(
% 0.47/0.90 ![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))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f12])).
% 0.47/0.90 fof(f17,plain,(
% 0.47/0.90 (?[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),
% 0.47/0.90 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.47/0.90 fof(f18,plain,(
% 0.47/0.90 (?[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),
% 0.47/0.90 inference(NNF_transformation,[status(thm)],[f17])).
% 0.47/0.90 fof(f19,plain,(
% 0.47/0.90 (((((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),
% 0.47/0.90 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(I,sK0_skl),skolemize(J,sK1_skl)],[f18])).
% 0.47/0.90 fof(f20,plain,(
% 0.47/0.90 le(s(n0),sK0_skl)|queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f21,plain,(
% 0.47/0.90 le(sK0_skl,n)|queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f22,plain,(
% 0.47/0.90 le(s(sK0_skl),sK1_skl)|queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f23,plain,(
% 0.47/0.90 le(sK1_skl,n)|queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f24,plain,(
% 0.47/0.90 ~le(s(sK0_skl),sK1_skl)|le(s(perm(sK1_skl)),perm(sK0_skl))|queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f26,plain,(
% 0.47/0.90 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),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f19])).
% 0.47/0.90 fof(f27,plain,(
% 0.47/0.90 ((queens_p&(![I]: q(I)=p(perm(I))))&~queens_q)),
% 0.47/0.90 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.47/0.90 fof(f28,plain,(
% 0.47/0.90 queens_p),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f27])).
% 0.47/0.90 fof(f29,plain,(
% 0.47/0.90 ![X0]: (q(X0)=p(perm(X0)))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f27])).
% 0.47/0.90 fof(f30,plain,(
% 0.47/0.90 ~queens_q),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f27])).
% 0.47/0.90 fof(f31,plain,(
% 0.47/0.90 ![I]: ((~le(s(n0),I)|~le(I,n))|(le(s(n0),perm(I))&le(perm(I),n)))),
% 0.47/0.90 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.47/0.90 fof(f32,plain,(
% 0.47/0.90 ![X0]: (~le(s(n0),X0)|~le(X0,n)|le(s(n0),perm(X0)))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f31])).
% 0.47/0.90 fof(f33,plain,(
% 0.47/0.90 ![X0]: (~le(s(n0),X0)|~le(X0,n)|le(perm(X0),n))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f31])).
% 0.47/0.90 fof(f34,plain,(
% 0.47/0.90 ![X0,X1]: (minus(X0,X1)=minus(perm(X1),perm(X0)))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f7])).
% 0.47/0.90 fof(f35,plain,(
% 0.47/0.90 ![X,Y,Z]: ((~le(X,Y)|~le(Y,Z))|le(X,Z))),
% 0.47/0.90 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.47/0.90 fof(f36,plain,(
% 0.47/0.90 ![X,Z]: ((![Y]: (~le(X,Y)|~le(Y,Z)))|le(X,Z))),
% 0.47/0.90 inference(miniscoping,[status(thm)],[f35])).
% 0.47/0.90 fof(f37,plain,(
% 0.47/0.90 ![X0,X1,X2]: (~le(X0,X1)|~le(X1,X2)|le(X0,X2))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f36])).
% 0.47/0.90 fof(f38,plain,(
% 0.47/0.90 ![X0]: (le(X0,s(X0)))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f9])).
% 0.47/0.90 fof(f39,plain,(
% 0.47/0.90 ![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)))),
% 0.47/0.90 inference(NNF_transformation,[status(thm)],[f10])).
% 0.47/0.90 fof(f40,plain,(
% 0.47/0.90 (![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)))),
% 0.47/0.90 inference(miniscoping,[status(thm)],[f39])).
% 0.47/0.90 fof(f41,plain,(
% 0.47/0.90 ![X0,X1,X2,X3]: (~plus(X0,X1)=plus(X2,X3)|minus(X0,X2)=minus(X3,X1))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f40])).
% 0.47/0.90 fof(f42,plain,(
% 0.47/0.90 ![X0,X1,X2,X3]: (plus(X0,X1)=plus(X2,X3)|~minus(X0,X2)=minus(X3,X1))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f40])).
% 0.47/0.90 fof(f43,plain,(
% 0.47/0.90 ![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)))),
% 0.47/0.90 inference(NNF_transformation,[status(thm)],[f11])).
% 0.47/0.90 fof(f44,plain,(
% 0.47/0.90 (![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)))),
% 0.47/0.90 inference(miniscoping,[status(thm)],[f43])).
% 0.47/0.90 fof(f45,plain,(
% 0.47/0.90 ![X0,X1,X2,X3]: (~minus(X0,X1)=minus(X2,X3)|minus(X0,X2)=minus(X1,X3))),
% 0.47/0.90 inference(cnf_transformation,[status(thm)],[f44])).
% 0.47/0.90 fof(f47,definition,(
% 0.47/0.90 sQ0_spl <=> (queens_p)),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f49,plain,(
% 0.47/0.90 ~queens_p|sQ0_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f47])).
% 0.47/0.90 fof(f50,definition,(
% 0.47/0.90 ![X0,X1]: (sQ1_spl <=> (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f51,plain,(
% 0.47/0.90 ![X0,X1]: (~le(s(n0),X0)|~le(X0,n)|~le(s(X0),X1)|~le(X1,n)|~p(X0)=p(X1)|~sQ1_spl)),
% 0.47/0.90 inference(component_clause,[status(thm)],[f50])).
% 0.47/0.90 fof(f53,plain,(
% 0.47/0.90 ~sQ0_spl|sQ1_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f13,f47,f50])).
% 0.47/0.90 fof(f54,definition,(
% 0.47/0.90 ![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)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f55,plain,(
% 0.47/0.90 ![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)),
% 0.47/0.90 inference(component_clause,[status(thm)],[f54])).
% 0.47/0.90 fof(f57,plain,(
% 0.47/0.90 ~sQ0_spl|sQ2_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f14,f47,f54])).
% 0.47/0.90 fof(f58,definition,(
% 0.47/0.90 ![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)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f59,plain,(
% 0.47/0.90 ![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)),
% 0.47/0.90 inference(component_clause,[status(thm)],[f58])).
% 0.47/0.90 fof(f61,plain,(
% 0.47/0.90 ~sQ0_spl|sQ3_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f15,f47,f58])).
% 0.47/0.90 fof(f62,definition,(
% 0.47/0.90 sQ4_spl <=> (le(s(n0),sK0_skl))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f63,plain,(
% 0.47/0.90 le(s(n0),sK0_skl)|~sQ4_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f62])).
% 0.47/0.90 fof(f65,definition,(
% 0.47/0.90 sQ5_spl <=> (queens_q)),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f66,plain,(
% 0.47/0.90 queens_q|~sQ5_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f65])).
% 0.47/0.90 fof(f68,plain,(
% 0.47/0.90 sQ4_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f20,f62,f65])).
% 0.47/0.90 fof(f69,definition,(
% 0.47/0.90 sQ6_spl <=> (le(sK0_skl,n))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f72,plain,(
% 0.47/0.90 sQ6_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f21,f69,f65])).
% 0.47/0.90 fof(f73,definition,(
% 0.47/0.90 sQ7_spl <=> (le(s(sK0_skl),sK1_skl))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f74,plain,(
% 0.47/0.90 le(s(sK0_skl),sK1_skl)|~sQ7_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f73])).
% 0.47/0.90 fof(f76,plain,(
% 0.47/0.90 sQ7_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f22,f73,f65])).
% 0.47/0.90 fof(f77,definition,(
% 0.47/0.90 sQ8_spl <=> (le(sK1_skl,n))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f80,plain,(
% 0.47/0.90 sQ8_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f23,f77,f65])).
% 0.47/0.90 fof(f81,definition,(
% 0.47/0.90 sQ9_spl <=> (le(s(perm(sK1_skl)),perm(sK0_skl)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f82,plain,(
% 0.47/0.90 le(s(perm(sK1_skl)),perm(sK0_skl))|~sQ9_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f81])).
% 0.47/0.90 fof(f84,plain,(
% 0.47/0.90 ~sQ7_spl|sQ9_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f24,f73,f81,f65])).
% 0.47/0.90 fof(f86,definition,(
% 0.47/0.90 sQ10_spl <=> (q(sK0_skl)=q(sK1_skl))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f87,plain,(
% 0.47/0.90 q(sK0_skl)=q(sK1_skl)|~sQ10_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f86])).
% 0.47/0.90 fof(f89,definition,(
% 0.47/0.90 sQ11_spl <=> (plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f90,plain,(
% 0.47/0.90 plus(q(sK0_skl),sK0_skl)=plus(q(sK1_skl),sK1_skl)|~sQ11_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f89])).
% 0.47/0.90 fof(f92,definition,(
% 0.47/0.90 sQ12_spl <=> (minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f93,plain,(
% 0.47/0.90 minus(q(sK0_skl),sK0_skl)=minus(q(sK1_skl),sK1_skl)|~sQ12_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f92])).
% 0.47/0.90 fof(f95,plain,(
% 0.47/0.90 sQ10_spl|sQ11_spl|sQ12_spl|sQ5_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f26,f86,f89,f92,f65])).
% 0.47/0.90 fof(f96,plain,(
% 0.47/0.90 $false|~sQ5_spl),
% 0.47/0.90 inference(forward_subsumption_resolution,[status(thm)],[f66,f30])).
% 0.47/0.90 fof(f97,plain,(
% 0.47/0.90 ~sQ5_spl),
% 0.47/0.90 inference(contradiction_clause,[status(thm)],[f96])).
% 0.47/0.90 fof(f98,plain,(
% 0.47/0.90 $false|sQ0_spl),
% 0.47/0.90 inference(forward_subsumption_resolution,[status(thm)],[f49,f28])).
% 0.47/0.90 fof(f99,plain,(
% 0.47/0.90 sQ0_spl),
% 0.47/0.90 inference(contradiction_clause,[status(thm)],[f98])).
% 0.47/0.90 fof(f113,plain,(
% 0.47/0.90 ~le(sK0_skl,n)|le(perm(sK0_skl),n)|~sQ4_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f33,f63])).
% 0.47/0.90 fof(f115,definition,(
% 0.47/0.90 sQ16_spl <=> (le(perm(sK0_skl),n))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f118,plain,(
% 0.47/0.90 ~sQ6_spl|sQ16_spl|~sQ4_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f113,f69,f115,f62])).
% 0.47/0.90 fof(f123,plain,(
% 0.47/0.90 ![X0]: (~le(sK0_skl,X0)|le(s(n0),X0)|~sQ4_spl)),
% 0.47/0.90 inference(resolution,[status(thm)],[f37,f63])).
% 0.47/0.90 fof(f131,plain,(
% 0.47/0.90 ![X0]: (~le(X0,s(sK0_skl))|le(X0,sK1_skl)|~sQ7_spl)),
% 0.47/0.90 inference(resolution,[status(thm)],[f74,f37])).
% 0.47/0.90 fof(f140,plain,(
% 0.47/0.90 ~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),
% 0.47/0.90 inference(resolution,[status(thm)],[f51,f82])).
% 0.47/0.90 fof(f152,definition,(
% 0.47/0.90 sQ20_spl <=> (le(s(n0),perm(sK1_skl)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f155,definition,(
% 0.47/0.90 sQ21_spl <=> (le(perm(sK1_skl),n))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f158,definition,(
% 0.47/0.90 sQ22_spl <=> (p(perm(sK1_skl))=p(perm(sK0_skl)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f160,plain,(
% 0.47/0.90 ~p(perm(sK1_skl))=p(perm(sK0_skl))|sQ22_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f158])).
% 0.47/0.90 fof(f161,plain,(
% 0.47/0.90 ~sQ20_spl|~sQ21_spl|~sQ16_spl|~sQ22_spl|~sQ1_spl|~sQ9_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f140,f152,f155,f115,f158,f50,f81])).
% 0.47/0.90 fof(f176,plain,(
% 0.47/0.90 ~q(sK1_skl)=p(perm(sK0_skl))|sQ22_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f160])).
% 0.47/0.90 fof(f177,plain,(
% 0.47/0.90 ~q(sK1_skl)=q(sK0_skl)|sQ22_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f176])).
% 0.47/0.90 fof(f189,plain,(
% 0.47/0.90 ![X0,X1,X2,X3]: (plus(X0,perm(X1))=plus(X2,perm(X3))|~minus(X0,X2)=minus(X1,X3))),
% 0.47/0.90 inference(paramodulation,[status(thm)],[f34,f42])).
% 0.47/0.90 fof(f192,plain,(
% 0.47/0.90 minus(q(sK0_skl),q(sK1_skl))=minus(sK0_skl,sK1_skl)|~sQ12_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f45,f93])).
% 0.47/0.90 fof(f200,plain,(
% 0.47/0.90 ![X0,X1,X2,X3]: (~minus(X0,X1)=minus(X2,X3)|minus(X0,perm(X3))=minus(X1,perm(X2)))),
% 0.47/0.90 inference(paramodulation,[status(thm)],[f34,f45])).
% 0.47/0.90 fof(f206,plain,(
% 0.47/0.90 ~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),
% 0.47/0.90 inference(resolution,[status(thm)],[f55,f82])).
% 0.47/0.90 fof(f218,definition,(
% 0.47/0.90 sQ29_spl <=> (plus(p(perm(sK1_skl)),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f220,plain,(
% 0.47/0.90 ~plus(p(perm(sK1_skl)),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl))|sQ29_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f218])).
% 0.47/0.90 fof(f221,plain,(
% 0.47/0.90 ~sQ20_spl|~sQ21_spl|~sQ16_spl|~sQ29_spl|~sQ2_spl|~sQ9_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f206,f152,f155,f115,f218,f54,f81])).
% 0.47/0.90 fof(f230,plain,(
% 0.47/0.90 ~plus(q(sK1_skl),perm(sK1_skl))=plus(p(perm(sK0_skl)),perm(sK0_skl))|sQ29_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f220])).
% 0.47/0.90 fof(f231,plain,(
% 0.47/0.90 ~plus(q(sK1_skl),perm(sK1_skl))=plus(q(sK0_skl),perm(sK0_skl))|sQ29_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f230])).
% 0.47/0.90 fof(f234,plain,(
% 0.47/0.90 ~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),
% 0.47/0.90 inference(resolution,[status(thm)],[f59,f82])).
% 0.47/0.90 fof(f246,definition,(
% 0.47/0.90 sQ34_spl <=> (minus(p(perm(sK1_skl)),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl)))),
% 0.47/0.90 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.47/0.90 fof(f248,plain,(
% 0.47/0.90 ~minus(p(perm(sK1_skl)),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl))|sQ34_spl),
% 0.47/0.90 inference(component_clause,[status(thm)],[f246])).
% 0.47/0.90 fof(f249,plain,(
% 0.47/0.90 ~sQ20_spl|~sQ21_spl|~sQ16_spl|~sQ34_spl|~sQ3_spl|~sQ9_spl),
% 0.47/0.90 inference(split_clause,[status(thm)],[f234,f152,f155,f115,f246,f58,f81])).
% 0.47/0.90 fof(f258,plain,(
% 0.47/0.90 ~minus(q(sK1_skl),perm(sK1_skl))=minus(p(perm(sK0_skl)),perm(sK0_skl))|sQ34_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f248])).
% 0.47/0.90 fof(f259,plain,(
% 0.47/0.90 ~minus(q(sK1_skl),perm(sK1_skl))=minus(q(sK0_skl),perm(sK0_skl))|sQ34_spl),
% 0.47/0.90 inference(forward_demodulation,[status(thm)],[f29,f258])).
% 0.47/0.90 fof(f397,plain,(
% 0.47/0.90 le(sK0_skl,sK1_skl)|~sQ7_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f131,f38])).
% 0.47/0.90 fof(f421,plain,(
% 0.47/0.90 le(s(n0),sK1_skl)|~sQ4_spl|~sQ7_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f123,f397])).
% 0.47/0.90 fof(f489,plain,(
% 0.47/0.90 ~le(sK1_skl,n)|le(perm(sK1_skl),n)|~sQ4_spl|~sQ7_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f421,f33])).
% 0.47/0.90 fof(f490,plain,(
% 0.47/0.90 ~le(sK1_skl,n)|le(s(n0),perm(sK1_skl))|~sQ4_spl|~sQ7_spl),
% 0.47/0.90 inference(resolution,[status(thm)],[f421,f32])).
% 0.47/0.91 fof(f510,plain,(
% 0.47/0.91 ~sQ8_spl|sQ21_spl|~sQ4_spl|~sQ7_spl),
% 0.47/0.91 inference(split_clause,[status(thm)],[f489,f77,f155,f62,f73])).
% 0.47/0.91 fof(f511,plain,(
% 0.47/0.91 ~sQ8_spl|sQ20_spl|~sQ4_spl|~sQ7_spl),
% 0.47/0.91 inference(split_clause,[status(thm)],[f490,f77,f152,f62,f73])).
% 0.47/0.91 fof(f702,definition,(
% 0.47/0.91 sQ90_spl <=> (minus(q(sK0_skl),sK0_skl)=minus(q(sK0_skl),sK0_skl))),
% 0.47/0.91 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.47/0.91 fof(f704,plain,(
% 0.47/0.91 ~minus(q(sK0_skl),sK0_skl)=minus(q(sK0_skl),sK0_skl)|sQ90_spl),
% 0.47/0.91 inference(component_clause,[status(thm)],[f702])).
% 0.47/0.91 fof(f716,plain,(
% 0.47/0.91 $false|sQ90_spl),
% 0.47/0.91 inference(trivial_equality_resolution,[status(thm)],[f704])).
% 0.47/0.91 fof(f717,plain,(
% 0.47/0.91 sQ90_spl),
% 0.47/0.91 inference(contradiction_clause,[status(thm)],[f716])).
% 0.47/0.91 fof(f1545,definition,(
% 0.47/0.91 sQ153_spl <=> (plus(sK1_skl,sK1_skl)=plus(sK1_skl,sK1_skl))),
% 0.47/0.91 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.47/0.91 fof(f1547,plain,(
% 0.47/0.91 ~plus(sK1_skl,sK1_skl)=plus(sK1_skl,sK1_skl)|sQ153_spl),
% 0.47/0.91 inference(component_clause,[status(thm)],[f1545])).
% 0.47/0.91 fof(f1568,plain,(
% 0.47/0.91 $false|sQ153_spl),
% 0.47/0.91 inference(trivial_equality_resolution,[status(thm)],[f1547])).
% 0.47/0.91 fof(f1569,plain,(
% 0.47/0.91 sQ153_spl),
% 0.47/0.91 inference(contradiction_clause,[status(thm)],[f1568])).
% 0.47/0.91 fof(f1570,plain,(
% 0.47/0.91 $false|sQ22_spl|~sQ10_spl),
% 0.47/0.91 inference(forward_subsumption_resolution,[status(thm)],[f87,f177])).
% 0.47/0.91 fof(f1571,plain,(
% 0.47/0.91 sQ22_spl|~sQ10_spl),
% 0.47/0.91 inference(contradiction_clause,[status(thm)],[f1570])).
% 0.47/0.91 fof(f1572,plain,(
% 0.47/0.91 minus(q(sK0_skl),q(sK1_skl))=minus(sK1_skl,sK0_skl)|~sQ11_spl),
% 0.47/0.91 inference(resolution,[status(thm)],[f90,f41])).
% 0.47/0.91 fof(f1618,plain,(
% 0.47/0.91 minus(q(sK0_skl),perm(sK0_skl))=minus(q(sK1_skl),perm(sK1_skl))|~sQ11_spl),
% 0.47/0.91 inference(resolution,[status(thm)],[f1572,f200])).
% 0.47/0.91 fof(f1646,plain,(
% 0.47/0.91 $false|sQ34_spl|~sQ11_spl),
% 0.47/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1618,f259])).
% 0.47/0.91 fof(f1647,plain,(
% 0.47/0.91 sQ34_spl|~sQ11_spl),
% 0.47/0.91 inference(contradiction_clause,[status(thm)],[f1646])).
% 0.47/0.91 fof(f1818,plain,(
% 0.47/0.91 plus(q(sK0_skl),perm(sK0_skl))=plus(q(sK1_skl),perm(sK1_skl))|~sQ12_spl),
% 0.47/0.91 inference(resolution,[status(thm)],[f192,f189])).
% 0.47/0.91 fof(f1866,plain,(
% 0.47/0.91 ~plus(q(sK0_skl),perm(sK0_skl))=plus(q(sK0_skl),perm(sK0_skl))|~sQ12_spl|sQ29_spl),
% 0.47/0.91 inference(forward_demodulation,[status(thm)],[f1818,f231])).
% 0.47/0.91 fof(f1867,plain,(
% 0.47/0.91 $false|~sQ12_spl|sQ29_spl),
% 0.47/0.91 inference(trivial_equality_resolution,[status(thm)],[f1866])).
% 0.47/0.91 fof(f1868,plain,(
% 0.47/0.91 ~sQ12_spl|sQ29_spl),
% 0.47/0.91 inference(contradiction_clause,[status(thm)],[f1867])).
% 0.47/0.91 fof(f1869,plain,(
% 0.47/0.91 $false),
% 0.47/0.91 inference(sat_refutation,[status(thm)],[f53,f57,f61,f68,f72,f76,f80,f84,f95,f97,f99,f118,f161,f221,f249,f510,f511,f717,f1569,f1571,f1647,f1868])).
% 0.47/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 1.17/0.93 % Elapsed time: 0.479708 seconds
% 1.17/0.93 % CPU time: 3.465376 seconds
% 1.17/0.93 % Total memory used: 134.351 MB
% 1.17/0.93 % Net memory used: 129.379 MB
%------------------------------------------------------------------------------