%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW950+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 : Sun Sep 27 09:14:56 AM UTC 2026
% Result : Theorem 119.50s 15.63s
% Output : CNFRefutation 119.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of formulae : 48 ( 29 unt; 0 def)
% Number of atoms : 72 ( 12 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 24 ~; 15 |; 2 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 49 ( 5 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax45,axiom,
! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO,
file('theBenchmark.p',ax45) ).
fof(ax46,axiom,
! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9,
file('theBenchmark.p',ax46) ).
fof(ax47,axiom,
! [VAR_X_7,VAR_Y_8] : constr_xor(VAR_X_7,VAR_Y_8) = constr_xor(VAR_Y_8,VAR_X_7),
file('theBenchmark.p',ax47) ).
fof(ax48,axiom,
! [VAR_X_0X30,VAR_Y_0X30,VAR_Z_0X30] : constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30),
file('theBenchmark.p',ax48) ).
fof(ax51,axiom,
! [VAR_V_33] :
( pred_attacker(VAR_V_33)
=> pred_attacker(constr_h(VAR_V_33)) ),
file('theBenchmark.p',ax51) ).
fof(ax55,axiom,
! [VAR_V_38] :
( pred_attacker(tuple_T_out_4(VAR_V_38))
=> pred_attacker(VAR_V_38) ),
file('theBenchmark.p',ax55) ).
fof(ax57,axiom,
! [VAR_V_44] :
( pred_attacker(tuple_T_out_2(VAR_V_44))
=> pred_attacker(VAR_V_44) ),
file('theBenchmark.p',ax57) ).
fof(ax58,axiom,
! [VAR_V_48,VAR_V_49] :
( ( pred_attacker(VAR_V_49)
& pred_attacker(VAR_V_48) )
=> pred_attacker(tuple_T_in_3(VAR_V_48,VAR_V_49)) ),
file('theBenchmark.p',ax58) ).
fof(ax61,axiom,
! [VAR_V_63] :
( pred_attacker(VAR_V_63)
=> pred_attacker(tuple_T_in_1(VAR_V_63)) ),
file('theBenchmark.p',ax61) ).
fof(ax73,axiom,
! [VAR_R_10X308] :
( pred_attacker(tuple_T_in_1(VAR_R_10X308))
=> pred_attacker(tuple_T_out_2(constr_h(constr_xor(VAR_R_10X308,constr_xor(name_k0x30,name_ki))))) ),
file('theBenchmark.p',ax73) ).
fof(ax74,axiom,
! [VAR_A_143,VAR_R_144] :
( ( pred_attacker(tuple_T_in_1(VAR_R_144))
& pred_attacker(tuple_T_in_3(VAR_A_143,constr_h(constr_xor(VAR_A_143,constr_xor(name_k0x30,name_ki))))) )
=> pred_attacker(tuple_T_out_4(name_objective)) ),
file('theBenchmark.p',ax74) ).
fof(co0,conjecture,
pred_attacker(name_objective),
file('theBenchmark.p',co0) ).
fof(co0_neg,negated_conjecture,
~ pred_attacker(name_objective),
inference(assume_negation,[status(cth)],[co0]) ).
cnf(c_98,plain,
constr_xor(A,A) = constr_ZERO,
inference(clausify,[status(thm)],[ax45]) ).
cnf(c_99,plain,
constr_xor(A,constr_ZERO) = A,
inference(clausify,[status(thm)],[ax46]) ).
cnf(c_100,plain,
constr_xor(A,B) = constr_xor(B,A),
inference(clausify,[status(thm)],[ax47]) ).
cnf(c_101,plain,
constr_xor(constr_xor(A,B),C) = constr_xor(A,constr_xor(B,C)),
inference(clausify,[status(thm)],[ax48]) ).
cnf(c_104,plain,
( pred_attacker(constr_h(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax51]) ).
fof(ax53,axiom,
pred_attacker(constr_ZERO),
file('theBenchmark.p',ax53) ).
cnf(c_106,plain,
pred_attacker(constr_ZERO),
inference(clausify,[status(thm)],[ax53]) ).
cnf(c_108,plain,
( pred_attacker(A)
| ~ pred_attacker(tuple_T_out_4(A)) ),
inference(clausify,[status(thm)],[ax55]) ).
cnf(c_110,plain,
( pred_attacker(A)
| ~ pred_attacker(tuple_T_out_2(A)) ),
inference(clausify,[status(thm)],[ax57]) ).
cnf(c_111,plain,
( pred_attacker(tuple_T_in_3(A,B))
| ~ pred_attacker(B)
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax58]) ).
cnf(c_114,plain,
( pred_attacker(tuple_T_in_1(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax61]) ).
fof(ax70,axiom,
pred_attacker(name_c),
file('theBenchmark.p',ax70) ).
cnf(c_121,plain,
pred_attacker(name_c),
inference(clausify,[status(thm)],[ax70]) ).
cnf(c_123,plain,
( pred_attacker(tuple_T_out_2(constr_h(constr_xor(A,constr_xor(name_k0x30,name_ki)))))
| ~ pred_attacker(tuple_T_in_1(A)) ),
inference(clausify,[status(thm)],[ax73]) ).
cnf(c_124,plain,
( pred_attacker(tuple_T_out_4(name_objective))
| ~ pred_attacker(tuple_T_in_1(B))
| ~ pred_attacker(tuple_T_in_3(A,constr_h(constr_xor(A,constr_xor(name_k0x30,name_ki))))) ),
inference(clausify,[status(thm)],[ax74]) ).
cnf(c_125,negated_conjecture,
~ pred_attacker(name_objective),
inference(clausify,[status(thm)],[co0_neg]) ).
cnf(c_126,plain,
constr_xor(constr_ZERO,A) = A,
inference(paramod,[status(thm)],[c_100,c_99]) ).
cnf(c_13386,plain,
constr_xor(constr_ZERO,A) = constr_xor(B,constr_xor(B,A)),
inference(paramod,[status(thm)],[c_98,c_101]) ).
cnf(c_13387,plain,
A = constr_xor(B,constr_xor(B,A)),
inference(paramod,[status(thm)],[c_126,c_13386]) ).
cnf(c_128,plain,
constr_xor(A,constr_xor(A,B)) = B,
inference(copy,[status(thm)],[c_13387]) ).
cnf(c_151,plain,
pred_attacker(tuple_T_in_1(constr_ZERO)),
inference(resolve,[status(thm)],[c_114,c_106]) ).
cnf(c_269,plain,
pred_attacker(constr_h(name_c)),
inference(resolve,[status(thm)],[c_104,c_121]) ).
cnf(c_311,plain,
( pred_attacker(tuple_T_out_4(name_objective))
| ~ pred_attacker(tuple_T_in_1(C))
| ~ pred_attacker(tuple_T_in_3(constr_xor(A,B),constr_h(constr_xor(A,constr_xor(B,constr_xor(name_k0x30,name_ki)))))) ),
inference(paramod,[status(thm)],[c_101,c_124]) ).
cnf(c_316,negated_conjecture,
~ pred_attacker(tuple_T_out_4(name_objective)),
inference(resolve,[status(thm)],[c_108,c_125]) ).
cnf(c_317,plain,
( ~ pred_attacker(tuple_T_in_1(C))
| ~ pred_attacker(tuple_T_in_3(constr_xor(A,B),constr_h(constr_xor(A,constr_xor(B,constr_xor(name_k0x30,name_ki)))))) ),
inference(resolve,[status(thm)],[c_316,c_311]) ).
cnf(c_13388,plain,
pred_attacker(tuple_T_out_2(constr_h(constr_xor(constr_ZERO,constr_xor(name_k0x30,name_ki))))),
inference(resolve,[status(thm)],[c_123,c_151]) ).
cnf(c_777,plain,
pred_attacker(tuple_T_out_2(constr_h(constr_xor(name_k0x30,name_ki)))),
inference(paramod,[status(thm)],[c_126,c_13388]) ).
cnf(c_3708,plain,
pred_attacker(tuple_T_in_1(constr_h(name_c))),
inference(resolve,[status(thm)],[c_114,c_269]) ).
cnf(c_13389,plain,
( ~ pred_attacker(tuple_T_in_1(B))
| ~ pred_attacker(tuple_T_in_3(constr_ZERO,constr_h(constr_xor(A,constr_xor(A,constr_xor(name_k0x30,name_ki)))))) ),
inference(paramod,[status(thm)],[c_98,c_317]) ).
cnf(c_13362,plain,
( ~ pred_attacker(tuple_T_in_1(A))
| ~ pred_attacker(tuple_T_in_3(constr_ZERO,constr_h(constr_xor(name_k0x30,name_ki)))) ),
inference(paramod,[status(thm)],[c_128,c_13389]) ).
cnf(c_13375,plain,
~ pred_attacker(tuple_T_in_3(constr_ZERO,constr_h(constr_xor(name_k0x30,name_ki)))),
inference(resolve,[status(thm)],[c_13362,c_3708]) ).
cnf(c_13390,plain,
( pred_attacker(tuple_T_in_3(constr_ZERO,A))
| ~ pred_attacker(A) ),
inference(resolve,[status(thm)],[c_111,c_106]) ).
cnf(c_13379,plain,
~ pred_attacker(constr_h(constr_xor(name_k0x30,name_ki))),
inference(resolve,[status(thm)],[c_13390,c_13375]) ).
cnf(c_13391,plain,
~ pred_attacker(tuple_T_out_2(constr_h(constr_xor(name_k0x30,name_ki)))),
inference(resolve,[status(thm)],[c_110,c_13379]) ).
cnf(c_13385,plain,
$false,
inference(resolve,[status(thm)],[c_777,c_13391]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW950+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.44 % Computer : n004.cluster.edu
% 0.15/0.44 % Model : x86_64 x86_64
% 0.15/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.44 % Memory : 8046.5625MB
% 0.15/0.44 % OS : Linux 6.8.0-71-generic
% 0.15/0.44 % CPULimit : 300
% 0.15/0.44 % WCLimit : 300
% 0.15/0.44 % DateTime : Sat Sep 26 16:37:07 UTC 2026
% 0.15/0.44 % CPUTime :
% 0.15/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.44 % Process 2164826 was started by sandbox2 on n004,
% 0.15/0.44 % Sat Sep 26 16:37:07 2026
% 0.15/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.45
% 0.15/0.45 % From the command line: assign(max_seconds, 300).
% 119.50/15.63
% 119.50/15.63 % given #500 (T,wt=19): 3520 pred_attacker(tuple_T_out_4(tuple_T_out_2(name_c))). [hyper(107,a,267,a)].
% 119.50/15.63
% 119.50/15.63 % SZS status Theorem for theBenchmark
% 119.50/15.63
% 119.50/15.63 % Proof 1 at 4.06 (+ 3.06) seconds.
% 119.50/15.63 % Length of proof is 39.
% 119.50/15.63 % Level of proof is 7.
% 119.50/15.63 % Maximum clause weight is 59.000.
% 119.50/15.63 % Given clauses 539.
% 119.50/15.63
% 119.50/15.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------