%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW961+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 : n011.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 50.81s 12.74s
% Output : Proof 50.81s
% 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 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 33 ( 6 sgn 21 !; 0 ?)
% 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_232,VAR_V_233] :
( pred_attacker(tuple_assoc_pair(VAR_V_232,VAR_V_233))
=> pred_attacker(VAR_V_232) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax143) ).
fof(f143_nnf,plain,
! [VAR_V_232,VAR_V_233] :
( pred_attacker(VAR_V_232)
| ~ pred_attacker(tuple_assoc_pair(VAR_V_232,VAR_V_233)) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [VAR_V_232,VAR_V_233] :
( pred_attacker(VAR_V_232)
| ~ pred_attacker(tuple_assoc_pair(VAR_V_232,VAR_V_233)) ),
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(p183,plain,
pred_attacker(X0),
inference(resolution,[status(thm)],[p182,c92]) ).
fof(f176,conjecture,
pred_attacker(name_objective),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co0) ).
fof(f176_neg,negated_conjecture,
~ pred_attacker(name_objective),
inference(negated_conjecture,[status(cth)],[f176]) ).
fof(f176_nnf,plain,
~ pred_attacker(name_objective),
inference(nnf_transformation,[status(thm)],[f176_neg]) ).
fof(f176_sk,plain,
~ pred_attacker(name_objective),
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c176,plain,
~ pred_attacker(name_objective),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(p184,plain,
$false,
inference(resolution,[status(thm)],[p183,c176]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW961+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n011.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Thu Sep 24 23:17:04 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 50.81/12.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.81/12.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------