%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW473+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 03:07:58 PM UTC 2026
% Result : Theorem 0.26s 0.60s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 31 ( 17 unt; 0 def)
% Number of atoms : 49 ( 8 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 38 ( 20 ~; 14 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-2 aty)
% Number of variables : 50 ( 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f412,axiom,
! [X_1] : hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),X_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f459,axiom,
! [Z_2,X_1,Y_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Y_1))
=> ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,Y_1),Z_2))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Z_2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f571,axiom,
! [A_2,C_11,D_4] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_11),D_4))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),C_11)),hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),D_4))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f575,axiom,
! [F,A_2,B] : image_pname_a(F,hAPP_f759274231e_bool(hAPP_p905327722e_bool(insert_pname,A_2),B)) = hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(F,A_2)),image_pname_a(F,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f577,axiom,
! [F,X_1,A] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A))
=> hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A)) = image_pname_a(F,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1410,hypothesis,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1413,hypothesis,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1415,conjecture,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1416,negated_conjecture,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(negated_conjecture,[status(cth)],[f1415]) ).
fof(f2695,plain,
! [X0] : hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X0)),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f2835,plain,
! [Z_2,X_1,Y_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Z_2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,Y_1),Z_2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Y_1)) ),
inference(pre_NNF_transformation,[status(thm)],[f459]) ).
fof(f2836,plain,
! [X_1,Y_1] :
( ! [Z_2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Z_2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,Y_1),Z_2)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X_1),Y_1)) ),
inference(miniscoping,[status(thm)],[f2835]) ).
fof(f2837,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f2836]) ).
fof(f3169,plain,
! [A_2,C_11,D_4] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),C_11)),hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),D_4)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_11),D_4)) ),
inference(pre_NNF_transformation,[status(thm)],[f571]) ).
fof(f3170,plain,
! [C_11,D_4] :
( ! [A_2] : hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),C_11)),hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),D_4)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_11),D_4)) ),
inference(miniscoping,[status(thm)],[f3169]) ).
fof(f3171,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X2),X0)),hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X2),X1)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f3170]) ).
fof(f3179,plain,
! [X0,X1,X2] : image_pname_a(X0,hAPP_f759274231e_bool(hAPP_p905327722e_bool(insert_pname,X1),X2)) = hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(X0,X1)),image_pname_a(X0,X2)),
inference(cnf_transformation,[status(thm)],[f575]) ).
fof(f3183,plain,
! [F,X_1,A] :
( hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A)) = image_pname_a(F,A)
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A)) ),
inference(pre_NNF_transformation,[status(thm)],[f577]) ).
fof(f3184,plain,
! [X_1,A] :
( ! [F] : hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A)) = image_pname_a(F,A)
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A)) ),
inference(miniscoping,[status(thm)],[f3183]) ).
fof(f3185,plain,
! [X0,X1,X2] :
( hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(X2,X0)),image_pname_a(X2,X1)) = image_pname_a(X2,X1)
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f3184]) ).
fof(f5625,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(thm)],[f1410]) ).
fof(f5628,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(cnf_transformation,[status(thm)],[f1413]) ).
fof(f5630,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(thm)],[f1416]) ).
fof(f5962,plain,
! [X0] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),image_pname_a(mgt_call,u)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),X0)) ),
inference(resolution,[status(thm)],[f2837,f5630]) ).
fof(f6085,plain,
! [X0] : hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X0),g)),hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X0),image_pname_a(mgt_call,u)))),
inference(resolution,[status(thm)],[f3171,f5625]) ).
fof(f6090,plain,
! [X0,X1,X2] :
( image_pname_a(X2,hAPP_f759274231e_bool(hAPP_p905327722e_bool(insert_pname,X0),X1)) = image_pname_a(X2,X1)
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1)) ),
inference(forward_demodulation,[status(thm)],[f3179,f3185]) ).
fof(f6091,plain,
! [X0] : image_pname_a(X0,hAPP_f759274231e_bool(hAPP_p905327722e_bool(insert_pname,pn),u)) = image_pname_a(X0,u),
inference(resolution,[status(thm)],[f6090,f5628]) ).
fof(f6455,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u))),image_pname_a(mgt_call,u))),
inference(resolution,[status(thm)],[f6085,f5962]) ).
fof(f6464,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,hAPP_f759274231e_bool(hAPP_p905327722e_bool(insert_pname,pn),u))),image_pname_a(mgt_call,u))),
inference(forward_demodulation,[status(thm)],[f3179,f6455]) ).
fof(f6465,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),image_pname_a(mgt_call,u))),
inference(forward_demodulation,[status(thm)],[f6091,f6464]) ).
fof(f6466,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6465,f2695]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW473+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 21 09:53:28 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.26/0.51 % Drodi V4.1.1
% 0.26/0.60 % Refutation found
% 0.26/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.35/0.66 % Elapsed time: 0.262087 seconds
% 0.35/0.66 % CPU time: 0.880435 seconds
% 0.35/0.66 % Total memory used: 243.964 MB
% 0.35/0.66 % Net memory used: 242.337 MB
%------------------------------------------------------------------------------