%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 : Tue Sep 29 01:30:03 PM UTC 2026
% Result : Theorem 2.41s 1.75s
% Output : Refutation 5.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 15
% Syntax : Number of formulae : 113 ( 10 unt; 12 def)
% Number of atoms : 336 ( 2 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 389 ( 166 ~; 178 |; 16 &)
% ( 16 <=>; 12 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 11 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 123 ( 0 sgn 111 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0)
<=> c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln_Oequations_I9_J) ).
fof(f723,axiom,
! [X0] : hAPP(c_Nat_OSuc,X0) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),X0),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Suc__eq__plus1) ).
fof(f5205,conjecture,
( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_Q(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f5206,negated_conjecture,
~ ( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_Q(X0,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f5205]) ).
fof(f5207,plain,
~ ( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X3,X4] :
( v_P(X3,X4)
=> ! [X5] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)
=> v_Q(X3,X5) ) ) ),
inference(rectify,[],[f5206]) ).
fof(f5208,plain,
( ! [X0,X1] :
( ! [X2] :
( v_Q(X0,X2)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2) )
| ~ v_P(X0,X1) )
<~> ! [X3,X4] :
( ! [X5] :
( v_Q(X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5) )
| ~ v_P(X3,X4) ) ),
inference(ennf_transformation,[],[f5207]) ).
fof(f5272,plain,
( ( ? [X3,X4] :
( ? [X5] :
( ~ v_Q(X3,X5)
& c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5) )
& v_P(X3,X4) )
| ? [X0,X1] :
( ? [X2] :
( ~ v_Q(X0,X2)
& c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2) )
& v_P(X0,X1) ) )
& ( ! [X3,X4] :
( ! [X5] :
( v_Q(X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5) )
| ~ v_P(X3,X4) )
| ! [X0,X1] :
( ! [X2] :
( v_Q(X0,X2)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2) )
| ~ v_P(X0,X1) ) ) ),
inference(nnf_transformation,[],[f5208]) ).
fof(f5273,plain,
( ( ? [X0,X1] :
( ? [X2] :
( ~ v_Q(X0,X2)
& c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2) )
& v_P(X0,X1) )
| ? [X3,X4] :
( ? [X5] :
( ~ v_Q(X3,X5)
& c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X4,v_n,X5) )
& v_P(X3,X4) ) )
& ( ! [X6,X7] :
( ! [X8] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8) )
| ~ v_P(X6,X7) )
| ! [X9,X10] :
( ! [X11] :
( v_Q(X9,X11)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X10,v_n,X11) )
| ~ v_P(X9,X10) ) ) ),
inference(rectify,[],[f5272]) ).
fof(f5274,plain,
( ( ( ~ v_Q(sK0,sK2)
& c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(c_Nat_OSuc,v_n),sK2)
& v_P(sK0,sK1) )
| ( ~ v_Q(sK3,sK5)
& c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5)
& v_P(sK3,sK4) ) )
& ( ! [X6,X7] :
( ! [X8] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8) )
| ~ v_P(X6,X7) )
| ! [X9,X10] :
( ! [X11] :
( v_Q(X9,X11)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X10,v_n,X11) )
| ~ v_P(X9,X10) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5)],[f5273]) ).
fof(f5294,plain,
! [X0,X1,X2,X3] :
( ( c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0) )
& ( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f5338,plain,
! [X10,X11,X8,X6,X9,X7] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8)
| ~ v_P(X6,X7)
| v_Q(X9,X11)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X10,v_n,X11)
| ~ v_P(X9,X10) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5339,plain,
( v_P(sK0,sK1)
| v_P(sK3,sK4) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5340,plain,
( v_P(sK0,sK1)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5341,plain,
( v_P(sK0,sK1)
| ~ v_Q(sK3,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5342,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(c_Nat_OSuc,v_n),sK2)
| v_P(sK3,sK4) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5343,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(c_Nat_OSuc,v_n),sK2)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5344,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(c_Nat_OSuc,v_n),sK2)
| ~ v_Q(sK3,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5345,plain,
( ~ v_Q(sK0,sK2)
| v_P(sK3,sK4) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5346,plain,
( ~ v_Q(sK0,sK2)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5347,plain,
( ~ v_Q(sK0,sK2)
| ~ v_Q(sK3,sK5) ),
inference(cnf_transformation,[],[f5274]) ).
fof(f5410,plain,
! [X2,X3,X0,X1] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0) ),
inference(cnf_transformation,[],[f5294]) ).
fof(f5411,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0) ),
inference(cnf_transformation,[],[f5294]) ).
fof(f5441,plain,
! [X0] : hAPP(c_Nat_OSuc,X0) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),X0),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(cnf_transformation,[],[f723]) ).
fof(f5603,plain,
! [X10,X11,X9] :
( ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X10,v_n,X11)
| ~ v_P(X9,X10)
| sP48(X9,X11) ),
inference(cnf_transformation,[],[f5603_D]) ).
fof(f5603_D,definition,
! [X11,X9] :
( ! [X10] :
( ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X10,v_n,X11)
| ~ v_P(X9,X10) )
<=> ~ sP48(X9,X11) ),
introduced(definition,[new_symbols(definition,[sP48])],[general_splitting_component_introduction]) ).
fof(f5604,plain,
! [X11,X8,X6,X9,X7] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8)
| ~ v_P(X6,X7)
| v_Q(X9,X11)
| ~ sP48(X9,X11) ),
inference(general_splitting,[],[f5338,f5603_D]) ).
fof(f5605,plain,
! [X11,X9] :
( ~ sP48(X9,X11)
| v_Q(X9,X11)
| sP49(X9) ),
inference(cnf_transformation,[],[f5605_D]) ).
fof(f5605_D,definition,
! [X9] :
( ! [X11] :
( ~ sP48(X9,X11)
| v_Q(X9,X11) )
<=> ~ sP49(X9) ),
introduced(definition,[new_symbols(definition,[sP49])],[general_splitting_component_introduction]) ).
fof(f5606,plain,
! [X8,X6,X9,X7] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8)
| ~ v_P(X6,X7)
| ~ sP49(X9) ),
inference(general_splitting,[],[f5604,f5605_D]) ).
fof(f5607,plain,
! [X9] :
( ~ sP49(X9)
| sP50 ),
inference(cnf_transformation,[],[f5607_D]) ).
fof(f5607_D,definition,
( ! [X9] : ~ sP49(X9)
<=> ~ sP50 ),
introduced(definition,[new_symbols(definition,[sP50])],[general_splitting_component_introduction]) ).
fof(f5608,plain,
! [X8,X6,X7] :
( v_Q(X6,X8)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(c_Nat_OSuc,v_n),X8)
| ~ v_P(X6,X7)
| ~ sP50 ),
inference(general_splitting,[],[f5606,f5607_D]) ).
fof(f5610,definition,
( spl51_1
<=> v_P(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl51_1])],[avatar_definition]) ).
fof(f5612,plain,
( v_P(sK3,sK4)
| ~ spl51_1 ),
inference(avatar_component_clause,[],[f5610]) ).
fof(f5614,definition,
( spl51_2
<=> v_P(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl51_2])],[avatar_definition]) ).
fof(f5616,plain,
( v_P(sK0,sK1)
| ~ spl51_2 ),
inference(avatar_component_clause,[],[f5614]) ).
fof(f5617,plain,
( spl51_1
| spl51_2 ),
inference(avatar_split_clause,[],[f5339,f5614,f5610]) ).
fof(f5619,definition,
( spl51_3
<=> c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5) ),
introduced(definition,[new_symbols(definition,[spl51_3])],[avatar_definition]) ).
fof(f5621,plain,
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5)
| ~ spl51_3 ),
inference(avatar_component_clause,[],[f5619]) ).
fof(f5622,plain,
( spl51_3
| spl51_2 ),
inference(avatar_split_clause,[],[f5340,f5614,f5619]) ).
fof(f5624,definition,
( spl51_4
<=> v_Q(sK3,sK5) ),
introduced(definition,[new_symbols(definition,[spl51_4])],[avatar_definition]) ).
fof(f5626,plain,
( ~ v_Q(sK3,sK5)
| spl51_4 ),
inference(avatar_component_clause,[],[f5624]) ).
fof(f5627,plain,
( ~ spl51_4
| spl51_2 ),
inference(avatar_split_clause,[],[f5341,f5614,f5624]) ).
fof(f5628,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK2)
| v_P(sK3,sK4) ),
inference(forward_demodulation,[],[f5342,f5441]) ).
fof(f5629,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK2)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK4,v_n,sK5) ),
inference(forward_demodulation,[],[f5343,f5441]) ).
fof(f5630,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK2)
| ~ v_Q(sK3,sK5) ),
inference(forward_demodulation,[],[f5344,f5441]) ).
fof(f5632,definition,
( spl51_5
<=> v_Q(sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl51_5])],[avatar_definition]) ).
fof(f5634,plain,
( ~ v_Q(sK0,sK2)
| spl51_5 ),
inference(avatar_component_clause,[],[f5632]) ).
fof(f5635,plain,
( spl51_1
| ~ spl51_5 ),
inference(avatar_split_clause,[],[f5345,f5632,f5610]) ).
fof(f5636,plain,
( spl51_3
| ~ spl51_5 ),
inference(avatar_split_clause,[],[f5346,f5632,f5619]) ).
fof(f5637,plain,
( ~ spl51_4
| ~ spl51_5 ),
inference(avatar_split_clause,[],[f5347,f5632,f5624]) ).
fof(f5639,definition,
( spl51_6
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl51_6])],[avatar_definition]) ).
fof(f5643,definition,
( spl51_7
<=> ! [X9] : ~ sP49(X9) ),
introduced(definition,[new_symbols(definition,[spl51_7])],[avatar_definition]) ).
fof(f5644,plain,
( ! [X9] : ~ sP49(X9)
| ~ spl51_7 ),
inference(avatar_component_clause,[],[f5643]) ).
fof(f5645,plain,
( spl51_6
| spl51_7 ),
inference(avatar_split_clause,[],[f5607,f5643,f5639]) ).
fof(f5646,plain,
! [X8,X6,X7] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),X8)
| v_Q(X6,X8)
| ~ v_P(X6,X7)
| ~ sP50 ),
inference(forward_demodulation,[],[f5608,f5441]) ).
fof(f5648,definition,
( spl51_8
<=> c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK2) ),
introduced(definition,[new_symbols(definition,[spl51_8])],[avatar_definition]) ).
fof(f5650,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK2)
| ~ spl51_8 ),
inference(avatar_component_clause,[],[f5648]) ).
fof(f5651,plain,
( spl51_1
| spl51_8 ),
inference(avatar_split_clause,[],[f5628,f5648,f5610]) ).
fof(f5652,plain,
( spl51_3
| spl51_8 ),
inference(avatar_split_clause,[],[f5629,f5648,f5619]) ).
fof(f5653,plain,
( ~ spl51_4
| spl51_8 ),
inference(avatar_split_clause,[],[f5630,f5648,f5624]) ).
fof(f5655,definition,
( spl51_9
<=> ! [X6,X8,X7] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),X8)
| ~ v_P(X6,X7)
| v_Q(X6,X8) ) ),
introduced(definition,[new_symbols(definition,[spl51_9])],[avatar_definition]) ).
fof(f5656,plain,
( ! [X8,X6,X7] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X7,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),X8)
| ~ v_P(X6,X7)
| v_Q(X6,X8) )
| ~ spl51_9 ),
inference(avatar_component_clause,[],[f5655]) ).
fof(f5657,plain,
( ~ spl51_6
| spl51_9 ),
inference(avatar_split_clause,[],[f5646,f5655,f5639]) ).
fof(f5668,plain,
! [X2,X0,X1] :
( ~ v_P(X0,X1)
| sP48(X0,X2)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2) ),
inference(resolution,[],[f5603,f5410]) ).
fof(f5678,plain,
! [X2,X0,X1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),X2)
| ~ v_P(X0,X1)
| sP48(X0,X2) ),
inference(forward_demodulation,[],[f5668,f5441]) ).
fof(f5679,plain,
( ! [X0] :
( ~ v_P(X0,sK1)
| sP48(X0,sK2) )
| ~ spl51_8 ),
inference(resolution,[],[f5678,f5650]) ).
fof(f5692,plain,
( sP48(sK0,sK2)
| ~ spl51_2
| ~ spl51_8 ),
inference(resolution,[],[f5679,f5616]) ).
fof(f5695,plain,
( v_Q(sK0,sK2)
| sP49(sK0)
| ~ spl51_2
| ~ spl51_8 ),
inference(resolution,[],[f5692,f5605]) ).
fof(f5696,plain,
( sP49(sK0)
| ~ spl51_2
| spl51_5
| ~ spl51_8 ),
inference(forward_subsumption_resolution,[],[f5695,f5634]) ).
fof(f5697,plain,
( $false
| ~ spl51_2
| spl51_5
| ~ spl51_7
| ~ spl51_8 ),
inference(forward_subsumption_resolution,[],[f5696,f5644]) ).
fof(f5698,plain,
( ~ spl51_2
| spl51_5
| ~ spl51_7
| ~ spl51_8 ),
inference(avatar_contradiction_clause,[],[f5697]) ).
fof(f5699,plain,
( ! [X0] :
( ~ v_P(X0,sK1)
| v_Q(X0,sK2) )
| ~ spl51_8
| ~ spl51_9 ),
inference(resolution,[],[f5656,f5650]) ).
fof(f5710,plain,
( v_Q(sK0,sK2)
| ~ spl51_2
| ~ spl51_8
| ~ spl51_9 ),
inference(resolution,[],[f5699,f5616]) ).
fof(f5711,plain,
( $false
| ~ spl51_2
| spl51_5
| ~ spl51_8
| ~ spl51_9 ),
inference(forward_subsumption_resolution,[],[f5710,f5634]) ).
fof(f5712,plain,
( ~ spl51_2
| spl51_5
| ~ spl51_8
| ~ spl51_9 ),
inference(avatar_contradiction_clause,[],[f5711]) ).
fof(f5714,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK4,hAPP(c_Nat_OSuc,v_n),sK5)
| ~ spl51_3 ),
inference(resolution,[],[f5621,f5411]) ).
fof(f5715,plain,
( ! [X0] :
( ~ v_P(X0,sK4)
| sP48(X0,sK5) )
| ~ spl51_3 ),
inference(resolution,[],[f5621,f5603]) ).
fof(f5716,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK4,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),v_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),sK5)
| ~ spl51_3 ),
inference(forward_demodulation,[],[f5714,f5441]) ).
fof(f5718,plain,
( sP48(sK3,sK5)
| ~ spl51_1
| ~ spl51_3 ),
inference(resolution,[],[f5715,f5612]) ).
fof(f5720,plain,
( v_Q(sK3,sK5)
| sP49(sK3)
| ~ spl51_1
| ~ spl51_3 ),
inference(resolution,[],[f5718,f5605]) ).
fof(f5721,plain,
( sP49(sK3)
| ~ spl51_1
| ~ spl51_3
| spl51_4 ),
inference(forward_subsumption_resolution,[],[f5720,f5626]) ).
fof(f5722,plain,
( $false
| ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_7 ),
inference(forward_subsumption_resolution,[],[f5721,f5644]) ).
fof(f5723,plain,
( ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_7 ),
inference(avatar_contradiction_clause,[],[f5722]) ).
fof(f5734,plain,
( ! [X0] :
( ~ v_P(X0,sK4)
| v_Q(X0,sK5) )
| ~ spl51_3
| ~ spl51_9 ),
inference(resolution,[],[f5716,f5656]) ).
fof(f5737,plain,
( v_Q(sK3,sK5)
| ~ spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(resolution,[],[f5734,f5612]) ).
fof(f5738,plain,
( $false
| ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_9 ),
inference(forward_subsumption_resolution,[],[f5737,f5626]) ).
fof(f5739,plain,
( ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_9 ),
inference(avatar_contradiction_clause,[],[f5738]) ).
cnf(s1,plain,
( spl51_1
| spl51_2 ),
inference(sat_conversion,[],[f5617]) ).
cnf(s2,plain,
( spl51_2
| spl51_3 ),
inference(sat_conversion,[],[f5622]) ).
cnf(s3,plain,
( spl51_2
| ~ spl51_4 ),
inference(sat_conversion,[],[f5627]) ).
cnf(s4,plain,
( spl51_1
| ~ spl51_5 ),
inference(sat_conversion,[],[f5635]) ).
cnf(s5,plain,
( spl51_3
| ~ spl51_5 ),
inference(sat_conversion,[],[f5636]) ).
cnf(s6,plain,
( ~ spl51_4
| ~ spl51_5 ),
inference(sat_conversion,[],[f5637]) ).
cnf(s7,plain,
( spl51_6
| spl51_7 ),
inference(sat_conversion,[],[f5645]) ).
cnf(s8,plain,
( spl51_1
| spl51_8 ),
inference(sat_conversion,[],[f5651]) ).
cnf(s9,plain,
( spl51_3
| spl51_8 ),
inference(sat_conversion,[],[f5652]) ).
cnf(s10,plain,
( ~ spl51_4
| spl51_8 ),
inference(sat_conversion,[],[f5653]) ).
cnf(s11,plain,
( ~ spl51_6
| spl51_9 ),
inference(sat_conversion,[],[f5657]) ).
cnf(s13,plain,
( ~ spl51_2
| spl51_5
| ~ spl51_7
| ~ spl51_8 ),
inference(sat_conversion,[],[f5698]) ).
cnf(s14,plain,
( ~ spl51_2
| spl51_5
| ~ spl51_8
| ~ spl51_9 ),
inference(sat_conversion,[],[f5712]) ).
cnf(s15,plain,
( ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_7 ),
inference(sat_conversion,[],[f5723]) ).
cnf(s16,plain,
( ~ spl51_1
| ~ spl51_3
| spl51_4
| ~ spl51_9 ),
inference(sat_conversion,[],[f5739]) ).
cnf(s17,plain,
( ~ spl51_2
| spl51_5
| ~ spl51_8 ),
inference(rat,[],[s7,s11,s13,s14]) ).
cnf(s18,plain,
spl51_1,
inference(rat,[],[s17,s1,s4,s8]) ).
cnf(s19,plain,
( ~ spl51_3
| spl51_4 ),
inference(rat,[],[s7,s11,s15,s16,s18]) ).
cnf(s20,plain,
spl51_8,
inference(rat,[],[s19,s9,s10]) ).
cnf(s21,plain,
~ spl51_5,
inference(rat,[],[s19,s5,s6]) ).
cnf(s22,plain,
~ spl51_2,
inference(rat,[],[s17,s20,s21]) ).
cnf(s23,plain,
~ spl51_4,
inference(rat,[],[s3,s22]) ).
cnf(s24,plain,
spl51_3,
inference(rat,[],[s2,s22]) ).
cnf(s25,plain,
$false,
inference(rat,[],[s19,s23,s24]) ).
fof(f5740,plain,
$false,
inference(avatar_sat_refutation,[],[s25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 % Computer : n002.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 13:33:37 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running first-order theorem proving
% 0.24/0.30 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.41/1.75 % (352598)Detected formulas, will run a generic FOF schedule.
% 2.41/1.75 % (352608)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2290937823:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 2.41/1.75 % (352608)First to succeed.
% 2.41/1.75 % (352608)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-352598"
% 2.41/1.75 % (352607)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3387868208:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 2.41/1.75 % (352610)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3288245646:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 2.41/1.75 % (352609)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3373638013:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 2.41/1.75 % (352605)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2969892963:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 2.41/1.75 % (352606)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3651726331:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 2.41/1.75 % (352611)dis-21_1_sil=8000:lcm=predicate:random_seed=847044484:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 2.41/1.75 % (352610)Instruction limit reached!
% 2.41/1.75 % (352610)------------------------------
% 2.41/1.75 % (352610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/1.75 % (352610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/1.75 % (352610)CaDiCaL version: 2.1.3
% 2.41/1.75 % (352610)Termination reason: Instruction limit
% 2.41/1.75 % (352610)Termination phase: SInE selection
% 2.41/1.75 % (352610)Time elapsed: 0.114 s
% 2.41/1.75 % (352610)Peak memory usage: 90 MB
% 2.41/1.75 % (352610)Instructions burned: 140 (million)
% 2.41/1.75 % (352609)Instruction limit reached!
% 2.41/1.75 % (352609)------------------------------
% 2.41/1.75 % (352609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/1.75 % (352609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/1.75 % (352609)CaDiCaL version: 2.1.3
% 2.41/1.75 % (352609)Termination reason: Instruction limit
% 2.41/1.75 % (352609)Termination phase: Property scanning
% 2.41/1.75 % (352609)Time elapsed: 0.118 s
% 2.41/1.75 % (352609)Peak memory usage: 93 MB
% 2.41/1.75 % (352609)Instructions burned: 120 (million)
% 2.41/1.75 % (352611)Instruction limit reached!
% 2.41/1.75 % (352611)------------------------------
% 2.41/1.75 % (352611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/1.75 % (352611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/1.75 % (352611)CaDiCaL version: 2.1.3
% 2.41/1.75 % (352611)Termination reason: Instruction limit
% 2.41/1.75 % (352611)Termination phase: Preprocessing 3
% 2.41/1.75 % (352611)Time elapsed: 0.137 s
% 2.41/1.75 % (352611)Peak memory usage: 93 MB
% 2.41/1.75 % (352611)Instructions burned: 130 (million)
% 2.41/1.75 % (352608)Refutation found. Thanks to Tanya!
% 2.41/1.75 % SZS status Theorem for theBenchmark
% 2.41/1.75 % SZS output start Proof for theBenchmark
% See solution above
% 5.06/2.07 % (352608)------------------------------
% 5.06/2.07 % (352608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/2.07 % (352608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/2.07 % (352608)CaDiCaL version: 2.1.3
% 5.06/2.07 % (352608)Termination reason: Refutation
% 5.06/2.07 % (352608)Time elapsed: 0.040 s
% 5.06/2.07 % (352608)Peak memory usage: 95 MB
% 5.06/2.07 % (352608)Instructions burned: 63 (million)
% 5.06/2.07 % (352608)------------------------------
% 5.06/2.07 % (352608)------------------------------
% 5.06/2.07 % (352598)Success in time 1.009 s
% 5.06/2.07 % Vampire exiting
%------------------------------------------------------------------------------