%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM925+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 01:44:06 PM UTC 2026
% Result : Theorem 0.13s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n002.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 03:20:31 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.45 % Refutation found
% 0.13/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.45 fof(f12,hypothesis,(
% 0.13/0.45 (! [B_1] : bit0(ti(int,B_1)) = bit0(B_1) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f35,axiom,(
% 0.13/0.45 (! [X_a] :( linordered_idom(X_a)=> (! [Xa,Ya] :( plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))) = zero_zero(X_a)<=> ( ti(X_a,Xa) = zero_zero(X_a)& ti(X_a,Ya) = zero_zero(X_a) ) ) )) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f57,axiom,(
% 0.13/0.45 semiring_1_of_nat(int,one_one(nat)) = one_one(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f65,axiom,(
% 0.13/0.45 ~ ord_less(int,pls,pls) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f70,axiom,(
% 0.13/0.45 one_one(int) = number_number_of(int,bit1(pls)) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f73,axiom,(
% 0.13/0.45 (! [X_a] :( ( number_ring(X_a)& ring_char_0(X_a) )=> (! [Xa,Ya] :( number_number_of(X_a,Xa) = number_number_of(X_a,Ya)<=> Xa = Ya ) )) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f76,axiom,(
% 0.13/0.45 (! [K_1,L_1] :( bit0(K_1) = bit0(L_1)<=> K_1 = L_1 ) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f80,axiom,(
% 0.13/0.45 (! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f93,axiom,(
% 0.13/0.45 (! [Wa,Z_1] :( ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))<=> ( ord_less(int,Wa,Z_1)| Wa = Z_1 ) ) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f94,axiom,(
% 0.13/0.45 (! [K] : ~ ord_less(int,semiring_1_of_nat(int,K),zero_zero(int)) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f99,axiom,(
% 0.13/0.45 (! [K] : bit1(K) != pls )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f103,axiom,(
% 0.13/0.45 (! [K_1] :( bit0(K_1) = pls<=> K_1 = pls ) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f106,axiom,(
% 0.13/0.45 pls = zero_zero(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f109,axiom,(
% 0.13/0.45 (! [K] : plus_plus(int,pls,K) = K )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f127,axiom,(
% 0.13/0.45 (! [X_a] :( number_semiring(X_a)=> (! [N] : number_number_of(X_a,semiring_1_of_nat(int,N)) = semiring_1_of_nat(X_a,N) )) )),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f134,axiom,(
% 0.13/0.45 linordered_idom(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f135,axiom,(
% 0.13/0.45 number_semiring(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f140,axiom,(
% 0.13/0.45 ring_char_0(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f141,axiom,(
% 0.13/0.45 number_ring(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f144,axiom,(
% 0.13/0.45 no_zero_divisors(nat) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f146,axiom,(
% 0.13/0.45 zero_neq_one(nat) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f149,axiom,(
% 0.13/0.45 mult_zero(nat) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f153,conjecture,(
% 0.13/0.45 power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f154,negated_conjecture,(
% 0.13/0.45 ~(power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) )),
% 0.13/0.45 inference(negated_conjecture,[status(cth)],[f153])).
% 0.13/0.45 fof(f182,plain,(
% 0.13/0.45 ![X0]: (bit0(ti(int,X0))=bit0(X0))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.45 fof(f239,plain,(
% 0.13/0.45 ![X_a]: (~linordered_idom(X_a)|(![Xa,Ya]: (plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)<=>(ti(X_a,Xa)=zero_zero(X_a)&ti(X_a,Ya)=zero_zero(X_a)))))),
% 0.13/0.45 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.13/0.45 fof(f240,plain,(
% 0.13/0.45 ![X_a]: (~linordered_idom(X_a)|(![Xa,Ya]: ((~plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)|(ti(X_a,Xa)=zero_zero(X_a)&ti(X_a,Ya)=zero_zero(X_a)))&(plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)|(~ti(X_a,Xa)=zero_zero(X_a)|~ti(X_a,Ya)=zero_zero(X_a))))))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f239])).
% 0.13/0.45 fof(f241,plain,(
% 0.13/0.45 ![X_a]: (~linordered_idom(X_a)|((![Xa,Ya]: (~plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)|(ti(X_a,Xa)=zero_zero(X_a)&ti(X_a,Ya)=zero_zero(X_a))))&(![Xa,Ya]: (plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)|(~ti(X_a,Xa)=zero_zero(X_a)|~ti(X_a,Ya)=zero_zero(X_a))))))),
% 0.13/0.45 inference(miniscoping,[status(thm)],[f240])).
% 0.13/0.45 fof(f242,plain,(
% 0.13/0.45 ![X0,X1,X2]: (~linordered_idom(X0)|~plus_plus(X0,power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))),power_power(X0,X2,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X0)|ti(X0,X1)=zero_zero(X0))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f241])).
% 0.13/0.45 fof(f288,plain,(
% 0.13/0.45 semiring_1_of_nat(int,one_one(nat))=one_one(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.45 fof(f305,plain,(
% 0.13/0.45 ~ord_less(int,pls,pls)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/0.45 fof(f322,plain,(
% 0.13/0.45 one_one(int)=number_number_of(int,bit1(pls))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f70])).
% 0.13/0.45 fof(f325,plain,(
% 0.13/0.45 ![X_a]: ((~number_ring(X_a)|~ring_char_0(X_a))|(![Xa,Ya]: (number_number_of(X_a,Xa)=number_number_of(X_a,Ya)<=>Xa=Ya)))),
% 0.13/0.45 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.13/0.45 fof(f326,plain,(
% 0.13/0.45 ![X_a]: ((~number_ring(X_a)|~ring_char_0(X_a))|(![Xa,Ya]: ((~number_number_of(X_a,Xa)=number_number_of(X_a,Ya)|Xa=Ya)&(number_number_of(X_a,Xa)=number_number_of(X_a,Ya)|~Xa=Ya))))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f325])).
% 0.13/0.45 fof(f327,plain,(
% 0.13/0.45 ![X_a]: ((~number_ring(X_a)|~ring_char_0(X_a))|((![Xa,Ya]: (~number_number_of(X_a,Xa)=number_number_of(X_a,Ya)|Xa=Ya))&(![Xa,Ya]: (number_number_of(X_a,Xa)=number_number_of(X_a,Ya)|~Xa=Ya))))),
% 0.13/0.45 inference(miniscoping,[status(thm)],[f326])).
% 0.13/0.45 fof(f328,plain,(
% 0.13/0.45 ![X0,X1,X2]: (~number_ring(X0)|~ring_char_0(X0)|~number_number_of(X0,X1)=number_number_of(X0,X2)|X1=X2)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f327])).
% 0.13/0.45 fof(f339,plain,(
% 0.13/0.45 ![K_1,L_1]: ((~bit0(K_1)=bit0(L_1)|K_1=L_1)&(bit0(K_1)=bit0(L_1)|~K_1=L_1))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f76])).
% 0.13/0.45 fof(f340,plain,(
% 0.13/0.45 (![K_1,L_1]: (~bit0(K_1)=bit0(L_1)|K_1=L_1))&(![K_1,L_1]: (bit0(K_1)=bit0(L_1)|~K_1=L_1))),
% 0.13/0.45 inference(miniscoping,[status(thm)],[f339])).
% 0.13/0.45 fof(f341,plain,(
% 0.13/0.45 ![X0,X1]: (~bit0(X0)=bit0(X1)|X0=X1)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f340])).
% 0.13/0.45 fof(f350,plain,(
% 0.13/0.45 ![X0,X1]: (plus_plus(int,X0,X1)=plus_plus(int,X1,X0))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.45 fof(f395,plain,(
% 0.13/0.45 ![Wa,Z_1]: ((~ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|(ord_less(int,Wa,Z_1)|Wa=Z_1))&(ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|(~ord_less(int,Wa,Z_1)&~Wa=Z_1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f93])).
% 0.13/0.45 fof(f396,plain,(
% 0.13/0.45 (![Wa,Z_1]: (~ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|(ord_less(int,Wa,Z_1)|Wa=Z_1)))&(![Wa,Z_1]: (ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|(~ord_less(int,Wa,Z_1)&~Wa=Z_1)))),
% 0.13/0.45 inference(miniscoping,[status(thm)],[f395])).
% 0.13/0.45 fof(f399,plain,(
% 0.13/0.45 ![X0,X1]: (ord_less(int,X0,plus_plus(int,X1,one_one(int)))|~X0=X1)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f396])).
% 0.13/0.45 fof(f400,plain,(
% 0.13/0.45 ![X0]: (~ord_less(int,semiring_1_of_nat(int,X0),zero_zero(int)))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/0.45 fof(f420,plain,(
% 0.13/0.45 ![X0]: (~bit1(X0)=pls)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f99])).
% 0.13/0.45 fof(f424,plain,(
% 0.13/0.45 ![K_1]: ((~bit0(K_1)=pls|K_1=pls)&(bit0(K_1)=pls|~K_1=pls))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f103])).
% 0.13/0.45 fof(f425,plain,(
% 0.13/0.45 (![K_1]: (~bit0(K_1)=pls|K_1=pls))&(![K_1]: (bit0(K_1)=pls|~K_1=pls))),
% 0.13/0.45 inference(miniscoping,[status(thm)],[f424])).
% 0.13/0.45 fof(f427,plain,(
% 0.13/0.45 ![X0]: (bit0(X0)=pls|~X0=pls)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f425])).
% 0.13/0.45 fof(f433,plain,(
% 0.13/0.45 pls=zero_zero(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f106])).
% 0.13/0.45 fof(f436,plain,(
% 0.13/0.45 ![X0]: (plus_plus(int,pls,X0)=X0)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f109])).
% 0.13/0.45 fof(f467,plain,(
% 0.13/0.45 ![X_a]: (~number_semiring(X_a)|(![N]: number_number_of(X_a,semiring_1_of_nat(int,N))=semiring_1_of_nat(X_a,N)))),
% 0.13/0.45 inference(pre_NNF_transformation,[status(thm)],[f127])).
% 0.13/0.45 fof(f468,plain,(
% 0.13/0.45 ![X0,X1]: (~number_semiring(X0)|number_number_of(X0,semiring_1_of_nat(int,X1))=semiring_1_of_nat(X0,X1))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f467])).
% 0.13/0.45 fof(f485,plain,(
% 0.13/0.45 linordered_idom(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f134])).
% 0.13/0.45 fof(f486,plain,(
% 0.13/0.45 number_semiring(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f135])).
% 0.13/0.45 fof(f491,plain,(
% 0.13/0.45 ring_char_0(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f140])).
% 0.13/0.45 fof(f492,plain,(
% 0.13/0.45 number_ring(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.45 fof(f495,plain,(
% 0.13/0.45 no_zero_divisors(nat)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f144])).
% 0.13/0.45 fof(f497,plain,(
% 0.13/0.45 zero_neq_one(nat)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f146])).
% 0.13/0.45 fof(f500,plain,(
% 0.13/0.45 mult_zero(nat)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f149])).
% 0.13/0.45 fof(f504,plain,(
% 0.13/0.45 power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls))))=zero_zero(int)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f154])).
% 0.13/0.45 fof(f506,plain,(
% 0.13/0.45 ![X0]: (ord_less(int,X0,plus_plus(int,X0,one_one(int))))),
% 0.13/0.45 inference(destructive_equality_resolution,[status(thm)],[f399])).
% 0.13/0.45 fof(f507,plain,(
% 0.13/0.45 bit0(pls)=pls),
% 0.13/0.45 inference(destructive_equality_resolution,[status(thm)],[f427])).
% 0.13/0.45 fof(f510,plain,(
% 0.13/0.45 power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls))))=pls),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f433,f504])).
% 0.13/0.45 fof(f562,plain,(
% 0.13/0.45 ![X0]: (ti(int,X0)=X0)),
% 0.13/0.45 inference(resolution,[status(thm)],[f182,f341])).
% 0.13/0.45 fof(f637,plain,(
% 0.13/0.45 ![X0]: (~ord_less(int,semiring_1_of_nat(int,X0),pls))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f433,f400])).
% 0.13/0.45 fof(f698,definition,(
% 0.13/0.45 sQ10_spl <=> (mult_zero(nat))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f700,plain,(
% 0.13/0.45 ~mult_zero(nat)|sQ10_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f698])).
% 0.13/0.45 fof(f701,definition,(
% 0.13/0.45 sQ11_spl <=> (no_zero_divisors(nat))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f703,plain,(
% 0.13/0.45 ~no_zero_divisors(nat)|sQ11_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f701])).
% 0.13/0.45 fof(f704,definition,(
% 0.13/0.45 sQ12_spl <=> (zero_neq_one(nat))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f706,plain,(
% 0.13/0.45 ~zero_neq_one(nat)|sQ12_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f704])).
% 0.13/0.45 fof(f741,plain,(
% 0.13/0.45 ![X0]: (ord_less(int,X0,plus_plus(int,one_one(int),X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f350,f506])).
% 0.13/0.45 fof(f873,plain,(
% 0.13/0.45 ![X0]: (number_number_of(int,semiring_1_of_nat(int,X0))=semiring_1_of_nat(int,X0))),
% 0.13/0.45 inference(resolution,[status(thm)],[f468,f486])).
% 0.13/0.45 fof(f878,plain,(
% 0.13/0.45 number_number_of(int,one_one(int))=semiring_1_of_nat(int,one_one(nat))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f288,f873])).
% 0.13/0.45 fof(f886,plain,(
% 0.13/0.45 number_number_of(int,one_one(int))=one_one(int)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f288,f878])).
% 0.13/0.45 fof(f899,definition,(
% 0.13/0.45 sQ20_spl <=> (linordered_idom(int))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f901,plain,(
% 0.13/0.45 ~linordered_idom(int)|sQ20_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f899])).
% 0.13/0.45 fof(f931,plain,(
% 0.13/0.45 $false|sQ20_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f901,f485])).
% 0.13/0.45 fof(f932,plain,(
% 0.13/0.45 sQ20_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f931])).
% 0.13/0.45 fof(f1235,plain,(
% 0.13/0.45 ![X0]: (~number_ring(int)|~ring_char_0(int)|~one_one(int)=number_number_of(int,X0)|one_one(int)=X0)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f886,f328])).
% 0.13/0.45 fof(f1265,definition,(
% 0.13/0.45 sQ65_spl <=> (number_ring(int))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f1267,plain,(
% 0.13/0.45 ~number_ring(int)|sQ65_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f1265])).
% 0.13/0.45 fof(f1268,definition,(
% 0.13/0.45 sQ66_spl <=> (ring_char_0(int))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f1270,plain,(
% 0.13/0.45 ~ring_char_0(int)|sQ66_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f1268])).
% 0.13/0.45 fof(f1271,definition,(
% 0.13/0.45 ![X0]: (sQ67_spl <=> (~one_one(int)=number_number_of(int,X0)|one_one(int)=X0))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f1272,plain,(
% 0.13/0.45 ![X0]: (~one_one(int)=number_number_of(int,X0)|one_one(int)=X0|~sQ67_spl)),
% 0.13/0.45 inference(component_clause,[status(thm)],[f1271])).
% 0.13/0.45 fof(f1274,plain,(
% 0.13/0.45 ~sQ65_spl|~sQ66_spl|sQ67_spl),
% 0.13/0.45 inference(split_clause,[status(thm)],[f1235,f1265,f1268,f1271])).
% 0.13/0.45 fof(f1301,plain,(
% 0.13/0.45 $false|sQ66_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1270,f491])).
% 0.13/0.45 fof(f1302,plain,(
% 0.13/0.45 sQ66_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1301])).
% 0.13/0.45 fof(f1303,plain,(
% 0.13/0.45 $false|sQ65_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1267,f492])).
% 0.13/0.45 fof(f1304,plain,(
% 0.13/0.45 sQ65_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1303])).
% 0.13/0.45 fof(f1313,definition,(
% 0.13/0.45 sQ73_spl <=> (pls=bit1(pls))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f1314,plain,(
% 0.13/0.45 pls=bit1(pls)|~sQ73_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f1313])).
% 0.13/0.45 fof(f1318,plain,(
% 0.13/0.45 one_one(int)=bit1(pls)|~sQ67_spl),
% 0.13/0.45 inference(resolution,[status(thm)],[f1272,f322])).
% 0.13/0.45 fof(f1338,plain,(
% 0.13/0.45 ![X0]: (ord_less(int,X0,plus_plus(int,bit1(pls),X0))|~sQ67_spl)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f1318,f741])).
% 0.13/0.45 fof(f1347,plain,(
% 0.13/0.45 power_power(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls))))=pls|~sQ67_spl),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f1318,f510])).
% 0.13/0.45 fof(f1376,plain,(
% 0.13/0.45 $false|~sQ73_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1314,f420])).
% 0.13/0.45 fof(f1377,plain,(
% 0.13/0.45 ~sQ73_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1376])).
% 0.13/0.45 fof(f1407,plain,(
% 0.13/0.45 $false|sQ12_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f706,f497])).
% 0.13/0.45 fof(f1408,plain,(
% 0.13/0.45 sQ12_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1407])).
% 0.13/0.45 fof(f1409,plain,(
% 0.13/0.45 $false|sQ11_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f703,f495])).
% 0.13/0.45 fof(f1410,plain,(
% 0.13/0.45 sQ11_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1409])).
% 0.13/0.45 fof(f1411,plain,(
% 0.13/0.45 $false|sQ10_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f700,f500])).
% 0.13/0.45 fof(f1412,plain,(
% 0.13/0.45 sQ10_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1411])).
% 0.13/0.45 fof(f1977,definition,(
% 0.13/0.45 sQ117_spl <=> (ord_less(int,pls,bit0(pls)))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f1978,plain,(
% 0.13/0.45 ord_less(int,pls,bit0(pls))|~sQ117_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f1977])).
% 0.13/0.45 fof(f1995,plain,(
% 0.13/0.45 ord_less(int,pls,pls)|~sQ117_spl),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f507,f1978])).
% 0.13/0.45 fof(f1996,plain,(
% 0.13/0.45 $false|~sQ117_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1995,f305])).
% 0.13/0.45 fof(f1997,plain,(
% 0.13/0.45 ~sQ117_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f1996])).
% 0.13/0.45 fof(f2093,plain,(
% 0.13/0.45 ![X0]: (~linordered_idom(int)|~plus_plus(int,pls,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(int)|ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)))=zero_zero(int)|~sQ67_spl)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f1347,f242])).
% 0.13/0.45 fof(f2106,definition,(
% 0.13/0.45 ![X0]: (sQ127_spl <=> (~plus_plus(int,pls,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(int)))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f2107,plain,(
% 0.13/0.45 ![X0]: (~plus_plus(int,pls,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(int)|~sQ127_spl)),
% 0.13/0.45 inference(component_clause,[status(thm)],[f2106])).
% 0.13/0.45 fof(f2109,definition,(
% 0.13/0.45 sQ128_spl <=> (ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)))=zero_zero(int))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.13/0.45 fof(f2110,plain,(
% 0.13/0.45 ti(int,plus_plus(int,bit1(pls),semiring_1_of_nat(int,n)))=zero_zero(int)|~sQ128_spl),
% 0.13/0.45 inference(component_clause,[status(thm)],[f2109])).
% 0.13/0.45 fof(f2112,plain,(
% 0.13/0.45 ~sQ20_spl|sQ127_spl|sQ128_spl|~sQ67_spl),
% 0.13/0.45 inference(split_clause,[status(thm)],[f2093,f899,f2106,f2109,f1271])).
% 0.13/0.45 fof(f2141,plain,(
% 0.13/0.45 ![X0]: (~power_power(int,X0,number_number_of(nat,bit0(bit1(pls))))=zero_zero(int)|~sQ127_spl)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f436,f2107])).
% 0.13/0.45 fof(f2142,plain,(
% 0.13/0.45 ![X0]: (~power_power(int,X0,number_number_of(nat,bit0(bit1(pls))))=pls|~sQ127_spl)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f433,f2141])).
% 0.13/0.45 fof(f2172,plain,(
% 0.13/0.45 plus_plus(int,bit1(pls),semiring_1_of_nat(int,n))=zero_zero(int)|~sQ128_spl),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f562,f2110])).
% 0.13/0.45 fof(f2173,plain,(
% 0.13/0.45 plus_plus(int,bit1(pls),semiring_1_of_nat(int,n))=pls|~sQ128_spl),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f433,f2172])).
% 0.13/0.45 fof(f2196,plain,(
% 0.13/0.45 ord_less(int,semiring_1_of_nat(int,n),pls)|~sQ67_spl|~sQ128_spl),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f2173,f1338])).
% 0.13/0.45 fof(f2200,plain,(
% 0.13/0.45 $false|~sQ67_spl|~sQ128_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f2196,f637])).
% 0.13/0.45 fof(f2201,plain,(
% 0.13/0.45 ~sQ67_spl|~sQ128_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f2200])).
% 0.13/0.45 fof(f2207,plain,(
% 0.13/0.45 $false|~sQ127_spl|~sQ67_spl),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1347,f2142])).
% 0.13/0.45 fof(f2208,plain,(
% 0.13/0.45 ~sQ127_spl|~sQ67_spl),
% 0.13/0.45 inference(contradiction_clause,[status(thm)],[f2207])).
% 0.13/0.45 fof(f2209,plain,(
% 0.13/0.45 $false),
% 0.13/0.45 inference(sat_refutation,[status(thm)],[f932,f1274,f1302,f1304,f1377,f1408,f1410,f1412,f1997,f2112,f2201,f2208])).
% 0.13/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.48 % Elapsed time: 0.114113 seconds
% 0.13/0.48 % CPU time: 0.513636 seconds
% 0.13/0.48 % Total memory used: 117.949 MB
% 0.13/0.48 % Net memory used: 117.420 MB
%------------------------------------------------------------------------------