%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ITP012+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:50:09 PM UTC 2026
% Result : Theorem 13.39s 2.17s
% Output : CNFRefutation 13.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 15
% Syntax : Number of formulae : 62 ( 13 unt; 6 def)
% Number of atoms : 158 ( 35 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 150 ( 54 ~; 63 |; 18 &)
% ( 10 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 72 ( 66 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V0_2E0,V1_2E0] :
( ( p(s(tyop_2Emin_2Ebool,V0_2E0))
<=> p(s(tyop_2Emin_2Ebool,V1_2E0)) )
=> s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [V0t_2E0] :
( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ! [V0t_2E0] :
( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
<=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [V0x_2E0,V1y_2E0] : s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,V0x_2E0),s(tyop_2Einteger_2Eint,V1y_2E0))) = s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,V0x_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,V1y_2E0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [V0p_2E0,V1q_2E0,V2r_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))
=> s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [V0p_2E0,V1q_2E0] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,V0p_2E0))),s(tyop_2Einteger_2Eint,V1q_2E0))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))
& s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,conjecture,
! [V0p_2E0,V1q_2E0,V2r_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))
=> s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ ! [V0p_2E0,V1q_2E0,V2r_2E0] :
( p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))
=> s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0))) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f57,plain,
! [V0_2E0,V1_2E0] :
( s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0)
| ( p(s(tyop_2Emin_2Ebool,V0_2E0))
<~> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f58,plain,
! [V0_2E0,V1_2E0] :
( s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0)
| ( ( ~ p(s(tyop_2Emin_2Ebool,V1_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V1_2E0))
| p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,X1)
| p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,X1)
| ~ p(s(tyop_2Emin_2Ebool,X1))
| ~ p(s(tyop_2Emin_2Ebool,X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f61,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f63,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)
| s(tyop_2Emin_2Ebool,X0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f131,plain,
p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f160,plain,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ! [V0t_2E0] :
( ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f161,plain,
( ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) )
& ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) )
& ! [V0t_2E0] :
( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0))
| p(s(tyop_2Emin_2Ebool,V0t_2E0)) )
& ! [V0t_2E0] :
( p(s(tyop_2Emin_2Ebool,V0t_2E0))
| ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f165,plain,
( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f216,plain,
! [X0,X1] : s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X1))) = s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,X1))))),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f217,plain,
! [V0p_2E0,V1q_2E0,V2r_2E0] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f218,plain,
! [V0p_2E0,V1q_2E0] :
( ! [V2r_2E0] : s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))) ),
inference(miniscoping,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1,X2] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,X2),s(tyop_2Einteger_2Eint,X1))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X2)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X1)))) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
( ! [V0p_2E0,V1q_2E0] : s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,V0p_2E0))),s(tyop_2Einteger_2Eint,V1q_2E0))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))
& ! [V0p_2E0,V1q_2E0] : s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,V1q_2E0))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f221,plain,
! [X0,X1] : s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,X1))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X1))),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f306,plain,
? [V0p_2E0,V1q_2E0,V2r_2E0] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0)))
& p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f307,plain,
? [V0p_2E0,V1q_2E0] :
( ? [V2r_2E0] : s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,V2r_2E0),s(tyop_2Einteger_2Eint,V1q_2E0))))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V2r_2E0)))
& p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,V0p_2E0),s(tyop_2Einteger_2Eint,V1q_2E0)))) ),
inference(miniscoping,[status(thm)],[f306]) ).
fof(f308,plain,
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK11_skl),s(tyop_2Einteger_2Eint,sK10_skl))))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK11_skl)))
& p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(V0p_2E0,sK9_skl),skolemize(V1q_2E0,sK10_skl),skolemize(V2r_2E0,sK11_skl)],[f307]) ).
fof(f309,plain,
p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl)))),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f310,plain,
s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK11_skl),s(tyop_2Einteger_2Eint,sK10_skl))))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK11_skl))),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f423,definition,
( sQ0_spl
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f434,definition,
( sQ3_spl
<=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( ~ sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f165,f434,f423]) ).
fof(f520,plain,
! [X0,X1,X2] :
( p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X2))
| s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X1)
| p(s(tyop_2Emin_2Ebool,X1))
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(paramodulation,[status(thm)],[f59,f59]) ).
fof(f525,plain,
! [X0] :
( p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl))))
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(paramodulation,[status(thm)],[f59,f309]) ).
fof(f536,definition,
! [X0] :
( sQ15_spl
<=> ( p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f537,plain,
! [X0] :
( ~ sQ15_spl
| p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,definition,
! [X1,X2] :
( sQ16_spl
<=> ( p(s(tyop_2Emin_2Ebool,X2))
| s(tyop_2Emin_2Ebool,X2) = s(tyop_2Emin_2Ebool,X1)
| p(s(tyop_2Emin_2Ebool,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f540,plain,
! [X0,X1] :
( ~ sQ16_spl
| p(s(tyop_2Emin_2Ebool,X1))
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X0)
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f520,f536,f539]) ).
fof(f550,definition,
( sQ18_spl
<=> p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f551,plain,
( ~ sQ18_spl
| p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl)))) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( sQ18_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f525,f536,f550]) ).
fof(f556,plain,
! [X0] :
( ~ sQ15_spl
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f537]) ).
fof(f557,plain,
! [X0,X1] :
( ~ sQ15_spl
| s(tyop_2Emin_2Ebool,X1) = s(tyop_2Emin_2Ebool,X0)
| ~ p(s(tyop_2Emin_2Ebool,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f60,f556]) ).
fof(f558,plain,
( ~ sQ15_spl
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK11_skl)))) ),
inference(resolution,[status(thm)],[f557,f310]) ).
fof(f560,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f558,f556]) ).
fof(f561,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f629,plain,
! [X0] :
( ~ sQ16_spl
| p(s(tyop_2Emin_2Ebool,X0))
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0))
| p(s(tyop_2Emin_2Ebool,X0)) ),
inference(paramodulation,[status(thm)],[f540,f131]) ).
fof(f631,plain,
( ~ sQ16_spl
| sQ3_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f629,f536,f434,f539]) ).
fof(f640,plain,
( ~ sQ18_spl
| s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)
| p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
inference(paramodulation,[status(thm)],[f63,f551]) ).
fof(f674,definition,
( sQ25_spl
<=> s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f675,plain,
( ~ sQ25_spl
| s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl))) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) ),
inference(component_clause,[status(thm)],[f674]) ).
fof(f677,plain,
( ~ sQ18_spl
| sQ25_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f640,f423,f674,f550]) ).
fof(f7988,plain,
! [X0,X1,X2] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,X2),s(tyop_2Einteger_2Eint,X1))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X2)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__neg_2E1(s(tyop_2Einteger_2Eint,X1)))))) ),
inference(paramodulation,[status(thm)],[f216,f219]) ).
fof(f10095,plain,
! [X0,X1,X2] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,X2),s(tyop_2Einteger_2Eint,X1))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X2)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X1)))) ),
inference(forward_demodulation,[status(thm)],[f221,f7988]) ).
fof(f10096,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK9_skl),s(tyop_2Einteger_2Eint,sK10_skl)))),
inference(resolution,[status(thm)],[f10095,f310]) ).
fof(f10143,plain,
( ~ sQ25_spl
| ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ),
inference(forward_demodulation,[status(thm)],[f675,f10096]) ).
fof(f10144,plain,
( ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10143,f61]) ).
fof(f10145,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f10144]) ).
fof(f10146,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f542,f553,f561,f631,f677,f10145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP012+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 21:47:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 13.39/2.17 % Refutation found
% 13.39/2.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.39/2.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.39/2.23 % Elapsed time: 1.851864 seconds
% 13.39/2.23 % CPU time: 14.320308 seconds
% 13.39/2.23 % Total memory used: 352.873 MB
% 13.39/2.23 % Net memory used: 344.629 MB
%------------------------------------------------------------------------------