%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ITP012+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:50:10 PM UTC 2026
% Result : Theorem 125.38s 27.93s
% Output : CNFRefutation 126.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 6 unt; 0 def)
% Number of atoms : 42 ( 28 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 21 ~; 12 |; 4 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 46 ( 40 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f138,axiom,
! [A_27a,V0x_2E0,V1y_2E0,V2z_2E0] :
( ( s(A_27a,V1y_2E0) = s(A_27a,V2z_2E0)
& s(A_27a,V0x_2E0) = s(A_27a,V1y_2E0) )
=> s(A_27a,V0x_2E0) = s(A_27a,V2z_2E0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13827,axiom,
! [V0x_2E0,V1y_2E0] : s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,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,V0x_2E0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14068,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,V1q_2E0),s(tyop_2Einteger_2Eint,V2r_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/sandbox/benchmark/theBenchmark.p') ).
fof(f14072,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/sandbox/benchmark/theBenchmark.p') ).
fof(f14073,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)],[f14072]) ).
fof(f14545,plain,
! [A_27a,V0x_2E0,V1y_2E0,V2z_2E0] :
( s(A_27a,V0x_2E0) = s(A_27a,V2z_2E0)
| s(A_27a,V1y_2E0) != s(A_27a,V2z_2E0)
| s(A_27a,V0x_2E0) != s(A_27a,V1y_2E0) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f14546,plain,
! [A_27a,V0x_2E0,V2z_2E0] :
( s(A_27a,V0x_2E0) = s(A_27a,V2z_2E0)
| ! [V1y_2E0] :
( s(A_27a,V1y_2E0) != s(A_27a,V2z_2E0)
| s(A_27a,V0x_2E0) != s(A_27a,V1y_2E0) ) ),
inference(miniscoping,[status(thm)],[f14545]) ).
fof(f14547,plain,
! [X0,X1,X2,X3] :
( s(X0,X3) != s(X0,X1)
| s(X0,X3) = s(X0,X2)
| s(X0,X1) != s(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f14546]) ).
fof(f55662,plain,
! [X0,X1] : s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,X1),s(tyop_2Einteger_2Eint,X0))))) = s(tyop_2Einteger_2Eint,X1),
inference(cnf_transformation,[status(thm)],[f13827]) ).
fof(f56312,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,V1q_2E0),s(tyop_2Einteger_2Eint,V2r_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)],[f14068]) ).
fof(f56313,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,V1q_2E0),s(tyop_2Einteger_2Eint,V2r_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)],[f56312]) ).
fof(f56314,plain,
! [X0,X1,X2] :
( ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X1))))
| 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,X1),s(tyop_2Einteger_2Eint,X2))))) = s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,X2))) ),
inference(cnf_transformation,[status(thm)],[f56313]) ).
fof(f56324,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)],[f14073]) ).
fof(f56325,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)],[f56324]) ).
fof(f56326,plain,
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK20511_skl),s(tyop_2Einteger_2Eint,sK20510_skl))))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl)))
& p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20510_skl)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20509_skl,sK20510_skl,sK20511_skl]),skolemize(V0p_2E0,sK20509_skl),skolemize(V1q_2E0,sK20510_skl),skolemize(V2r_2E0,sK20511_skl)],[f56325]) ).
fof(f56327,plain,
p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20510_skl)))),
inference(cnf_transformation,[status(thm)],[f56326]) ).
fof(f56328,plain,
s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK20511_skl),s(tyop_2Einteger_2Eint,sK20510_skl))))),
inference(cnf_transformation,[status(thm)],[f56326]) ).
fof(f64427,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,X0) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl)))
| s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK20511_skl),s(tyop_2Einteger_2Eint,sK20510_skl))))) != s(tyop_2Emin_2Ebool,X0) ),
inference(resolution,[status(thm)],[f14547,f56328]) ).
fof(f67547,plain,
! [X0] :
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__add_2E2(s(tyop_2Einteger_2Eint,X0),s(tyop_2Einteger_2Eint,c_2Einteger_2Eint__sub_2E2(s(tyop_2Einteger_2Eint,sK20511_skl),s(tyop_2Einteger_2Eint,sK20510_skl)))))))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,X0)))) ),
inference(resolution,[status(thm)],[f56314,f64427]) ).
fof(f82689,plain,
( s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl))) != s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20511_skl)))
| ~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20510_skl)))) ),
inference(paramodulation,[status(thm)],[f55662,f67547]) ).
fof(f82912,plain,
~ p(s(tyop_2Emin_2Ebool,c_2Einteger_2Eint__divides_2E2(s(tyop_2Einteger_2Eint,sK20509_skl),s(tyop_2Einteger_2Eint,sK20510_skl)))),
inference(trivial_equality_resolution,[status(thm)],[f82689]) ).
fof(f82913,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f82912,f56327]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP012+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.37 % Computer : n001.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Sun Sep 20 21:51:50 UTC 2026
% 0.08/5.37 % CPUTime :
% 7.65/13.02 % Drodi V4.1.1
% 125.38/27.93 % Refutation found
% 125.38/27.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 125.38/27.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.25/28.63 % Elapsed time: 23.212070 seconds
% 11.25/28.63 % CPU time: 126.820761 seconds
% 11.25/28.63 % Total memory used: 5.665 GB
% 11.25/28.63 % Net memory used: 5.644 GB
%------------------------------------------------------------------------------