%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW962+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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:51 PM UTC 2026
% Result : Theorem 42.55s 6.65s
% Output : Proof 42.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 5
% Syntax : Number of formulae : 24 ( 19 unt; 0 def)
% Number of atoms : 29 ( 9 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 13 ( 8 ~; 4 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 36 ( 6 sgn 23 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f82,axiom,
! [VAR_X_17,VAR_Y_18,VAR_Z_0X30] : tuple_assoc_pair(VAR_X_17,tuple_assoc_pair(VAR_Y_18,VAR_Z_0X30)) = tuple_assoc_pair(tuple_assoc_pair(VAR_X_17,VAR_Y_18),VAR_Z_0X30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax82) ).
fof(f82_nnf,plain,
! [VAR_X_17,VAR_Y_18,VAR_Z_0X30] : tuple_assoc_pair(VAR_X_17,tuple_assoc_pair(VAR_Y_18,VAR_Z_0X30)) = tuple_assoc_pair(tuple_assoc_pair(VAR_X_17,VAR_Y_18),VAR_Z_0X30),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [VAR_X_17,VAR_Y_18,VAR_Z_0X30] : tuple_assoc_pair(VAR_X_17,tuple_assoc_pair(VAR_Y_18,VAR_Z_0X30)) = tuple_assoc_pair(tuple_assoc_pair(VAR_X_17,VAR_Y_18),VAR_Z_0X30),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
tuple_assoc_pair(X0,tuple_assoc_pair(X1,X2)) = tuple_assoc_pair(tuple_assoc_pair(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
fof(f83,axiom,
! [VAR_X0X30_15,VAR_X1_16] : constr_assoc_pair_2_get_1_bitstring(tuple_assoc_pair(VAR_X0X30_15,VAR_X1_16)) = VAR_X1_16,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax83) ).
fof(f83_nnf,plain,
! [VAR_X0X30_15,VAR_X1_16] : constr_assoc_pair_2_get_1_bitstring(tuple_assoc_pair(VAR_X0X30_15,VAR_X1_16)) = VAR_X1_16,
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [VAR_X0X30_15,VAR_X1_16] : constr_assoc_pair_2_get_1_bitstring(tuple_assoc_pair(VAR_X0X30_15,VAR_X1_16)) = VAR_X1_16,
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
constr_assoc_pair_2_get_1_bitstring(tuple_assoc_pair(X0,X1)) = X1,
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(p177,plain,
tuple_assoc_pair(X0,X1) = X1,
inference(superposition,[status(thm)],[c82,c83]) ).
fof(f143,axiom,
! [VAR_V_233,VAR_V_234] :
( pred_attacker(tuple_assoc_pair(VAR_V_233,VAR_V_234))
=> pred_attacker(VAR_V_233) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax143) ).
fof(f143_nnf,plain,
! [VAR_V_233,VAR_V_234] :
( pred_attacker(VAR_V_233)
| ~ pred_attacker(tuple_assoc_pair(VAR_V_233,VAR_V_234)) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [VAR_V_233,VAR_V_234] :
( pred_attacker(VAR_V_233)
| ~ pred_attacker(tuple_assoc_pair(VAR_V_233,VAR_V_234)) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c143,plain,
( pred_attacker(X0)
| ~ pred_attacker(tuple_assoc_pair(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
cnf(p182,plain,
( pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(demodulation,[status(thm)],[p177,c143]) ).
fof(f92,axiom,
pred_attacker(tuple_true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax92) ).
fof(f92_nnf,plain,
pred_attacker(tuple_true),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
pred_attacker(tuple_true),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(p562,plain,
pred_attacker(X0),
inference(resolution,[status(thm)],[p182,c92]) ).
fof(f176,conjecture,
! [VAR_V_711] : pred_attacker(tuple_2(name_Nb(VAR_V_711),name_objective)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co0) ).
fof(f176_neg,negated_conjecture,
~ ! [VAR_V_711] : pred_attacker(tuple_2(name_Nb(VAR_V_711),name_objective)),
inference(negated_conjecture,[status(cth)],[f176]) ).
fof(f176_nnf,plain,
? [VAR_V_711] : ~ pred_attacker(tuple_2(name_Nb(VAR_V_711),name_objective)),
inference(nnf_transformation,[status(thm)],[f176_neg]) ).
fof(f176_sk,plain,
~ pred_attacker(tuple_2(name_Nb(sk0),name_objective)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f176_nnf]) ).
cnf(c176,plain,
~ pred_attacker(tuple_2(name_Nb(sk0),name_objective)),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(p565,plain,
$false,
inference(resolution,[status(thm)],[p562,c176]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW962+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 23:18:49 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 42.55/6.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.55/6.65 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------