%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP125-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 10:12:44 AM UTC 2026
% Result : Unsatisfiable 3.42s 1.50s
% Output : Refutation 3.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 95
% Syntax : Number of formulae : 523 ( 90 unt; 61 def)
% Number of atoms : 1273 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1378 ( 628 ~; 689 |; 0 &)
% ( 61 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 67 ( 66 usr; 62 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 71 ( 0 sgn 71 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
fof(f3,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_then_e_4) ).
fof(f12,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
fof(f13,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_3) ).
fof(f14,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_4) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ~ product(X0,e_1,X1)
| ~ next(X0,X2)
| ~ greater(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
fof(f16,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f17,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f18,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f19,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f20,axiom,
group_element(e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_5) ).
fof(f21,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f22,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f23,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f24,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
fof(f25,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
fof(f26,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f27,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f28,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
fof(f29,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f30,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f32,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
fof(f33,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
fof(f34,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f36,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
fof(f37,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
fof(f38,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
fof(f40,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
fof(f41,axiom,
! [X0,X1] :
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f42,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f43,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f44,axiom,
! [X2,X3,X0,X1] :
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f45,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
fof(f46,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ product(X1,X0,X3)
| ~ product(X0,X1,X2)
| product(X2,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f50,plain,
! [X0,X1] :
( ~ product(X0,X0,X1)
| equalish(X1,X0) ),
inference(resolution,[],[f42,f45]) ).
fof(f52,plain,
! [X0,X1] :
( ~ product(X0,X1,X0)
| equalish(X1,X0) ),
inference(resolution,[],[f43,f45]) ).
fof(f54,plain,
! [X0,X1] :
( ~ product(X0,X1,X1)
| equalish(X0,X1) ),
inference(resolution,[],[f44,f45]) ).
fof(f56,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_5) ),
inference(resolution,[],[f41,f16]) ).
fof(f57,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_5) ),
inference(resolution,[],[f41,f17]) ).
fof(f58,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_5) ),
inference(resolution,[],[f41,f18]) ).
fof(f59,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_5) ),
inference(resolution,[],[f41,f19]) ).
fof(f60,plain,
! [X0] :
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_5) ),
inference(resolution,[],[f41,f20]) ).
fof(f62,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[],[f56,f17]) ).
fof(f63,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(resolution,[],[f56,f18]) ).
fof(f65,plain,
( product(e_5,e_1,e_1)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_5) ),
inference(resolution,[],[f56,f20]) ).
fof(f67,definition,
( spl0_1
<=> product(e_5,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f69,plain,
( product(e_5,e_1,e_5)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f71,definition,
( spl0_2
<=> product(e_5,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f73,plain,
( product(e_5,e_1,e_4)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f75,definition,
( spl0_3
<=> product(e_5,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f77,plain,
( product(e_5,e_1,e_3)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f79,definition,
( spl0_4
<=> product(e_5,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f81,plain,
( product(e_5,e_1,e_2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f83,definition,
( spl0_5
<=> product(e_5,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f85,plain,
( product(e_5,e_1,e_1)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f86,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f65,f83,f79,f75,f71,f67]) ).
fof(f96,definition,
( spl0_8
<=> product(e_4,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f97,plain,
( ~ product(e_4,e_1,e_3)
| spl0_8 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f98,plain,
( product(e_4,e_1,e_3)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f100,definition,
( spl0_9
<=> product(e_4,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f101,plain,
( ~ product(e_4,e_1,e_2)
| spl0_9 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f102,plain,
( product(e_4,e_1,e_2)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f109,definition,
( spl0_11
<=> product(e_3,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f111,plain,
( product(e_3,e_1,e_5)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f113,definition,
( spl0_12
<=> product(e_3,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f115,plain,
( product(e_3,e_1,e_4)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f117,definition,
( spl0_13
<=> product(e_3,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f119,plain,
( product(e_3,e_1,e_3)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f121,definition,
( spl0_14
<=> product(e_3,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f123,plain,
( product(e_3,e_1,e_2)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f125,definition,
( spl0_15
<=> product(e_3,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f127,plain,
( product(e_3,e_1,e_1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f63,f125,f121,f117,f113,f109]) ).
fof(f130,definition,
( spl0_16
<=> product(e_2,e_1,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f131,plain,
( ~ product(e_2,e_1,e_5)
| spl0_16 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f132,plain,
( product(e_2,e_1,e_5)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f134,definition,
( spl0_17
<=> product(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f135,plain,
( ~ product(e_2,e_1,e_4)
| spl0_17 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f136,plain,
( product(e_2,e_1,e_4)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f138,definition,
( spl0_18
<=> product(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f140,plain,
( product(e_2,e_1,e_3)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f142,definition,
( spl0_19
<=> product(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f144,plain,
( product(e_2,e_1,e_2)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f146,definition,
( spl0_20
<=> product(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f148,plain,
( product(e_2,e_1,e_1)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f62,f146,f142,f138,f134,f130]) ).
fof(f151,plain,
( ! [X0] :
( ~ product(X0,e_1,e_4)
| equalish(X0,e_5) )
| ~ spl0_2 ),
inference(resolution,[],[f73,f44]) ).
fof(f160,plain,
( ! [X0] :
( ~ greater(e_5,X0)
| ~ next(e_3,X0) )
| ~ spl0_11 ),
inference(resolution,[],[f111,f15]) ).
fof(f179,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[],[f57,f18]) ).
fof(f181,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_5) ),
inference(resolution,[],[f57,f20]) ).
fof(f183,definition,
( spl0_21
<=> product(e_5,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f185,plain,
( product(e_5,e_2,e_5)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f187,definition,
( spl0_22
<=> product(e_5,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f189,plain,
( product(e_5,e_2,e_4)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f191,definition,
( spl0_23
<=> product(e_5,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f193,plain,
( product(e_5,e_2,e_3)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f195,definition,
( spl0_24
<=> product(e_5,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f197,plain,
( product(e_5,e_2,e_2)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f199,definition,
( spl0_25
<=> product(e_5,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f201,plain,
( product(e_5,e_2,e_1)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f181,f199,f195,f191,f187,f183]) ).
fof(f212,definition,
( spl0_28
<=> product(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f214,plain,
( product(e_4,e_2,e_3)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f225,definition,
( spl0_31
<=> product(e_3,e_2,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f226,plain,
( ~ product(e_3,e_2,e_5)
| spl0_31 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( product(e_3,e_2,e_5)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl0_32
<=> product(e_3,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f231,plain,
( product(e_3,e_2,e_4)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_33
<=> product(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f235,plain,
( product(e_3,e_2,e_3)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f237,definition,
( spl0_34
<=> product(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f239,plain,
( product(e_3,e_2,e_2)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f241,definition,
( spl0_35
<=> product(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f243,plain,
( product(e_3,e_2,e_1)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f244,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(avatar_split_clause,[],[f179,f241,f237,f233,f229,f225]) ).
fof(f270,plain,
( equalish(e_2,e_5)
| ~ spl0_21 ),
inference(resolution,[],[f185,f52]) ).
fof(f271,plain,
( $false
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f270,f28]) ).
fof(f272,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f271]) ).
fof(f284,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_5,e_2) )
| ~ spl0_31 ),
inference(resolution,[],[f227,f46]) ).
fof(f299,plain,
( ! [X0] :
( ~ greater(e_4,X0)
| ~ next(e_2,X0) )
| ~ spl0_17 ),
inference(resolution,[],[f136,f15]) ).
fof(f324,plain,
( ~ next(e_3,e_4)
| ~ spl0_11 ),
inference(resolution,[],[f160,f14]) ).
fof(f325,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f324,f3]) ).
fof(f326,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f325]) ).
fof(f331,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_4,e_1) )
| ~ spl0_12 ),
inference(resolution,[],[f115,f46]) ).
fof(f334,plain,
( ~ next(e_2,e_3)
| ~ spl0_17 ),
inference(resolution,[],[f299,f12]) ).
fof(f335,plain,
( $false
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f334,f2]) ).
fof(f336,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f335]) ).
fof(f365,plain,
( equalish(e_3,e_5)
| ~ spl0_2
| ~ spl0_12 ),
inference(resolution,[],[f151,f115]) ).
fof(f367,plain,
( $false
| ~ spl0_2
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f365,f32]) ).
fof(f368,plain,
( ~ spl0_2
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f367]) ).
fof(f389,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(resolution,[],[f58,f16]) ).
fof(f390,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(resolution,[],[f58,f17]) ).
fof(f416,definition,
( spl0_46
<=> product(e_2,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f417,plain,
( ~ product(e_2,e_3,e_5)
| spl0_46 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( product(e_2,e_3,e_5)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f420,definition,
( spl0_47
<=> product(e_2,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f422,plain,
( product(e_2,e_3,e_4)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f424,definition,
( spl0_48
<=> product(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f426,plain,
( product(e_2,e_3,e_3)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f428,definition,
( spl0_49
<=> product(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f430,plain,
( product(e_2,e_3,e_2)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f432,definition,
( spl0_50
<=> product(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f434,plain,
( product(e_2,e_3,e_1)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,plain,
( spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f390,f432,f428,f424,f420,f416]) ).
fof(f437,definition,
( spl0_51
<=> product(e_1,e_3,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f439,plain,
( product(e_1,e_3,e_5)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f441,definition,
( spl0_52
<=> product(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f442,plain,
( ~ product(e_1,e_3,e_4)
| spl0_52 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f443,plain,
( product(e_1,e_3,e_4)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f445,definition,
( spl0_53
<=> product(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f447,plain,
( product(e_1,e_3,e_3)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f449,definition,
( spl0_54
<=> product(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f451,plain,
( product(e_1,e_3,e_2)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f453,definition,
( spl0_55
<=> product(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f455,plain,
( product(e_1,e_3,e_1)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f456,plain,
( spl0_51
| spl0_52
| spl0_53
| spl0_54
| spl0_55 ),
inference(avatar_split_clause,[],[f389,f453,f449,f445,f441,f437]) ).
fof(f466,plain,
( product(e_5,e_5,e_2)
| ~ spl0_31
| ~ spl0_46 ),
inference(resolution,[],[f418,f284]) ).
fof(f470,plain,
( ! [X0] :
( ~ product(e_3,e_2,X0)
| product(X0,e_5,e_3) )
| ~ spl0_46 ),
inference(resolution,[],[f418,f46]) ).
fof(f472,plain,
( equalish(e_2,e_5)
| ~ spl0_31
| ~ spl0_46 ),
inference(resolution,[],[f466,f50]) ).
fof(f478,plain,
( $false
| ~ spl0_31
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f472,f28]) ).
fof(f479,plain,
( ~ spl0_31
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f478]) ).
fof(f486,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_4,e_2) )
| ~ spl0_32 ),
inference(resolution,[],[f231,f46]) ).
fof(f497,plain,
( product(e_5,e_4,e_2)
| ~ spl0_32
| ~ spl0_46 ),
inference(resolution,[],[f486,f418]) ).
fof(f500,plain,
( ! [X0] :
( ~ product(e_5,e_4,X0)
| equalish(X0,e_2) )
| ~ spl0_32
| ~ spl0_46 ),
inference(resolution,[],[f497,f42]) ).
fof(f512,plain,
( product(e_5,e_4,e_1)
| ~ spl0_12
| ~ spl0_51 ),
inference(resolution,[],[f439,f331]) ).
fof(f516,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_5,e_3) )
| ~ spl0_51 ),
inference(resolution,[],[f439,f46]) ).
fof(f518,plain,
( equalish(e_1,e_2)
| ~ spl0_12
| ~ spl0_32
| ~ spl0_46
| ~ spl0_51 ),
inference(resolution,[],[f512,f500]) ).
fof(f526,plain,
( $false
| ~ spl0_12
| ~ spl0_32
| ~ spl0_46
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f518,f21]) ).
fof(f527,plain,
( ~ spl0_12
| ~ spl0_32
| ~ spl0_46
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f526]) ).
fof(f534,plain,
( equalish(e_1,e_3)
| ~ spl0_13 ),
inference(resolution,[],[f119,f52]) ).
fof(f535,plain,
( $false
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f534,f22]) ).
fof(f536,plain,
~ spl0_13,
inference(avatar_contradiction_clause,[],[f535]) ).
fof(f537,plain,
( product(e_2,e_5,e_3)
| ~ spl0_14
| ~ spl0_51 ),
inference(resolution,[],[f123,f516]) ).
fof(f552,plain,
( equalish(e_3,e_1)
| ~ spl0_15 ),
inference(resolution,[],[f127,f54]) ).
fof(f553,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f552,f29]) ).
fof(f554,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f553]) ).
fof(f596,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_4,e_1) )
| ~ spl0_12 ),
inference(resolution,[],[f115,f46]) ).
fof(f613,plain,
( equalish(e_1,e_2)
| ~ spl0_19 ),
inference(resolution,[],[f144,f52]) ).
fof(f614,plain,
( $false
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f613,f21]) ).
fof(f615,plain,
~ spl0_19,
inference(avatar_contradiction_clause,[],[f614]) ).
fof(f622,plain,
( equalish(e_2,e_1)
| ~ spl0_20 ),
inference(resolution,[],[f148,f54]) ).
fof(f623,plain,
( $false
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f622,f25]) ).
fof(f624,plain,
~ spl0_20,
inference(avatar_contradiction_clause,[],[f623]) ).
fof(f635,plain,
( equalish(e_2,e_3)
| ~ spl0_33 ),
inference(resolution,[],[f235,f52]) ).
fof(f636,plain,
( $false
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f635,f26]) ).
fof(f637,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f636]) ).
fof(f643,plain,
( equalish(e_3,e_2)
| ~ spl0_34 ),
inference(resolution,[],[f239,f54]) ).
fof(f644,plain,
( $false
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f643,f30]) ).
fof(f645,plain,
~ spl0_34,
inference(avatar_contradiction_clause,[],[f644]) ).
fof(f650,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_5) ),
inference(resolution,[],[f59,f20]) ).
fof(f673,definition,
( spl0_66
<=> product(e_2,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f675,plain,
( product(e_2,e_4,e_5)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f681,definition,
( spl0_68
<=> product(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f682,plain,
( ~ product(e_2,e_4,e_3)
| spl0_68 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( product(e_2,e_4,e_3)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f706,definition,
( spl0_74
<=> product(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f708,plain,
( product(e_1,e_4,e_2)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f714,plain,
( product(e_1,e_5,e_3)
| ~ spl0_35
| ~ spl0_46 ),
inference(resolution,[],[f243,f470]) ).
fof(f721,plain,
( ! [X0] :
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1) )
| ~ spl0_35
| ~ spl0_46 ),
inference(resolution,[],[f714,f44]) ).
fof(f728,definition,
( spl0_76
<=> product(e_5,e_4,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f730,plain,
( product(e_5,e_4,e_5)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f732,definition,
( spl0_77
<=> product(e_5,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f734,plain,
( product(e_5,e_4,e_4)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f736,definition,
( spl0_78
<=> product(e_5,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f738,plain,
( product(e_5,e_4,e_3)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f740,definition,
( spl0_79
<=> product(e_5,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f742,plain,
( product(e_5,e_4,e_2)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f740]) ).
fof(f744,definition,
( spl0_80
<=> product(e_5,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f746,plain,
( product(e_5,e_4,e_1)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f747,plain,
( spl0_76
| spl0_77
| spl0_78
| spl0_79
| spl0_80 ),
inference(avatar_split_clause,[],[f650,f744,f740,f736,f732,f728]) ).
fof(f766,plain,
( ! [X0] :
( ~ product(e_1,e_5,X0)
| product(X0,e_2,e_1) )
| ~ spl0_4 ),
inference(resolution,[],[f81,f46]) ).
fof(f788,plain,
( product(e_4,e_4,e_1)
| ~ spl0_12
| ~ spl0_52 ),
inference(resolution,[],[f443,f596]) ).
fof(f793,plain,
( equalish(e_1,e_4)
| ~ spl0_12
| ~ spl0_52 ),
inference(resolution,[],[f788,f50]) ).
fof(f800,plain,
( $false
| ~ spl0_12
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f793,f23]) ).
fof(f801,plain,
( ~ spl0_12
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f800]) ).
fof(f808,plain,
( equalish(e_1,e_3)
| ~ spl0_53 ),
inference(resolution,[],[f447,f54]) ).
fof(f809,plain,
( $false
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f808,f22]) ).
fof(f810,plain,
~ spl0_53,
inference(avatar_contradiction_clause,[],[f809]) ).
fof(f825,plain,
( equalish(e_3,e_1)
| ~ spl0_55 ),
inference(resolution,[],[f455,f52]) ).
fof(f826,plain,
( $false
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f825,f29]) ).
fof(f827,plain,
~ spl0_55,
inference(avatar_contradiction_clause,[],[f826]) ).
fof(f833,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_2,e_3) )
| ~ spl0_54 ),
inference(resolution,[],[f451,f46]) ).
fof(f834,plain,
( product(e_4,e_2,e_3)
| ~ spl0_12
| ~ spl0_54 ),
inference(resolution,[],[f833,f115]) ).
fof(f835,plain,
( spl0_28
| ~ spl0_12
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f834,f449,f113,f212]) ).
fof(f915,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_3,e_2) )
| ~ spl0_23 ),
inference(resolution,[],[f193,f46]) ).
fof(f922,plain,
( ! [X0] :
( ~ product(e_4,e_2,X0)
| product(X0,e_5,e_4) )
| ~ spl0_66 ),
inference(resolution,[],[f675,f46]) ).
fof(f935,plain,
( product(e_3,e_5,e_4)
| ~ spl0_28
| ~ spl0_66 ),
inference(resolution,[],[f922,f214]) ).
fof(f940,plain,
( ! [X0] :
( ~ product(e_3,X0,e_4)
| equalish(X0,e_5) )
| ~ spl0_28
| ~ spl0_66 ),
inference(resolution,[],[f935,f43]) ).
fof(f950,plain,
( product(e_1,e_5,e_1)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_5) ),
inference(resolution,[],[f60,f16]) ).
fof(f951,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_5) ),
inference(resolution,[],[f60,f17]) ).
fof(f953,plain,
( product(e_4,e_5,e_1)
| product(e_4,e_5,e_2)
| product(e_4,e_5,e_3)
| product(e_4,e_5,e_4)
| product(e_4,e_5,e_5) ),
inference(resolution,[],[f60,f19]) ).
fof(f956,definition,
( spl0_81
<=> product(e_4,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f958,plain,
( product(e_4,e_5,e_5)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f960,definition,
( spl0_82
<=> product(e_4,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f962,plain,
( product(e_4,e_5,e_4)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f964,definition,
( spl0_83
<=> product(e_4,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f966,plain,
( product(e_4,e_5,e_3)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f964]) ).
fof(f968,definition,
( spl0_84
<=> product(e_4,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f970,plain,
( product(e_4,e_5,e_2)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f972,definition,
( spl0_85
<=> product(e_4,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f974,plain,
( product(e_4,e_5,e_1)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f975,plain,
( spl0_81
| spl0_82
| spl0_83
| spl0_84
| spl0_85 ),
inference(avatar_split_clause,[],[f953,f972,f968,f964,f960,f956]) ).
fof(f977,definition,
( spl0_86
<=> product(e_2,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f979,plain,
( product(e_2,e_5,e_5)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f981,definition,
( spl0_87
<=> product(e_2,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f983,plain,
( product(e_2,e_5,e_4)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f985,definition,
( spl0_88
<=> product(e_2,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f987,plain,
( product(e_2,e_5,e_3)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f989,definition,
( spl0_89
<=> product(e_2,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f991,plain,
( product(e_2,e_5,e_2)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f993,definition,
( spl0_90
<=> product(e_2,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f995,plain,
( product(e_2,e_5,e_1)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f996,plain,
( spl0_86
| spl0_87
| spl0_88
| spl0_89
| spl0_90 ),
inference(avatar_split_clause,[],[f951,f993,f989,f985,f981,f977]) ).
fof(f997,plain,
( equalish(e_1,e_5)
| ~ spl0_12
| ~ spl0_28
| ~ spl0_66 ),
inference(resolution,[],[f940,f115]) ).
fof(f999,plain,
( $false
| ~ spl0_12
| ~ spl0_28
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f997,f24]) ).
fof(f1000,plain,
( ~ spl0_12
| ~ spl0_28
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f999]) ).
fof(f1138,plain,
( ! [X0] :
( ~ product(e_4,e_5,X0)
| product(X0,e_2,e_4) )
| ~ spl0_79 ),
inference(resolution,[],[f742,f46]) ).
fof(f1144,plain,
( equalish(e_4,e_5)
| ~ spl0_81 ),
inference(resolution,[],[f958,f54]) ).
fof(f1145,plain,
( $false
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f1144,f36]) ).
fof(f1146,plain,
~ spl0_81,
inference(avatar_contradiction_clause,[],[f1145]) ).
fof(f1154,plain,
( equalish(e_5,e_4)
| ~ spl0_82 ),
inference(resolution,[],[f962,f52]) ).
fof(f1155,plain,
( $false
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1154,f40]) ).
fof(f1156,plain,
~ spl0_82,
inference(avatar_contradiction_clause,[],[f1155]) ).
fof(f1159,plain,
( equalish(e_4,e_1)
| ~ spl0_35
| ~ spl0_46
| ~ spl0_83 ),
inference(resolution,[],[f966,f721]) ).
fof(f1164,plain,
( $false
| ~ spl0_35
| ~ spl0_46
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f1159,f33]) ).
fof(f1165,plain,
( ~ spl0_35
| ~ spl0_46
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
fof(f1168,plain,
( product(e_2,e_2,e_4)
| ~ spl0_79
| ~ spl0_84 ),
inference(resolution,[],[f970,f1138]) ).
fof(f1172,plain,
( ! [X0] :
( ~ product(e_5,e_4,X0)
| product(X0,e_2,e_5) )
| ~ spl0_84 ),
inference(resolution,[],[f970,f46]) ).
fof(f1173,plain,
( equalish(e_4,e_2)
| ~ spl0_79
| ~ spl0_84 ),
inference(resolution,[],[f1168,f50]) ).
fof(f1180,plain,
( $false
| ~ spl0_79
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f1173,f34]) ).
fof(f1181,plain,
( ~ spl0_79
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f1180]) ).
fof(f1187,plain,
( equalish(e_4,e_5)
| ~ spl0_76 ),
inference(resolution,[],[f730,f52]) ).
fof(f1188,plain,
( $false
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1187,f36]) ).
fof(f1189,plain,
~ spl0_76,
inference(avatar_contradiction_clause,[],[f1188]) ).
fof(f1197,plain,
( equalish(e_5,e_4)
| ~ spl0_77 ),
inference(resolution,[],[f734,f54]) ).
fof(f1198,plain,
( $false
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1197,f40]) ).
fof(f1199,plain,
~ spl0_77,
inference(avatar_contradiction_clause,[],[f1198]) ).
fof(f1202,plain,
( product(e_3,e_2,e_5)
| ~ spl0_78
| ~ spl0_84 ),
inference(resolution,[],[f738,f1172]) ).
fof(f1207,plain,
( $false
| spl0_31
| ~ spl0_78
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f1202,f226]) ).
fof(f1208,plain,
( spl0_31
| ~ spl0_78
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1213,plain,
( ! [X0] :
( ~ product(e_4,e_5,X0)
| product(X0,e_1,e_4) )
| ~ spl0_80 ),
inference(resolution,[],[f746,f46]) ).
fof(f1214,plain,
( product(e_2,e_1,e_4)
| ~ spl0_80
| ~ spl0_84 ),
inference(resolution,[],[f1213,f970]) ).
fof(f1215,plain,
( $false
| spl0_17
| ~ spl0_80
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f1214,f135]) ).
fof(f1216,plain,
( spl0_17
| ~ spl0_80
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f1215]) ).
fof(f1230,definition,
( spl0_96
<=> product(e_1,e_5,e_5) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f1232,plain,
( product(e_1,e_5,e_5)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1234,definition,
( spl0_97
<=> product(e_1,e_5,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f1236,plain,
( product(e_1,e_5,e_4)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f1234]) ).
fof(f1238,definition,
( spl0_98
<=> product(e_1,e_5,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f1240,plain,
( product(e_1,e_5,e_3)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1242,definition,
( spl0_99
<=> product(e_1,e_5,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f1243,plain,
( ~ product(e_1,e_5,e_2)
| spl0_99 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1244,plain,
( product(e_1,e_5,e_2)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1246,definition,
( spl0_100
<=> product(e_1,e_5,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f1248,plain,
( product(e_1,e_5,e_1)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f1246]) ).
fof(f1249,plain,
( spl0_96
| spl0_97
| spl0_98
| spl0_99
| spl0_100 ),
inference(avatar_split_clause,[],[f950,f1246,f1242,f1238,f1234,f1230]) ).
fof(f1280,plain,
( ! [X0] :
( ~ product(e_1,e_4,X0)
| product(X0,e_2,e_1) )
| ~ spl0_9 ),
inference(resolution,[],[f102,f46]) ).
fof(f1285,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_1,e_2) )
| ~ spl0_25 ),
inference(resolution,[],[f201,f46]) ).
fof(f1290,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_4,e_2) )
| ~ spl0_32 ),
inference(resolution,[],[f231,f46]) ).
fof(f1312,plain,
( equalish(e_5,e_2)
| ~ spl0_89 ),
inference(resolution,[],[f991,f52]) ).
fof(f1313,plain,
( $false
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1312,f38]) ).
fof(f1314,plain,
~ spl0_89,
inference(avatar_contradiction_clause,[],[f1313]) ).
fof(f1358,plain,
( ! [X0] :
( ~ greater(e_5,X0)
| ~ next(e_2,X0) )
| ~ spl0_16 ),
inference(resolution,[],[f132,f15]) ).
fof(f1405,plain,
( equalish(e_5,e_1)
| ~ spl0_100 ),
inference(resolution,[],[f1248,f52]) ).
fof(f1406,plain,
( $false
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f1405,f37]) ).
fof(f1407,plain,
~ spl0_100,
inference(avatar_contradiction_clause,[],[f1406]) ).
fof(f1415,plain,
( equalish(e_1,e_5)
| ~ spl0_96 ),
inference(resolution,[],[f1232,f54]) ).
fof(f1416,plain,
( $false
| ~ spl0_96 ),
inference(forward_subsumption_resolution,[],[f1415,f24]) ).
fof(f1417,plain,
~ spl0_96,
inference(avatar_contradiction_clause,[],[f1416]) ).
fof(f1418,plain,
( product(e_2,e_2,e_1)
| ~ spl0_4
| ~ spl0_99 ),
inference(resolution,[],[f1244,f766]) ).
fof(f1423,plain,
( equalish(e_1,e_2)
| ~ spl0_4
| ~ spl0_99 ),
inference(resolution,[],[f1418,f50]) ).
fof(f1430,plain,
( $false
| ~ spl0_4
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f1423,f21]) ).
fof(f1431,plain,
( ~ spl0_4
| ~ spl0_99 ),
inference(avatar_contradiction_clause,[],[f1430]) ).
fof(f1438,plain,
( equalish(e_1,e_5)
| ~ spl0_1 ),
inference(resolution,[],[f69,f52]) ).
fof(f1439,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f1438,f24]) ).
fof(f1440,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f1439]) ).
fof(f1449,plain,
( equalish(e_5,e_1)
| ~ spl0_5 ),
inference(resolution,[],[f85,f54]) ).
fof(f1450,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1449,f37]) ).
fof(f1451,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f1450]) ).
fof(f1458,plain,
( ! [X0] :
( ~ product(e_1,e_5,X0)
| product(X0,e_2,e_1) )
| ~ spl0_4 ),
inference(resolution,[],[f81,f46]) ).
fof(f1459,plain,
( product(e_3,e_2,e_1)
| ~ spl0_4
| ~ spl0_98 ),
inference(resolution,[],[f1240,f1458]) ).
fof(f1493,plain,
( spl0_35
| ~ spl0_4
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f1459,f1238,f79,f241]) ).
fof(f1504,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_1,e_2) )
| ~ spl0_35 ),
inference(resolution,[],[f243,f46]) ).
fof(f1517,plain,
( equalish(e_2,e_3)
| ~ spl0_48 ),
inference(resolution,[],[f426,f54]) ).
fof(f1518,plain,
( $false
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1517,f26]) ).
fof(f1519,plain,
~ spl0_48,
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1530,plain,
( equalish(e_3,e_2)
| ~ spl0_49 ),
inference(resolution,[],[f430,f52]) ).
fof(f1531,plain,
( $false
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1530,f30]) ).
fof(f1532,plain,
~ spl0_49,
inference(avatar_contradiction_clause,[],[f1531]) ).
fof(f1536,plain,
( product(e_4,e_1,e_2)
| ~ spl0_35
| ~ spl0_47 ),
inference(resolution,[],[f422,f1504]) ).
fof(f1537,plain,
( product(e_4,e_4,e_2)
| ~ spl0_32
| ~ spl0_47 ),
inference(resolution,[],[f422,f1290]) ).
fof(f1542,plain,
( equalish(e_2,e_4)
| ~ spl0_32
| ~ spl0_47 ),
inference(resolution,[],[f1537,f50]) ).
fof(f1549,plain,
( $false
| ~ spl0_32
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1542,f27]) ).
fof(f1550,plain,
( ~ spl0_32
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f1549]) ).
fof(f1551,plain,
( product(e_1,e_1,e_2)
| ~ spl0_35
| ~ spl0_50 ),
inference(resolution,[],[f434,f1504]) ).
fof(f1559,plain,
( equalish(e_2,e_1)
| ~ spl0_35
| ~ spl0_50 ),
inference(resolution,[],[f1551,f50]) ).
fof(f1567,plain,
( $false
| ~ spl0_35
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1559,f25]) ).
fof(f1568,plain,
( ~ spl0_35
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1567]) ).
fof(f1583,plain,
( product(e_2,e_2,e_1)
| ~ spl0_9
| ~ spl0_74 ),
inference(resolution,[],[f708,f1280]) ).
fof(f1588,plain,
( equalish(e_1,e_2)
| ~ spl0_9
| ~ spl0_74 ),
inference(resolution,[],[f1583,f50]) ).
fof(f1595,plain,
( $false
| ~ spl0_9
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1588,f21]) ).
fof(f1596,plain,
( ~ spl0_9
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1595]) ).
fof(f1601,plain,
( ! [X0] :
( ~ product(e_5,e_4,X0)
| product(X0,e_1,e_5) )
| ~ spl0_85 ),
inference(resolution,[],[f974,f46]) ).
fof(f1602,plain,
( product(e_2,e_1,e_5)
| ~ spl0_79
| ~ spl0_85 ),
inference(resolution,[],[f1601,f742]) ).
fof(f1607,plain,
( ! [X0] :
( ~ product(e_5,e_1,X0)
| product(X0,e_3,e_5) )
| ~ spl0_98 ),
inference(resolution,[],[f1240,f46]) ).
fof(f1608,plain,
( product(e_2,e_3,e_5)
| ~ spl0_4
| ~ spl0_98 ),
inference(resolution,[],[f1607,f81]) ).
fof(f1609,plain,
( $false
| ~ spl0_4
| spl0_46
| ~ spl0_98 ),
inference(forward_subsumption_resolution,[],[f1608,f417]) ).
fof(f1610,plain,
( ~ spl0_4
| spl0_46
| ~ spl0_98 ),
inference(avatar_contradiction_clause,[],[f1609]) ).
fof(f1611,plain,
( spl0_80
| ~ spl0_12
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f512,f437,f113,f744]) ).
fof(f1627,plain,
( ! [X0] :
( ~ product(e_3,e_1,X0)
| product(X0,e_4,e_3) )
| ~ spl0_52 ),
inference(resolution,[],[f443,f46]) ).
fof(f1628,plain,
( product(e_2,e_4,e_3)
| ~ spl0_14
| ~ spl0_52 ),
inference(resolution,[],[f1627,f123]) ).
fof(f1647,plain,
( ! [X0] :
( ~ product(X0,e_5,e_4)
| equalish(X0,e_1) )
| ~ spl0_97 ),
inference(resolution,[],[f1236,f44]) ).
fof(f1650,plain,
( ! [X0] :
( ~ product(e_5,e_1,X0)
| product(X0,e_4,e_5) )
| ~ spl0_97 ),
inference(resolution,[],[f1236,f46]) ).
fof(f1651,plain,
( product(e_2,e_4,e_5)
| ~ spl0_4
| ~ spl0_97 ),
inference(resolution,[],[f1650,f81]) ).
fof(f1663,plain,
( ~ next(e_2,e_3)
| ~ spl0_16 ),
inference(resolution,[],[f1358,f13]) ).
fof(f1665,plain,
( $false
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1663,f2]) ).
fof(f1666,plain,
~ spl0_16,
inference(avatar_contradiction_clause,[],[f1665]) ).
fof(f1671,plain,
( $false
| spl0_16
| ~ spl0_79
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f1602,f131]) ).
fof(f1672,plain,
( spl0_16
| ~ spl0_79
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f1671]) ).
fof(f1681,plain,
( ! [X0] :
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) )
| ~ spl0_18 ),
inference(resolution,[],[f140,f44]) ).
fof(f1682,plain,
( ! [X0] :
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) )
| ~ spl0_18 ),
inference(resolution,[],[f140,f43]) ).
fof(f1755,plain,
( equalish(e_2,e_5)
| ~ spl0_86 ),
inference(resolution,[],[f979,f54]) ).
fof(f1756,plain,
( $false
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f1755,f28]) ).
fof(f1757,plain,
~ spl0_86,
inference(avatar_contradiction_clause,[],[f1756]) ).
fof(f1760,plain,
( product(e_1,e_1,e_2)
| ~ spl0_25
| ~ spl0_90 ),
inference(resolution,[],[f995,f1285]) ).
fof(f1761,plain,
( product(e_1,e_3,e_2)
| ~ spl0_23
| ~ spl0_90 ),
inference(resolution,[],[f995,f915]) ).
fof(f1769,plain,
( equalish(e_2,e_1)
| ~ spl0_25
| ~ spl0_90 ),
inference(resolution,[],[f1760,f50]) ).
fof(f1777,plain,
( $false
| ~ spl0_25
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f1769,f25]) ).
fof(f1778,plain,
( ~ spl0_25
| ~ spl0_90 ),
inference(avatar_contradiction_clause,[],[f1777]) ).
fof(f1783,plain,
( ! [X0] :
( ~ product(e_2,e_5,X0)
| product(X0,e_4,e_2) )
| ~ spl0_22 ),
inference(resolution,[],[f189,f46]) ).
fof(f1784,plain,
( product(e_1,e_4,e_2)
| ~ spl0_22
| ~ spl0_90 ),
inference(resolution,[],[f1783,f995]) ).
fof(f1813,plain,
( equalish(e_5,e_2)
| ~ spl0_24 ),
inference(resolution,[],[f197,f54]) ).
fof(f1814,plain,
( $false
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1813,f38]) ).
fof(f1815,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f1814]) ).
fof(f1846,plain,
( ! [X0] :
( ~ product(e_2,e_3,X0)
| product(X0,e_5,e_2) )
| ~ spl0_31 ),
inference(resolution,[],[f227,f46]) ).
fof(f1853,plain,
( product(e_4,e_5,e_2)
| ~ spl0_31
| ~ spl0_47 ),
inference(resolution,[],[f422,f1846]) ).
fof(f1860,plain,
( product(e_1,e_5,e_2)
| ~ spl0_31
| ~ spl0_50 ),
inference(resolution,[],[f434,f1846]) ).
fof(f1865,plain,
( $false
| ~ spl0_31
| ~ spl0_50
| spl0_99 ),
inference(forward_subsumption_resolution,[],[f1860,f1243]) ).
fof(f1866,plain,
( ~ spl0_31
| ~ spl0_50
| spl0_99 ),
inference(avatar_contradiction_clause,[],[f1865]) ).
fof(f2044,plain,
( equalish(e_2,e_1)
| ~ spl0_87
| ~ spl0_97 ),
inference(resolution,[],[f1647,f983]) ).
fof(f2045,plain,
( $false
| ~ spl0_87
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f2044,f25]) ).
fof(f2046,plain,
( ~ spl0_87
| ~ spl0_97 ),
inference(avatar_contradiction_clause,[],[f2045]) ).
fof(f2052,plain,
( equalish(e_5,e_2)
| ~ spl0_3
| ~ spl0_18 ),
inference(resolution,[],[f1681,f77]) ).
fof(f2053,plain,
( $false
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2052,f38]) ).
fof(f2054,plain,
( ~ spl0_3
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2053]) ).
fof(f2055,plain,
( spl0_66
| ~ spl0_4
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f1651,f1234,f79,f673]) ).
fof(f2059,plain,
( spl0_88
| ~ spl0_14
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f537,f437,f121,f985]) ).
fof(f2061,plain,
( spl0_84
| ~ spl0_31
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1853,f420,f225,f968]) ).
fof(f2072,plain,
( equalish(e_4,e_2)
| ~ spl0_8
| ~ spl0_18 ),
inference(resolution,[],[f98,f1681]) ).
fof(f2078,plain,
( $false
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2072,f34]) ).
fof(f2079,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2078]) ).
fof(f2190,plain,
( equalish(e_5,e_1)
| ~ spl0_18
| ~ spl0_88 ),
inference(resolution,[],[f1682,f987]) ).
fof(f2191,plain,
( $false
| ~ spl0_18
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f2190,f37]) ).
fof(f2192,plain,
( ~ spl0_18
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f2191]) ).
fof(f2210,plain,
( ! [X0] :
( ~ product(e_3,e_2,X0)
| product(X0,e_1,e_3) )
| ~ spl0_50 ),
inference(resolution,[],[f434,f46]) ).
fof(f2211,plain,
( product(e_4,e_1,e_3)
| ~ spl0_32
| ~ spl0_50 ),
inference(resolution,[],[f2210,f231]) ).
fof(f2212,plain,
( $false
| spl0_8
| ~ spl0_32
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2211,f97]) ).
fof(f2213,plain,
( spl0_8
| ~ spl0_32
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2212]) ).
fof(f2216,plain,
( $false
| spl0_9
| ~ spl0_35
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1536,f101]) ).
fof(f2217,plain,
( spl0_9
| ~ spl0_35
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f2216]) ).
fof(f2218,plain,
( spl0_54
| ~ spl0_23
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1761,f993,f191,f449]) ).
fof(f2234,plain,
( ! [X0] :
( ~ product(e_1,e_3,X0)
| product(X0,e_2,e_1) )
| ~ spl0_14 ),
inference(resolution,[],[f123,f46]) ).
fof(f2249,plain,
( product(e_2,e_2,e_1)
| ~ spl0_14
| ~ spl0_54 ),
inference(resolution,[],[f451,f2234]) ).
fof(f2254,plain,
( equalish(e_1,e_2)
| ~ spl0_14
| ~ spl0_54 ),
inference(resolution,[],[f2249,f50]) ).
fof(f2262,plain,
( $false
| ~ spl0_14
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f2254,f21]) ).
fof(f2263,plain,
( ~ spl0_14
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
fof(f2264,plain,
( spl0_74
| ~ spl0_22
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1784,f993,f187,f706]) ).
fof(f2265,plain,
( $false
| ~ spl0_14
| ~ spl0_52
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f1628,f682]) ).
fof(f2266,plain,
( ~ spl0_14
| ~ spl0_52
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f2265]) ).
fof(f2283,plain,
( equalish(e_4,e_1)
| ~ spl0_18
| ~ spl0_68 ),
inference(resolution,[],[f683,f1682]) ).
fof(f2289,plain,
( $false
| ~ spl0_18
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f2283,f33]) ).
fof(f2290,plain,
( ~ spl0_18
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f2289]) ).
fof(f2292,plain,
( spl0_98
| ~ spl0_35
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f714,f416,f241,f1238]) ).
fof(f2337,plain,
( ! [X0] :
( ~ product(e_4,e_5,X0)
| product(X0,e_3,e_4) )
| ~ spl0_78 ),
inference(resolution,[],[f738,f46]) ).
fof(f2338,plain,
( product(e_1,e_3,e_4)
| ~ spl0_78
| ~ spl0_85 ),
inference(resolution,[],[f974,f2337]) ).
fof(f2342,plain,
( ! [X0] :
( ~ product(e_5,e_4,X0)
| product(X0,e_1,e_5) )
| ~ spl0_85 ),
inference(resolution,[],[f974,f46]) ).
fof(f2343,plain,
( $false
| spl0_52
| ~ spl0_78
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f2338,f442]) ).
fof(f2344,plain,
( spl0_52
| ~ spl0_78
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f2343]) ).
fof(f2345,plain,
( product(e_1,e_1,e_5)
| ~ spl0_80
| ~ spl0_85 ),
inference(resolution,[],[f746,f2342]) ).
fof(f2351,plain,
( equalish(e_5,e_1)
| ~ spl0_80
| ~ spl0_85 ),
inference(resolution,[],[f2345,f50]) ).
fof(f2359,plain,
( $false
| ~ spl0_80
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f2351,f37]) ).
fof(f2360,plain,
( ~ spl0_80
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f2359]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f86]) ).
cnf(s3,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f128]) ).
cnf(s4,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f149]) ).
cnf(s5,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f202]) ).
cnf(s7,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f244]) ).
cnf(s9,plain,
~ spl0_21,
inference(sat_conversion,[],[f272]) ).
cnf(s11,plain,
~ spl0_11,
inference(sat_conversion,[],[f326]) ).
cnf(s12,plain,
~ spl0_17,
inference(sat_conversion,[],[f336]) ).
cnf(s13,plain,
( ~ spl0_2
| ~ spl0_12 ),
inference(sat_conversion,[],[f368]) ).
cnf(s17,plain,
( spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f435]) ).
cnf(s18,plain,
( spl0_51
| spl0_52
| spl0_53
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f456]) ).
cnf(s19,plain,
( ~ spl0_31
| ~ spl0_46 ),
inference(sat_conversion,[],[f479]) ).
cnf(s23,plain,
( ~ spl0_12
| ~ spl0_32
| ~ spl0_46
| ~ spl0_51 ),
inference(sat_conversion,[],[f527]) ).
cnf(s24,plain,
~ spl0_13,
inference(sat_conversion,[],[f536]) ).
cnf(s26,plain,
~ spl0_15,
inference(sat_conversion,[],[f554]) ).
cnf(s29,plain,
~ spl0_19,
inference(sat_conversion,[],[f615]) ).
cnf(s30,plain,
~ spl0_20,
inference(sat_conversion,[],[f624]) ).
cnf(s31,plain,
~ spl0_33,
inference(sat_conversion,[],[f637]) ).
cnf(s32,plain,
~ spl0_34,
inference(sat_conversion,[],[f645]) ).
cnf(s37,plain,
( spl0_76
| spl0_77
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f747]) ).
cnf(s43,plain,
( ~ spl0_12
| ~ spl0_52 ),
inference(sat_conversion,[],[f801]) ).
cnf(s44,plain,
~ spl0_53,
inference(sat_conversion,[],[f810]) ).
cnf(s48,plain,
~ spl0_55,
inference(sat_conversion,[],[f827]) ).
cnf(s51,plain,
( ~ spl0_12
| spl0_28
| ~ spl0_54 ),
inference(sat_conversion,[],[f835]) ).
cnf(s66,plain,
( spl0_81
| spl0_82
| spl0_83
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f975]) ).
cnf(s67,plain,
( spl0_86
| spl0_87
| spl0_88
| spl0_89
| spl0_90 ),
inference(sat_conversion,[],[f996]) ).
cnf(s68,plain,
( ~ spl0_12
| ~ spl0_28
| ~ spl0_66 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s84,plain,
~ spl0_81,
inference(sat_conversion,[],[f1146]) ).
cnf(s86,plain,
~ spl0_82,
inference(sat_conversion,[],[f1156]) ).
cnf(s88,plain,
( ~ spl0_35
| ~ spl0_46
| ~ spl0_83 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s91,plain,
( ~ spl0_79
| ~ spl0_84 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s92,plain,
~ spl0_76,
inference(sat_conversion,[],[f1189]) ).
cnf(s94,plain,
~ spl0_77,
inference(sat_conversion,[],[f1199]) ).
cnf(s96,plain,
( spl0_31
| ~ spl0_78
| ~ spl0_84 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s97,plain,
( spl0_17
| ~ spl0_80
| ~ spl0_84 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s100,plain,
( spl0_96
| spl0_97
| spl0_98
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s105,plain,
~ spl0_89,
inference(sat_conversion,[],[f1314]) ).
cnf(s119,plain,
~ spl0_100,
inference(sat_conversion,[],[f1407]) ).
cnf(s121,plain,
~ spl0_96,
inference(sat_conversion,[],[f1417]) ).
cnf(s123,plain,
( ~ spl0_4
| ~ spl0_99 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s124,plain,
~ spl0_1,
inference(sat_conversion,[],[f1440]) ).
cnf(s126,plain,
~ spl0_5,
inference(sat_conversion,[],[f1451]) ).
cnf(s132,plain,
( ~ spl0_4
| spl0_35
| ~ spl0_98 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s134,plain,
~ spl0_48,
inference(sat_conversion,[],[f1519]) ).
cnf(s137,plain,
~ spl0_49,
inference(sat_conversion,[],[f1532]) ).
cnf(s141,plain,
( ~ spl0_32
| ~ spl0_47 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s144,plain,
( ~ spl0_35
| ~ spl0_50 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s147,plain,
( ~ spl0_9
| ~ spl0_74 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s148,plain,
( ~ spl0_4
| spl0_46
| ~ spl0_98 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s149,plain,
( ~ spl0_12
| ~ spl0_51
| spl0_80 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s154,plain,
~ spl0_16,
inference(sat_conversion,[],[f1666]) ).
cnf(s158,plain,
( spl0_16
| ~ spl0_79
| ~ spl0_85 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s170,plain,
~ spl0_86,
inference(sat_conversion,[],[f1757]) ).
cnf(s174,plain,
( ~ spl0_25
| ~ spl0_90 ),
inference(sat_conversion,[],[f1778]) ).
cnf(s178,plain,
~ spl0_24,
inference(sat_conversion,[],[f1815]) ).
cnf(s188,plain,
( ~ spl0_31
| ~ spl0_50
| spl0_99 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s209,plain,
( ~ spl0_87
| ~ spl0_97 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s212,plain,
( ~ spl0_3
| ~ spl0_18 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s215,plain,
( ~ spl0_4
| spl0_66
| ~ spl0_97 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s218,plain,
( ~ spl0_14
| ~ spl0_51
| spl0_88 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s220,plain,
( ~ spl0_31
| ~ spl0_47
| spl0_84 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s223,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s232,plain,
( ~ spl0_18
| ~ spl0_88 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s239,plain,
( spl0_8
| ~ spl0_32
| ~ spl0_50 ),
inference(sat_conversion,[],[f2213]) ).
cnf(s241,plain,
( spl0_9
| ~ spl0_35
| ~ spl0_47 ),
inference(sat_conversion,[],[f2217]) ).
cnf(s242,plain,
( ~ spl0_23
| spl0_54
| ~ spl0_90 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s246,plain,
( ~ spl0_14
| ~ spl0_54 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s247,plain,
( ~ spl0_22
| spl0_74
| ~ spl0_90 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s250,plain,
( ~ spl0_14
| ~ spl0_52
| spl0_68 ),
inference(sat_conversion,[],[f2266]) ).
cnf(s251,plain,
( ~ spl0_18
| ~ spl0_68 ),
inference(sat_conversion,[],[f2290]) ).
cnf(s256,plain,
( ~ spl0_35
| ~ spl0_46
| spl0_98 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s257,plain,
( spl0_52
| ~ spl0_78
| ~ spl0_85 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s259,plain,
( ~ spl0_80
| ~ spl0_85 ),
inference(sat_conversion,[],[f2360]) ).
cnf(s265,plain,
( spl0_97
| spl0_98
| spl0_99 ),
inference(rat,[],[s100,s119,s121]) ).
cnf(s269,plain,
( spl0_87
| spl0_88
| spl0_90 ),
inference(rat,[],[s67,s105,s170]) ).
cnf(s270,plain,
( spl0_83
| spl0_84
| spl0_85 ),
inference(rat,[],[s66,s86,s84]) ).
cnf(s275,plain,
( spl0_78
| spl0_79
| spl0_80 ),
inference(rat,[],[s37,s94,s92]) ).
cnf(s280,plain,
( spl0_51
| spl0_52
| spl0_54 ),
inference(rat,[],[s18,s48,s44]) ).
cnf(s281,plain,
( spl0_46
| spl0_47
| spl0_50 ),
inference(rat,[],[s17,s137,s134]) ).
cnf(s284,plain,
( spl0_31
| spl0_32
| spl0_35 ),
inference(rat,[],[s7,s32,s31]) ).
cnf(s286,plain,
( spl0_22
| spl0_23
| spl0_25 ),
inference(rat,[],[s5,s178,s9]) ).
cnf(s287,plain,
spl0_18,
inference(rat,[],[s4,s30,s29,s12,s154]) ).
cnf(s288,plain,
~ spl0_68,
inference(rat,[],[s251,s287]) ).
cnf(s289,plain,
~ spl0_88,
inference(rat,[],[s232,s287]) ).
cnf(s290,plain,
~ spl0_8,
inference(rat,[],[s223,s287]) ).
cnf(s291,plain,
~ spl0_3,
inference(rat,[],[s212,s287]) ).
cnf(s293,plain,
( spl0_12
| spl0_14 ),
inference(rat,[],[s3,s26,s24,s11]) ).
cnf(s295,plain,
( spl0_2
| spl0_4 ),
inference(rat,[],[s1,s126,s291,s124]) ).
cnf(s296,plain,
~ spl0_14,
inference(rat,[],[s280,s218,s246,s250,s289,s288]) ).
cnf(s297,plain,
spl0_12,
inference(rat,[],[s293,s296]) ).
cnf(s298,plain,
~ spl0_52,
inference(rat,[],[s43,s297]) ).
cnf(s299,plain,
( ~ spl0_80
| spl0_83 ),
inference(rat,[],[s270,s97,s259,s12]) ).
cnf(s300,plain,
( ~ spl0_78
| spl0_83
| spl0_31 ),
inference(rat,[],[s270,s96,s257,s298]) ).
cnf(s301,plain,
( ~ spl0_98
| ~ spl0_4 ),
inference(rat,[],[s270,s91,s158,s275,s300,s299,s88,s19,s132,s148,s154]) ).
cnf(s302,plain,
( ~ spl0_35
| ~ spl0_4 ),
inference(rat,[],[s281,s144,s241,s256,s147,s247,s286,s174,s242,s51,s68,s215,s269,s209,s265,s301,s123,s289,s297]) ).
cnf(s303,plain,
( ~ spl0_46
| ~ spl0_4 ),
inference(rat,[],[s284,s23,s19,s280,s51,s68,s215,s265,s301,s123,s302,s297,s298]) ).
cnf(s304,plain,
( ~ spl0_32
| spl0_46 ),
inference(rat,[],[s281,s141,s239,s290]) ).
cnf(s305,plain,
~ spl0_4,
inference(rat,[],[s281,s188,s220,s284,s304,s303,s302,s97,s149,s280,s51,s68,s215,s265,s301,s123,s12,s297,s298]) ).
cnf(s306,plain,
~ spl0_2,
inference(rat,[],[s13,s297]) ).
cnf(s307,plain,
$false,
inference(rat,[],[s295,s305,s306]) ).
fof(f2361,plain,
$false,
inference(avatar_sat_refutation,[],[s307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP125-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 09:22:19 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.42/1.50 % (2828854)Input is clausal, will run a generic CNF schedule.
% 3.42/1.50 % (2828862)lrs+10_1_sil=8000:sp=occurrence:random_seed=2419694751:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.42/1.50 % (2828862)Instruction limit reached!
% 3.42/1.50 % (2828862)------------------------------
% 3.42/1.50 % (2828862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828862)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828862)Termination reason: Instruction limit
% 3.42/1.50 % (2828862)Termination phase: Saturation
% 3.42/1.50 % (2828862)Time elapsed: 0.032 s
% 3.42/1.50 % (2828862)Peak memory usage: 88 MB
% 3.42/1.50 % (2828862)Instructions burned: 111 (million)
% 3.42/1.50 % (2828864)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4024876468:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.42/1.50 % (2828861)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=201807896:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.42/1.50 % (2828863)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4090369371:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.42/1.50 % (2828860)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1881554308:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.42/1.50 % (2828859)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=693278964:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.42/1.50 % (2828865)dis-21_1_sil=8000:lcm=predicate:random_seed=2810695166:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.42/1.50 % (2828863)Instruction limit reached!
% 3.42/1.50 % (2828863)------------------------------
% 3.42/1.50 % (2828863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828863)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828863)Termination reason: Instruction limit
% 3.42/1.50 % (2828863)Termination phase: Saturation
% 3.42/1.50 % (2828863)Time elapsed: 0.059 s
% 3.42/1.50 % (2828863)Peak memory usage: 88 MB
% 3.42/1.50 % (2828863)Instructions burned: 114 (million)
% 3.42/1.50 % (2828867)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=680264468:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.42/1.50 % (2828865)Instruction limit reached!
% 3.42/1.50 % (2828865)------------------------------
% 3.42/1.50 % (2828865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828865)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828865)Termination reason: Instruction limit
% 3.42/1.50 % (2828865)Termination phase: Saturation
% 3.42/1.50 % (2828865)Time elapsed: 0.080 s
% 3.42/1.50 % (2828865)Peak memory usage: 89 MB
% 3.42/1.50 % (2828865)Instructions burned: 118 (million)
% 3.42/1.50 % (2828864)Instruction limit reached!
% 3.42/1.50 % (2828864)------------------------------
% 3.42/1.50 % (2828864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828864)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828864)Termination reason: Instruction limit
% 3.42/1.50 % (2828864)Termination phase: Saturation
% 3.42/1.50 % (2828864)Time elapsed: 0.110 s
% 3.42/1.50 % (2828864)Peak memory usage: 89 MB
% 3.42/1.50 % (2828864)Instructions burned: 180 (million)
% 3.42/1.50 % (2828867)Instruction limit reached!
% 3.42/1.50 % (2828867)------------------------------
% 3.42/1.50 % (2828867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828867)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828867)Termination reason: Instruction limit
% 3.42/1.50 % (2828867)Termination phase: Saturation
% 3.42/1.50 % (2828867)Time elapsed: 0.042 s
% 3.42/1.50 % (2828867)Peak memory usage: 88 MB
% 3.42/1.50 % (2828867)Instructions burned: 144 (million)
% 3.42/1.50 % (2828874)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3146733500:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.42/1.50 % (2828874)Refutation not found, incomplete strategy
% 3.42/1.50 % (2828874)------------------------------
% 3.42/1.50 % (2828874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828874)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828874)Termination reason: Refutation not found, incomplete strategy
% 3.42/1.50 % (2828874)Time elapsed: 0.002 s
% 3.42/1.50 % (2828874)Peak memory usage: 87 MB
% 3.42/1.50 % (2828874)Instructions burned: 1 (million)
% 3.42/1.50 % (2828878)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=466259907:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 3.42/1.50 % (2828876)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2279322249:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.42/1.50 % (2828877)lrs+10_64_to=lpo:sil=8000:random_seed=3913884017:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 3.42/1.50 % (2828878)Instruction limit reached!
% 3.42/1.50 % (2828878)------------------------------
% 3.42/1.50 % (2828878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828878)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828878)Termination reason: Instruction limit
% 3.42/1.50 % (2828878)Termination phase: Saturation
% 3.42/1.50 % (2828878)Time elapsed: 0.052 s
% 3.42/1.50 % (2828878)Peak memory usage: 88 MB
% 3.42/1.50 % (2828878)Instructions burned: 196 (million)
% 3.42/1.50 % (2828877)First to succeed.
% 3.42/1.50 % (2828877)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2828854"
% 3.42/1.50 % (2828876)Instruction limit reached!
% 3.42/1.50 % (2828876)------------------------------
% 3.42/1.50 % (2828876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828876)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828876)Termination reason: Instruction limit
% 3.42/1.50 % (2828876)Termination phase: Saturation
% 3.42/1.50 % (2828876)Time elapsed: 0.118 s
% 3.42/1.50 % (2828876)Peak memory usage: 88 MB
% 3.42/1.50 % (2828876)Instructions burned: 220 (million)
% 3.42/1.50 % (2828883)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3412070711:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 3.42/1.50 % (2828883)Instruction limit reached!
% 3.42/1.50 % (2828883)------------------------------
% 3.42/1.50 % (2828883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828883)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828883)Termination reason: Instruction limit
% 3.42/1.50 % (2828883)Termination phase: Saturation
% 3.42/1.50 % (2828883)Time elapsed: 0.045 s
% 3.42/1.50 % (2828883)Peak memory usage: 88 MB
% 3.42/1.50 % (2828883)Instructions burned: 161 (million)
% 3.42/1.50 % (2828874)------------------------------
% 3.42/1.50 % (2828874)------------------------------
% 3.42/1.50 % (2828884)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1096618136:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 3.42/1.50 % (2828886)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=180012632:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 3.42/1.50 % (2828886)Refutation not found, incomplete strategy
% 3.42/1.50 % (2828886)------------------------------
% 3.42/1.50 % (2828886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.50 % (2828886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.50 % (2828886)CaDiCaL version: 2.1.3
% 3.42/1.50 % (2828886)Termination reason: Refutation not found, incomplete strategy
% 3.42/1.50 % (2828886)Time elapsed: 0.002 s
% 3.42/1.50 % (2828886)Peak memory usage: 87 MB
% 3.42/1.50 % (2828886)Instructions burned: 8 (million)
% 3.42/1.50 % (2828877)Refutation found. Thanks to Tanya!
% 3.42/1.50 % SZS status Unsatisfiable for theBenchmark
% 3.42/1.50 % SZS output start Proof for theBenchmark
% See solution above
% 3.42/1.59 % (2828877)------------------------------
% 3.42/1.59 % (2828877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.59 % (2828877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.59 % (2828877)CaDiCaL version: 2.1.3
% 3.42/1.59 % (2828877)Termination reason: Refutation
% 3.42/1.59 % (2828877)Time elapsed: 0.041 s
% 3.42/1.59 % (2828877)Peak memory usage: 89 MB
% 3.42/1.59 % (2828877)Instructions burned: 66 (million)
% 3.42/1.59 % (2828877)------------------------------
% 3.42/1.59 % (2828877)------------------------------
% 3.42/1.59 % (2828854)Success in time 0.672 s
% 3.42/1.59 % Vampire exiting
%------------------------------------------------------------------------------