%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW473+1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 03:27:12 PM UTC 2026
% Result : Theorem 36.29s 5.28s
% Output : Proof 36.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of formulae : 37 ( 28 unt; 0 def)
% Number of atoms : 50 ( 15 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 27 ( 14 ~; 10 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f304,axiom,
! [A_1,A] :
( is_fun_pname_bool(A)
=> ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_1),A))
=> insert_pname(A_1,A) = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_insert__absorb) ).
fof(f304_nnf,plain,
! [A_1,A] :
( insert_pname(A_1,A) = A
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_1),A))
| ~ is_fun_pname_bool(A) ),
inference(nnf_transformation,[status(thm)],[f304]) ).
fof(f304_sk,plain,
! [A,A_1] :
( insert_pname(A_1,A) = A
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_1),A))
| ~ is_fun_pname_bool(A) ),
inference(skolemisation,[status(esa)],[f304_nnf]) ).
cnf(c364,plain,
( insert_pname(X0,X1) = X1
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1))
| ~ is_fun_pname_bool(X1) ),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
fof(f79,hypothesis,
is_fun_pname_bool(u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_U) ).
fof(f79_nnf,plain,
is_fun_pname_bool(u),
inference(nnf_transformation,[status(thm)],[f79]) ).
cnf(c79,plain,
is_fun_pname_bool(u),
inference(cnf_transformation,[status(esa)],[f79_nnf]) ).
cnf(p748,plain,
( insert_pname(X0,u) = u
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),u)) ),
inference(resolution,[status(thm)],[c364,c79]) ).
fof(f446,hypothesis,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_4) ).
fof(f446_nnf,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(nnf_transformation,[status(thm)],[f446]) ).
cnf(c545,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(cnf_transformation,[status(esa)],[f446_nnf]) ).
cnf(p751,plain,
insert_pname(pn,u) = u,
inference(resolution,[status(thm)],[p748,c545]) ).
fof(f365,axiom,
! [F,A_1,B] : image_pname_a(F,insert_pname(A_1,B)) = insert_a(hAPP_pname_a(F,A_1),image_pname_a(F,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_image__insert) ).
fof(f365_nnf,plain,
! [F,A_1,B] : image_pname_a(F,insert_pname(A_1,B)) = insert_a(hAPP_pname_a(F,A_1),image_pname_a(F,B)),
inference(nnf_transformation,[status(thm)],[f365]) ).
fof(f365_sk,plain,
! [F,A_1,B] : image_pname_a(F,insert_pname(A_1,B)) = insert_a(hAPP_pname_a(F,A_1),image_pname_a(F,B)),
inference(skolemisation,[status(esa)],[f365_nnf]) ).
cnf(c449,plain,
image_pname_a(X0,insert_pname(X1,X2)) = insert_a(hAPP_pname_a(X0,X1),image_pname_a(X0,X2)),
inference(cnf_transformation,[status(esa)],[f365_sk]) ).
fof(f287,axiom,
! [X_2,A] : insert_a(X_2,insert_a(X_2,A)) = insert_a(X_2,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_insert__absorb2) ).
fof(f287_nnf,plain,
! [X_2,A] : insert_a(X_2,insert_a(X_2,A)) = insert_a(X_2,A),
inference(nnf_transformation,[status(thm)],[f287]) ).
fof(f287_sk,plain,
! [X_2,A] : insert_a(X_2,insert_a(X_2,A)) = insert_a(X_2,A),
inference(skolemisation,[status(esa)],[f287_nnf]) ).
cnf(c332,plain,
insert_a(X0,insert_a(X0,X1)) = insert_a(X0,X1),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(p715,plain,
insert_a(hAPP_pname_a(X0,X1),image_pname_a(X0,X2)) = image_pname_a(X0,insert_pname(X1,X2)),
inference(superposition,[status(thm)],[c449,c332]) ).
fof(f364,axiom,
! [A_1,C,D] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C),D))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_1,C)),insert_a(A_1,D))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_283_insert__mono) ).
fof(f364_nnf,plain,
! [A_1,C,D] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_1,C)),insert_a(A_1,D)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C),D)) ),
inference(nnf_transformation,[status(thm)],[f364]) ).
fof(f364_sk,plain,
! [C,D,A_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_1,C)),insert_a(A_1,D)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C),D)) ),
inference(skolemisation,[status(esa)],[f364_nnf]) ).
cnf(c448,plain,
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X0,X1)),insert_a(X0,X2)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f364_sk]) ).
fof(f443,hypothesis,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f443_nnf,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
inference(nnf_transformation,[status(thm)],[f443]) ).
cnf(c542,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(esa)],[f443_nnf]) ).
cnf(p1367,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X0,g)),insert_a(X0,image_pname_a(mgt_call,u)))),
inference(resolution,[status(thm)],[c448,c542]) ).
cnf(p1385,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,X0),g)),image_pname_a(mgt_call,insert_pname(X0,u)))),
inference(superposition,[status(thm)],[p715,p1367]) ).
cnf(p1402,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(superposition,[status(thm)],[p751,p1385]) ).
fof(f448,conjecture,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_6) ).
fof(f448_neg,negated_conjecture,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(negated_conjecture,[status(cth)],[f448]) ).
fof(f448_nnf,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(nnf_transformation,[status(thm)],[f448_neg]) ).
fof(f448_sk,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(skolemisation,[status(esa)],[f448_nnf]) ).
cnf(c547,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(esa)],[f448_sk]) ).
cnf(p1414,plain,
$false,
inference(resolution,[status(thm)],[p1402,c547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW473+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.62 % Computer : n015.cluster.edu
% 0.16/0.62 % Model : x86_64 x86_64
% 0.16/0.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.62 % Memory : 8046.5625MB
% 0.16/0.62 % OS : Linux 6.8.0-71-generic
% 0.16/0.62 % CPULimit : 300
% 0.16/0.62 % WCLimit : 300
% 0.16/0.62 % DateTime : Thu Sep 24 22:35:58 UTC 2026
% 0.16/0.62 % CPUTime :
% 0.16/0.62 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 36.29/5.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.29/5.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------