%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW478+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:18 PM UTC 2026
% Result : Theorem 101.05s 15.05s
% Output : Proof 101.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 22 unt; 0 def)
% Number of atoms : 38 ( 12 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 12 ~; 9 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 16 con; 0-3 aty)
% Number of variables : 14 ( 2 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1344,axiom,
! [P] :
( is_bool(P)
=> ( P = fFalse
| P = fTrue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_T) ).
fof(f1344_nnf,plain,
! [P] :
( P = fFalse
| P = fTrue
| ~ is_bool(P) ),
inference(nnf_transformation,[status(thm)],[f1344]) ).
fof(f1344_sk,plain,
! [P] :
( P = fFalse
| P = fTrue
| ~ is_bool(P) ),
inference(skolemisation,[status(esa)],[f1344_nnf]) ).
cnf(c2195,plain,
( X0 = fFalse
| X0 = fTrue
| ~ is_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f1344_sk]) ).
fof(f81,hypothesis,
! [B_1_1,B_2_1] : is_bool(hAPP_f1453283057l_bool(B_1_1,B_2_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__fun_Itc__prod_Itc__pro_ha6610e7409cd6f70) ).
fof(f81_nnf,plain,
! [B_1_1,B_2_1] : is_bool(hAPP_f1453283057l_bool(B_1_1,B_2_1)),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [B_1_1,B_2_1] : is_bool(hAPP_f1453283057l_bool(B_1_1,B_2_1)),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c81,plain,
is_bool(hAPP_f1453283057l_bool(X0,X1)),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(p634,plain,
( hAPP_f1453283057l_bool(X0,X1) = fFalse
| hAPP_f1453283057l_bool(X0,X1) = fTrue ),
inference(resolution,[status(thm)],[c2195,c81]) ).
fof(f1490,conjecture,
hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1490_neg,negated_conjecture,
~ hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(negated_conjecture,[status(cth)],[f1490]) ).
fof(f1490_nnf,plain,
~ hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(nnf_transformation,[status(thm)],[f1490_neg]) ).
fof(f1490_sk,plain,
~ hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(skolemisation,[status(esa)],[f1490_nnf]) ).
cnf(c2341,plain,
~ hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(cnf_transformation,[status(esa)],[f1490_sk]) ).
cnf(p2052,plain,
( ~ hBOOL(fTrue)
| hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p)) = fFalse ),
inference(superposition,[status(thm)],[p634,c2341]) ).
fof(f1343,axiom,
hBOOL(fTrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
fof(f1343_nnf,plain,
hBOOL(fTrue),
inference(nnf_transformation,[status(thm)],[f1343]) ).
cnf(c2194,plain,
hBOOL(fTrue),
inference(cnf_transformation,[status(esa)],[f1343_nnf]) ).
cnf(p2068,plain,
hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p)) = fFalse,
inference(resolution,[status(thm)],[p2052,c2194]) ).
fof(f142,axiom,
hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_InitBlockRed_I1_J) ).
fof(f142_nnf,plain,
hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(nnf_transformation,[status(thm)],[f142]) ).
cnf(c142,plain,
hBOOL(hAPP_f1453283057l_bool(hAPP_P1303341961l_bool(member773094996on_val,hAPP_P1886180715on_val(hAPP_P1870962205on_val(produc1441475159on_val,hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,ea),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,ha),fun_up1149430426on_val(la,v_1,hAPP_val_option_val(some_val,v))))),hAPP_P604205461on_val(hAPP_e1659493427on_val(produc1259058957on_val,e_a),hAPP_f1727192346on_val(hAPP_f1849790461on_val(produc899768717on_val,h_a),l_a)))),red(p))),
inference(cnf_transformation,[status(esa)],[f142_nnf]) ).
cnf(p2069,plain,
hBOOL(fFalse),
inference(demodulation,[status(thm)],[p2068,c142]) ).
fof(f1351,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1351_nnf,plain,
~ hBOOL(fFalse),
inference(nnf_transformation,[status(thm)],[f1351]) ).
fof(f1351_sk,plain,
~ hBOOL(fFalse),
inference(skolemisation,[status(esa)],[f1351_nnf]) ).
cnf(c2202,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(esa)],[f1351_sk]) ).
cnf(p2070,plain,
$false,
inference(resolution,[status(thm)],[p2069,c2202]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW478+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 22:41:35 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 101.05/15.05 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.05/15.05 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------