%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-8.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:43 AM UTC 2026
% Result : Unsatisfiable 2.83s 1.28s
% Output : Refutation 3.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 64
% Syntax : Number of formulae : 352 ( 92 unt; 46 def)
% Number of atoms : 841 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 927 ( 438 ~; 443 |; 0 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 51 ( 50 usr; 47 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 75 ( 0 sgn 75 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
fof(f23,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
fof(f24,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
fof(f25,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
fof(f26,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
fof(f27,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
fof(f28,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
fof(f30,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f31,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f34,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f38,axiom,
! [X0,X1] :
( product1(X0,X1,e_4)
| ~ group_element(X1)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| ~ group_element(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
fof(f39,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product1(X0,X1,X3)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function2) ).
fof(f40,axiom,
! [X2,X3,X0,X1] :
( equalish(X1,X3)
| ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( equalish(X0,X3)
| ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
fof(f42,axiom,
! [X0] : product1(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
fof(f44,axiom,
! [X2,X3,X0,X1] :
( equalish(X2,X3)
| ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
fof(f47,axiom,
! [X0] : product2(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
fof(f48,negated_conjecture,
! [X2,X3,X0,X1] :
( product2(X3,X1,X0)
| ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
fof(f63,plain,
! [X0,X1] :
( ~ product1(X0,X1,e_4)
| ~ product1(X0,X1,e_1) ),
inference(resolution,[],[f39,f28]) ).
fof(f66,plain,
! [X0,X1] :
( ~ product1(X0,X1,e_4)
| ~ product1(X0,X1,e_2) ),
inference(resolution,[],[f39,f31]) ).
fof(f69,plain,
! [X0,X1] :
( ~ product1(X0,X1,e_4)
| ~ product1(X0,X1,e_3) ),
inference(resolution,[],[f39,f34]) ).
fof(f73,plain,
! [X0,X1] :
( ~ product1(X0,e_2,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f40,f26]) ).
fof(f74,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f40,f27]) ).
fof(f75,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_1,X1) ),
inference(resolution,[],[f40,f28]) ).
fof(f77,plain,
! [X0,X1] :
( ~ product1(X0,e_3,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f40,f30]) ).
fof(f78,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_2,X1) ),
inference(resolution,[],[f40,f31]) ).
fof(f81,plain,
! [X0,X1] :
( ~ product1(X0,e_4,X1)
| ~ product1(X0,e_3,X1) ),
inference(resolution,[],[f40,f34]) ).
fof(f85,plain,
! [X0,X1] :
( ~ product1(e_2,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f41,f26]) ).
fof(f86,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f41,f27]) ).
fof(f87,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_1,X0,X1) ),
inference(resolution,[],[f41,f28]) ).
fof(f89,plain,
! [X0,X1] :
( ~ product1(e_3,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f41,f30]) ).
fof(f90,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_2,X0,X1) ),
inference(resolution,[],[f41,f31]) ).
fof(f93,plain,
! [X0,X1] :
( ~ product1(e_4,X0,X1)
| ~ product1(e_3,X0,X1) ),
inference(resolution,[],[f41,f34]) ).
fof(f97,plain,
! [X0,X1] :
( ~ product2(X0,X1,e_2)
| ~ product2(X0,X1,e_1) ),
inference(resolution,[],[f44,f26]) ).
fof(f697,plain,
~ product1(e_4,e_4,e_1),
inference(resolution,[],[f63,f42]) ).
fof(f700,plain,
~ product1(e_4,e_4,e_2),
inference(resolution,[],[f66,f42]) ).
fof(f702,plain,
~ product1(e_4,e_4,e_3),
inference(resolution,[],[f69,f42]) ).
fof(f704,plain,
~ product1(e_2,e_1,e_2),
inference(resolution,[],[f73,f42]) ).
fof(f707,definition,
( spl0_81
<=> group_element(e_2) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f708,plain,
( ~ group_element(e_2)
| spl0_81 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f713,plain,
( $false
| spl0_81 ),
inference(resolution,[],[f708,f23]) ).
fof(f714,plain,
spl0_81,
inference(avatar_contradiction_clause,[],[f713]) ).
fof(f720,definition,
( spl0_83
<=> product1(e_4,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f721,plain,
( product1(e_4,e_2,e_1)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f723,definition,
( spl0_84
<=> product1(e_4,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f724,plain,
( product1(e_4,e_2,e_2)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,definition,
( spl0_85
<=> product1(e_4,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f727,plain,
( product1(e_4,e_2,e_3)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f733,definition,
( spl0_87
<=> product1(e_3,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f734,plain,
( product1(e_3,e_2,e_1)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f736,definition,
( spl0_88
<=> product1(e_3,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f737,plain,
( product1(e_3,e_2,e_2)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,definition,
( spl0_89
<=> product1(e_3,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f740,plain,
( product1(e_3,e_2,e_3)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f739]) ).
fof(f746,definition,
( spl0_91
<=> product1(e_1,e_2,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f747,plain,
( product1(e_1,e_2,e_1)
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f749,definition,
( spl0_92
<=> product1(e_1,e_2,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f750,plain,
( product1(e_1,e_2,e_2)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,definition,
( spl0_93
<=> product1(e_1,e_2,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f753,plain,
( product1(e_1,e_2,e_3)
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f760,definition,
( spl0_95
<=> group_element(e_4) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f761,plain,
( ~ group_element(e_4)
| spl0_95 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f772,definition,
( spl0_99
<=> group_element(e_1) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f773,plain,
( ~ group_element(e_1)
| spl0_99 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f776,plain,
! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(e_3)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f74,f38]) ).
fof(f778,definition,
( spl0_100
<=> group_element(e_3) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f779,plain,
( ~ group_element(e_3)
| spl0_100 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f781,definition,
( spl0_101
<=> ! [X0] :
( ~ product1(X0,e_1,e_4)
| ~ group_element(X0)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f782,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_1,e_4)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) )
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f783,plain,
( ~ spl0_100
| spl0_101 ),
inference(avatar_split_clause,[],[f776,f781,f778]) ).
fof(f784,plain,
( $false
| spl0_100 ),
inference(resolution,[],[f779,f24]) ).
fof(f785,plain,
spl0_100,
inference(avatar_contradiction_clause,[],[f784]) ).
fof(f786,plain,
( $false
| spl0_95 ),
inference(resolution,[],[f761,f25]) ).
fof(f787,plain,
spl0_95,
inference(avatar_contradiction_clause,[],[f786]) ).
fof(f789,plain,
( ~ product1(e_2,e_1,e_4)
| product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ spl0_101 ),
inference(resolution,[],[f782,f23]) ).
fof(f793,definition,
( spl0_102
<=> product1(e_2,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f794,plain,
( product1(e_2,e_3,e_1)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f796,definition,
( spl0_103
<=> product1(e_2,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f797,plain,
( product1(e_2,e_3,e_2)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f799,definition,
( spl0_104
<=> product1(e_2,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f800,plain,
( product1(e_2,e_3,e_3)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f802,definition,
( spl0_105
<=> product1(e_2,e_1,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f803,plain,
( ~ product1(e_2,e_1,e_4)
| spl0_105 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f804,plain,
( spl0_102
| spl0_103
| spl0_104
| ~ spl0_105
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f789,f781,f802,f799,f796,f793]) ).
fof(f806,definition,
( spl0_106
<=> product1(e_1,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f807,plain,
( product1(e_1,e_3,e_1)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,definition,
( spl0_107
<=> product1(e_1,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f810,plain,
( product1(e_1,e_3,e_2)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f812,definition,
( spl0_108
<=> product1(e_1,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f813,plain,
( product1(e_1,e_3,e_3)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f815,plain,
( $false
| spl0_99 ),
inference(resolution,[],[f773,f22]) ).
fof(f816,plain,
spl0_99,
inference(avatar_contradiction_clause,[],[f815]) ).
fof(f832,definition,
( spl0_112
<=> product1(e_2,e_1,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f833,plain,
( product1(e_2,e_1,e_3)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f835,definition,
( spl0_113
<=> product1(e_2,e_1,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f836,plain,
( product1(e_2,e_1,e_2)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f838,definition,
( spl0_114
<=> product1(e_2,e_1,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f839,plain,
( product1(e_2,e_1,e_1)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f845,plain,
( $false
| ~ spl0_113 ),
inference(resolution,[],[f704,f836]) ).
fof(f846,plain,
~ spl0_113,
inference(avatar_contradiction_clause,[],[f845]) ).
fof(f861,plain,
~ product1(e_3,e_2,e_3),
inference(resolution,[],[f77,f42]) ).
fof(f862,plain,
! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(e_3)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| ~ group_element(X0) ),
inference(resolution,[],[f77,f38]) ).
fof(f864,definition,
( spl0_116
<=> ! [X0] :
( ~ product1(X0,e_2,e_4)
| ~ group_element(X0)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f865,plain,
( ! [X0] :
( ~ group_element(X0)
| ~ product1(X0,e_2,e_4)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_1) )
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f864]) ).
fof(f866,plain,
( ~ spl0_100
| spl0_116 ),
inference(avatar_split_clause,[],[f862,f864,f778]) ).
fof(f867,plain,
( ~ product1(e_1,e_2,e_4)
| product1(e_1,e_3,e_3)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_1)
| ~ spl0_116 ),
inference(resolution,[],[f865,f22]) ).
fof(f872,definition,
( spl0_117
<=> product1(e_4,e_3,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f873,plain,
( product1(e_4,e_3,e_1)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f875,definition,
( spl0_118
<=> product1(e_4,e_3,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f876,plain,
( product1(e_4,e_3,e_2)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f878,definition,
( spl0_119
<=> product1(e_4,e_3,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f879,plain,
( product1(e_4,e_3,e_3)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f881,definition,
( spl0_120
<=> product1(e_4,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f882,plain,
( ~ product1(e_4,e_2,e_4)
| spl0_120 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f889,definition,
( spl0_122
<=> product1(e_1,e_2,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f890,plain,
( ~ product1(e_1,e_2,e_4)
| spl0_122 ),
inference(avatar_component_clause,[],[f889]) ).
fof(f891,plain,
( spl0_106
| spl0_107
| spl0_108
| ~ spl0_122
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f867,f864,f889,f812,f809,f806]) ).
fof(f897,plain,
( ~ group_element(e_2)
| product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| ~ group_element(e_1)
| spl0_122 ),
inference(resolution,[],[f890,f38]) ).
fof(f898,plain,
( ~ spl0_99
| spl0_93
| spl0_92
| spl0_91
| ~ spl0_81
| spl0_122 ),
inference(avatar_split_clause,[],[f897,f889,f707,f746,f749,f752,f772]) ).
fof(f899,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_91 ),
inference(resolution,[],[f747,f73]) ).
fof(f900,plain,
( $false
| ~ spl0_91 ),
inference(resolution,[],[f899,f42]) ).
fof(f901,plain,
~ spl0_91,
inference(avatar_contradiction_clause,[],[f900]) ).
fof(f904,plain,
~ product1(e_4,e_2,e_4),
inference(resolution,[],[f78,f42]) ).
fof(f932,plain,
~ product1(e_4,e_3,e_4),
inference(resolution,[],[f81,f42]) ).
fof(f944,definition,
( spl0_129
<=> product1(e_4,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f945,plain,
( product1(e_4,e_4,e_1)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f947,definition,
( spl0_130
<=> product1(e_4,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f948,plain,
( product1(e_4,e_4,e_2)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f947]) ).
fof(f950,definition,
( spl0_131
<=> product1(e_4,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f951,plain,
( product1(e_4,e_4,e_3)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f953,definition,
( spl0_132
<=> product1(e_4,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f954,plain,
( ~ product1(e_4,e_3,e_4)
| spl0_132 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f957,definition,
( spl0_133
<=> product1(e_2,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f958,plain,
( product1(e_2,e_4,e_1)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f960,definition,
( spl0_134
<=> product1(e_2,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f961,plain,
( product1(e_2,e_4,e_2)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,definition,
( spl0_135
<=> product1(e_2,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f964,plain,
( product1(e_2,e_4,e_3)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f963]) ).
fof(f970,definition,
( spl0_137
<=> product1(e_1,e_4,e_1) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f971,plain,
( product1(e_1,e_4,e_1)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f970]) ).
fof(f973,definition,
( spl0_138
<=> product1(e_1,e_4,e_2) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f974,plain,
( product1(e_1,e_4,e_2)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f973]) ).
fof(f976,definition,
( spl0_139
<=> product1(e_1,e_4,e_3) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f977,plain,
( product1(e_1,e_4,e_3)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f979,definition,
( spl0_140
<=> product1(e_1,e_3,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f980,plain,
( ~ product1(e_1,e_3,e_4)
| spl0_140 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f984,plain,
( $false
| ~ spl0_131 ),
inference(resolution,[],[f951,f702]) ).
fof(f990,plain,
~ spl0_131,
inference(avatar_contradiction_clause,[],[f984]) ).
fof(f991,plain,
( ~ product1(e_4,e_2,e_1)
| ~ spl0_117 ),
inference(resolution,[],[f873,f77]) ).
fof(f998,plain,
( ~ product1(e_2,e_1,e_3)
| ~ spl0_135 ),
inference(resolution,[],[f964,f75]) ).
fof(f1003,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_138 ),
inference(resolution,[],[f974,f81]) ).
fof(f1007,plain,
( $false
| ~ spl0_83
| ~ spl0_117 ),
inference(resolution,[],[f991,f721]) ).
fof(f1008,plain,
( ~ spl0_83
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1009,plain,
~ spl0_132,
inference(avatar_split_clause,[],[f932,f953]) ).
fof(f1013,plain,
( $false
| ~ spl0_130 ),
inference(resolution,[],[f948,f700]) ).
fof(f1018,plain,
~ spl0_130,
inference(avatar_contradiction_clause,[],[f1013]) ).
fof(f1019,plain,
( ~ group_element(e_3)
| product1(e_4,e_3,e_1)
| product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_3)
| ~ group_element(e_4)
| spl0_132 ),
inference(resolution,[],[f954,f38]) ).
fof(f1020,plain,
( $false
| ~ spl0_112
| ~ spl0_135 ),
inference(resolution,[],[f998,f833]) ).
fof(f1021,plain,
( ~ spl0_112
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1022,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_133 ),
inference(resolution,[],[f958,f81]) ).
fof(f1024,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_133 ),
inference(resolution,[],[f958,f75]) ).
fof(f1029,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_137 ),
inference(resolution,[],[f971,f75]) ).
fof(f1032,plain,
( ~ spl0_95
| spl0_119
| spl0_118
| spl0_117
| ~ spl0_100
| spl0_132 ),
inference(avatar_split_clause,[],[f1019,f953,f778,f872,f875,f878,f760]) ).
fof(f1037,plain,
( $false
| ~ spl0_137 ),
inference(resolution,[],[f1029,f42]) ).
fof(f1038,plain,
~ spl0_137,
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1040,plain,
( ~ product1(e_1,e_2,e_3)
| ~ spl0_139 ),
inference(resolution,[],[f977,f78]) ).
fof(f1046,plain,
~ product1(e_1,e_2,e_2),
inference(resolution,[],[f85,f42]) ).
fof(f1047,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_2,X0,e_1)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| ~ group_element(e_2) ),
inference(resolution,[],[f85,f38]) ).
fof(f1049,definition,
( spl0_141
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1050,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1051,plain,
( ~ spl0_81
| spl0_141 ),
inference(avatar_split_clause,[],[f1047,f1049,f707]) ).
fof(f1054,plain,
( product1(e_2,e_3,e_3)
| product1(e_2,e_3,e_2)
| product1(e_2,e_3,e_1)
| ~ product1(e_1,e_3,e_4)
| ~ spl0_141 ),
inference(resolution,[],[f1050,f24]) ).
fof(f1056,plain,
( ~ spl0_140
| spl0_102
| spl0_103
| spl0_104
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1054,f1049,f799,f796,f793,f979]) ).
fof(f1057,plain,
( $false
| ~ spl0_102
| ~ spl0_133 ),
inference(resolution,[],[f794,f1022]) ).
fof(f1060,plain,
( ~ product1(e_2,e_1,e_1)
| ~ spl0_102 ),
inference(resolution,[],[f794,f74]) ).
fof(f1061,plain,
( ~ spl0_102
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1063,definition,
( spl0_142
<=> product1(e_1,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1064,plain,
( ~ product1(e_1,e_4,e_4)
| spl0_142 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1068,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_134 ),
inference(resolution,[],[f961,f78]) ).
fof(f1071,plain,
( $false
| ~ spl0_134 ),
inference(resolution,[],[f1068,f42]) ).
fof(f1072,plain,
~ spl0_134,
inference(avatar_contradiction_clause,[],[f1071]) ).
fof(f1077,plain,
~ product1(e_1,e_3,e_3),
inference(resolution,[],[f86,f42]) ).
fof(f1078,plain,
! [X0] :
( ~ product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| ~ group_element(e_3) ),
inference(resolution,[],[f86,f38]) ).
fof(f1080,definition,
( spl0_143
<=> ! [X0] :
( ~ product1(e_1,X0,e_4)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1081,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_1)
| ~ product1(e_1,X0,e_4) )
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f1080]) ).
fof(f1082,plain,
( ~ spl0_100
| spl0_143 ),
inference(avatar_split_clause,[],[f1078,f1080,f778]) ).
fof(f1084,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ product1(e_1,e_2,e_4)
| ~ spl0_143 ),
inference(resolution,[],[f1081,f23]) ).
fof(f1091,plain,
( $false
| ~ spl0_92 ),
inference(resolution,[],[f1046,f750]) ).
fof(f1092,plain,
~ spl0_92,
inference(avatar_contradiction_clause,[],[f1091]) ).
fof(f1093,plain,
( $false
| ~ spl0_93
| ~ spl0_139 ),
inference(resolution,[],[f753,f1040]) ).
fof(f1097,plain,
( ~ spl0_93
| ~ spl0_139 ),
inference(avatar_contradiction_clause,[],[f1093]) ).
fof(f1106,plain,
~ product1(e_1,e_4,e_4),
inference(resolution,[],[f87,f42]) ).
fof(f1118,plain,
~ spl0_142,
inference(avatar_split_clause,[],[f1106,f1063]) ).
fof(f1122,plain,
( ~ product1(e_1,e_1,e_1)
| ~ spl0_106 ),
inference(resolution,[],[f807,f74]) ).
fof(f1132,plain,
( ~ group_element(e_3)
| product1(e_1,e_3,e_1)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_3)
| ~ group_element(e_1)
| spl0_140 ),
inference(resolution,[],[f980,f38]) ).
fof(f1133,plain,
( ~ group_element(e_4)
| product1(e_1,e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_3)
| ~ group_element(e_1)
| spl0_142 ),
inference(resolution,[],[f1064,f38]) ).
fof(f1134,plain,
( $false
| ~ spl0_106 ),
inference(resolution,[],[f1122,f42]) ).
fof(f1135,plain,
~ spl0_106,
inference(avatar_contradiction_clause,[],[f1134]) ).
fof(f1136,plain,
( ~ spl0_99
| spl0_108
| spl0_107
| spl0_106
| ~ spl0_100
| spl0_140 ),
inference(avatar_split_clause,[],[f1132,f979,f778,f806,f809,f812,f772]) ).
fof(f1142,plain,
~ product1(e_2,e_3,e_3),
inference(resolution,[],[f89,f42]) ).
fof(f1156,plain,
! [X0] :
( ~ product1(e_2,X0,e_4)
| ~ group_element(X0)
| product1(e_4,X0,e_1)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_3)
| ~ group_element(e_4) ),
inference(resolution,[],[f90,f38]) ).
fof(f1158,definition,
( spl0_146
<=> ! [X0] :
( ~ product1(e_2,X0,e_4)
| product1(e_4,X0,e_3)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_1)
| ~ group_element(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1159,plain,
( ! [X0] :
( ~ group_element(X0)
| product1(e_4,X0,e_3)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_1)
| ~ product1(e_2,X0,e_4) )
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1160,plain,
( ~ spl0_95
| spl0_146 ),
inference(avatar_split_clause,[],[f1156,f1158,f760]) ).
fof(f1164,plain,
( product1(e_4,e_4,e_3)
| product1(e_4,e_4,e_2)
| product1(e_4,e_4,e_1)
| ~ product1(e_2,e_4,e_4)
| ~ spl0_146 ),
inference(resolution,[],[f1159,f25]) ).
fof(f1166,definition,
( spl0_147
<=> product1(e_2,e_4,e_4) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1167,plain,
( ~ product1(e_2,e_4,e_4)
| spl0_147 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1168,plain,
( ~ spl0_147
| spl0_129
| spl0_130
| spl0_131
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f1164,f1158,f950,f947,f944,f1166]) ).
fof(f1169,plain,
( ~ group_element(e_4)
| product1(e_2,e_4,e_1)
| product1(e_2,e_4,e_2)
| product1(e_2,e_4,e_3)
| ~ group_element(e_2)
| spl0_147 ),
inference(resolution,[],[f1167,f38]) ).
fof(f1172,plain,
( ~ product1(e_3,e_3,e_3)
| ~ spl0_119 ),
inference(resolution,[],[f93,f879]) ).
fof(f1192,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_84 ),
inference(resolution,[],[f724,f90]) ).
fof(f1197,plain,
( $false
| ~ spl0_119 ),
inference(resolution,[],[f1172,f42]) ).
fof(f1198,plain,
~ spl0_119,
inference(avatar_contradiction_clause,[],[f1197]) ).
fof(f1205,plain,
( ~ product1(e_2,e_3,e_1)
| ~ spl0_117 ),
inference(resolution,[],[f873,f90]) ).
fof(f1209,plain,
( $false
| ~ spl0_84 ),
inference(resolution,[],[f1192,f42]) ).
fof(f1210,plain,
~ spl0_84,
inference(avatar_contradiction_clause,[],[f1209]) ).
fof(f1211,plain,
( ~ spl0_99
| spl0_139
| spl0_138
| spl0_137
| ~ spl0_95
| spl0_142 ),
inference(avatar_split_clause,[],[f1133,f1063,f760,f970,f973,f976,f772]) ).
fof(f1215,plain,
~ spl0_120,
inference(avatar_split_clause,[],[f904,f881]) ).
fof(f1219,plain,
( ~ product1(e_1,e_2,e_3)
| ~ spl0_85 ),
inference(resolution,[],[f727,f87]) ).
fof(f1228,plain,
( ~ group_element(e_2)
| product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_3)
| ~ group_element(e_4)
| spl0_120 ),
inference(resolution,[],[f882,f38]) ).
fof(f1231,plain,
( $false
| ~ spl0_129 ),
inference(resolution,[],[f945,f697]) ).
fof(f1238,plain,
~ spl0_129,
inference(avatar_contradiction_clause,[],[f1231]) ).
fof(f1254,plain,
( $false
| ~ spl0_107
| ~ spl0_138 ),
inference(resolution,[],[f1003,f810]) ).
fof(f1255,plain,
( ~ spl0_107
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f1254]) ).
fof(f1263,plain,
( ~ spl0_81
| spl0_135
| spl0_134
| spl0_133
| ~ spl0_95
| spl0_147 ),
inference(avatar_split_clause,[],[f1169,f1166,f760,f957,f960,f963,f707]) ).
fof(f1268,plain,
( ~ product1(e_1,e_4,e_3)
| ~ spl0_135 ),
inference(resolution,[],[f964,f85]) ).
fof(f1275,plain,
( $false
| ~ spl0_102
| ~ spl0_117 ),
inference(resolution,[],[f1205,f794]) ).
fof(f1276,plain,
( ~ spl0_102
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f1275]) ).
fof(f1279,plain,
( ~ product1(e_2,e_3,e_2)
| ~ spl0_118 ),
inference(resolution,[],[f876,f90]) ).
fof(f1280,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_118 ),
inference(resolution,[],[f876,f87]) ).
fof(f1291,plain,
( ~ spl0_122
| spl0_87
| spl0_88
| spl0_89
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f1084,f1080,f739,f736,f733,f889]) ).
fof(f1293,plain,
( ~ spl0_95
| spl0_85
| spl0_84
| spl0_83
| ~ spl0_81
| spl0_120 ),
inference(avatar_split_clause,[],[f1228,f881,f707,f720,f723,f726,f760]) ).
fof(f1298,plain,
( ~ product1(e_2,e_2,e_2)
| ~ spl0_88 ),
inference(resolution,[],[f737,f89]) ).
fof(f1302,plain,
( $false
| ~ spl0_135
| ~ spl0_139 ),
inference(resolution,[],[f1268,f977]) ).
fof(f1303,plain,
( ~ spl0_135
| ~ spl0_139 ),
inference(avatar_contradiction_clause,[],[f1302]) ).
fof(f1306,plain,
( ~ product1(e_1,e_3,e_2)
| ~ spl0_103 ),
inference(resolution,[],[f797,f85]) ).
fof(f1329,plain,
( $false
| ~ spl0_103
| ~ spl0_118 ),
inference(resolution,[],[f1279,f797]) ).
fof(f1330,plain,
( ~ spl0_103
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f1329]) ).
fof(f1336,plain,
( $false
| ~ spl0_107
| ~ spl0_118 ),
inference(resolution,[],[f1280,f810]) ).
fof(f1337,plain,
( ~ spl0_107
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f1336]) ).
fof(f1338,plain,
( $false
| ~ spl0_108 ),
inference(resolution,[],[f813,f1077]) ).
fof(f1343,plain,
~ spl0_108,
inference(avatar_contradiction_clause,[],[f1338]) ).
fof(f1362,plain,
( $false
| ~ spl0_104 ),
inference(resolution,[],[f1142,f800]) ).
fof(f1363,plain,
~ spl0_104,
inference(avatar_contradiction_clause,[],[f1362]) ).
fof(f1368,plain,
( $false
| ~ spl0_88 ),
inference(resolution,[],[f1298,f42]) ).
fof(f1369,plain,
~ spl0_88,
inference(avatar_contradiction_clause,[],[f1368]) ).
fof(f1370,plain,
( $false
| ~ spl0_89 ),
inference(resolution,[],[f740,f861]) ).
fof(f1376,plain,
~ spl0_89,
inference(avatar_contradiction_clause,[],[f1370]) ).
fof(f1385,plain,
! [X2,X0,X1] :
( ~ product2(X0,X1,e_1)
| ~ product1(X2,e_2,X0)
| ~ product1(e_2,X1,X2) ),
inference(resolution,[],[f97,f48]) ).
fof(f1387,plain,
( $false
| ~ spl0_85
| ~ spl0_93 ),
inference(resolution,[],[f1219,f753]) ).
fof(f1388,plain,
( ~ spl0_85
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f1387]) ).
fof(f1415,plain,
! [X0] :
( ~ product1(X0,e_2,e_1)
| ~ product1(e_2,e_1,X0) ),
inference(resolution,[],[f1385,f47]) ).
fof(f1448,plain,
( ~ product1(e_2,e_1,e_3)
| ~ spl0_87 ),
inference(resolution,[],[f1415,f734]) ).
fof(f1461,plain,
( $false
| ~ spl0_114
| ~ spl0_133 ),
inference(resolution,[],[f1024,f839]) ).
fof(f1462,plain,
( ~ spl0_114
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f1461]) ).
fof(f1463,plain,
( $false
| ~ spl0_87
| ~ spl0_112 ),
inference(resolution,[],[f833,f1448]) ).
fof(f1467,plain,
( ~ spl0_87
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f1463]) ).
fof(f1475,plain,
( $false
| ~ spl0_103
| ~ spl0_107 ),
inference(resolution,[],[f1306,f810]) ).
fof(f1476,plain,
( ~ spl0_103
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f1475]) ).
fof(f1480,plain,
( ~ product1(e_2,e_1,e_4)
| ~ spl0_83 ),
inference(resolution,[],[f721,f1415]) ).
fof(f1482,plain,
( ~ spl0_105
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1480,f720,f802]) ).
fof(f1491,plain,
( ~ group_element(e_1)
| product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| ~ group_element(e_2)
| spl0_105 ),
inference(resolution,[],[f803,f38]) ).
fof(f1492,plain,
( ~ spl0_81
| spl0_112
| spl0_113
| spl0_114
| ~ spl0_99
| spl0_105 ),
inference(avatar_split_clause,[],[f1491,f802,f772,f838,f835,f832,f707]) ).
fof(f1527,plain,
( $false
| ~ spl0_102
| ~ spl0_114 ),
inference(resolution,[],[f1060,f839]) ).
fof(f1528,plain,
( ~ spl0_102
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f1527]) ).
cnf(s110,plain,
spl0_81,
inference(sat_conversion,[],[f714]) ).
cnf(s115,plain,
( ~ spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f783]) ).
cnf(s116,plain,
spl0_100,
inference(sat_conversion,[],[f785]) ).
cnf(s117,plain,
spl0_95,
inference(sat_conversion,[],[f787]) ).
cnf(s118,plain,
( ~ spl0_101
| spl0_102
| spl0_103
| spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f804]) ).
cnf(s120,plain,
spl0_99,
inference(sat_conversion,[],[f816]) ).
cnf(s123,plain,
~ spl0_113,
inference(sat_conversion,[],[f846]) ).
cnf(s126,plain,
( ~ spl0_100
| spl0_116 ),
inference(sat_conversion,[],[f866]) ).
cnf(s129,plain,
( spl0_106
| spl0_107
| spl0_108
| ~ spl0_116
| ~ spl0_122 ),
inference(sat_conversion,[],[f891]) ).
cnf(s131,plain,
( ~ spl0_81
| spl0_91
| spl0_92
| spl0_93
| ~ spl0_99
| spl0_122 ),
inference(sat_conversion,[],[f898]) ).
cnf(s132,plain,
~ spl0_91,
inference(sat_conversion,[],[f901]) ).
cnf(s141,plain,
~ spl0_131,
inference(sat_conversion,[],[f990]) ).
cnf(s144,plain,
( ~ spl0_83
| ~ spl0_117 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s145,plain,
~ spl0_132,
inference(sat_conversion,[],[f1009]) ).
cnf(s146,plain,
~ spl0_130,
inference(sat_conversion,[],[f1018]) ).
cnf(s147,plain,
( ~ spl0_112
| ~ spl0_135 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s150,plain,
( ~ spl0_95
| ~ spl0_100
| spl0_117
| spl0_118
| spl0_119
| spl0_132 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s151,plain,
~ spl0_137,
inference(sat_conversion,[],[f1038]) ).
cnf(s152,plain,
( ~ spl0_81
| spl0_141 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s153,plain,
( spl0_102
| spl0_103
| spl0_104
| ~ spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s154,plain,
( ~ spl0_102
| ~ spl0_133 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s156,plain,
~ spl0_134,
inference(sat_conversion,[],[f1072]) ).
cnf(s157,plain,
( ~ spl0_100
| spl0_143 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s159,plain,
~ spl0_92,
inference(sat_conversion,[],[f1092]) ).
cnf(s160,plain,
( ~ spl0_93
| ~ spl0_139 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s164,plain,
~ spl0_142,
inference(sat_conversion,[],[f1118]) ).
cnf(s167,plain,
~ spl0_106,
inference(sat_conversion,[],[f1135]) ).
cnf(s168,plain,
( ~ spl0_99
| ~ spl0_100
| spl0_106
| spl0_107
| spl0_108
| spl0_140 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s170,plain,
( ~ spl0_95
| spl0_146 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s171,plain,
( spl0_129
| spl0_130
| spl0_131
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s177,plain,
~ spl0_119,
inference(sat_conversion,[],[f1198]) ).
cnf(s180,plain,
~ spl0_84,
inference(sat_conversion,[],[f1210]) ).
cnf(s181,plain,
( ~ spl0_95
| ~ spl0_99
| spl0_137
| spl0_138
| spl0_139
| spl0_142 ),
inference(sat_conversion,[],[f1211]) ).
cnf(s185,plain,
~ spl0_120,
inference(sat_conversion,[],[f1215]) ).
cnf(s188,plain,
~ spl0_129,
inference(sat_conversion,[],[f1238]) ).
cnf(s189,plain,
( ~ spl0_107
| ~ spl0_138 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s191,plain,
( ~ spl0_81
| ~ spl0_95
| spl0_133
| spl0_134
| spl0_135
| spl0_147 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s193,plain,
( ~ spl0_102
| ~ spl0_117 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s196,plain,
( spl0_87
| spl0_88
| spl0_89
| ~ spl0_122
| ~ spl0_143 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s198,plain,
( ~ spl0_81
| spl0_83
| spl0_84
| spl0_85
| ~ spl0_95
| spl0_120 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s199,plain,
( ~ spl0_135
| ~ spl0_139 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s203,plain,
( ~ spl0_103
| ~ spl0_118 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s204,plain,
( ~ spl0_107
| ~ spl0_118 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s205,plain,
~ spl0_108,
inference(sat_conversion,[],[f1343]) ).
cnf(s206,plain,
~ spl0_104,
inference(sat_conversion,[],[f1363]) ).
cnf(s207,plain,
~ spl0_88,
inference(sat_conversion,[],[f1369]) ).
cnf(s208,plain,
~ spl0_89,
inference(sat_conversion,[],[f1376]) ).
cnf(s209,plain,
( ~ spl0_85
| ~ spl0_93 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s217,plain,
( ~ spl0_114
| ~ spl0_133 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s218,plain,
( ~ spl0_87
| ~ spl0_112 ),
inference(sat_conversion,[],[f1467]) ).
cnf(s219,plain,
( ~ spl0_103
| ~ spl0_107 ),
inference(sat_conversion,[],[f1476]) ).
cnf(s220,plain,
( ~ spl0_83
| ~ spl0_105 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s221,plain,
( ~ spl0_81
| ~ spl0_99
| spl0_105
| spl0_112
| spl0_113
| spl0_114 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s223,plain,
( ~ spl0_102
| ~ spl0_114 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s226,plain,
( spl0_87
| ~ spl0_122
| ~ spl0_143 ),
inference(rat,[],[s196,s208,s207]) ).
cnf(s231,plain,
( spl0_130
| spl0_131
| ~ spl0_146
| ~ spl0_147 ),
inference(rat,[],[s171,s188]) ).
cnf(s232,plain,
( ~ spl0_99
| ~ spl0_100
| spl0_106
| spl0_107
| spl0_140 ),
inference(rat,[],[s168,s205]) ).
cnf(s235,plain,
( spl0_102
| spl0_103
| ~ spl0_140
| ~ spl0_141 ),
inference(rat,[],[s153,s206]) ).
cnf(s236,plain,
( ~ spl0_95
| ~ spl0_100
| spl0_117
| spl0_118
| spl0_132 ),
inference(rat,[],[s150,s177]) ).
cnf(s243,plain,
( ~ spl0_81
| spl0_93
| ~ spl0_99
| spl0_122 ),
inference(rat,[],[s131,s159,s132]) ).
cnf(s245,plain,
( spl0_107
| ~ spl0_116
| ~ spl0_122 ),
inference(rat,[],[s129,s205,s167]) ).
cnf(s250,plain,
( ~ spl0_101
| spl0_102
| spl0_103
| ~ spl0_105 ),
inference(rat,[],[s118,s206]) ).
cnf(s252,plain,
spl0_146,
inference(rat,[],[s170,s117]) ).
cnf(s258,plain,
~ spl0_147,
inference(rat,[],[s231,s141,s146,s252]) ).
cnf(s260,plain,
spl0_143,
inference(rat,[],[s157,s116]) ).
cnf(s261,plain,
spl0_116,
inference(rat,[],[s126,s116]) ).
cnf(s262,plain,
spl0_101,
inference(rat,[],[s115,s116]) ).
cnf(s266,plain,
spl0_141,
inference(rat,[],[s152,s110]) ).
cnf(s288,plain,
~ spl0_122,
inference(rat,[],[s217,s221,s191,s250,s199,s193,s181,s236,s189,s204,s219,s218,s245,s226,s120,s110,s123,s117,s156,s258,s262,s151,s164,s116,s145,s261,s260]) ).
cnf(s289,plain,
spl0_93,
inference(rat,[],[s243,s110,s120,s288]) ).
cnf(s290,plain,
~ spl0_85,
inference(rat,[],[s209,s289]) ).
cnf(s291,plain,
~ spl0_139,
inference(rat,[],[s160,s289]) ).
cnf(s292,plain,
spl0_83,
inference(rat,[],[s198,s185,s117,s110,s180,s290]) ).
cnf(s293,plain,
spl0_138,
inference(rat,[],[s181,s164,s117,s120,s151,s291]) ).
cnf(s295,plain,
~ spl0_105,
inference(rat,[],[s220,s292]) ).
cnf(s297,plain,
~ spl0_117,
inference(rat,[],[s144,s292]) ).
cnf(s298,plain,
~ spl0_107,
inference(rat,[],[s189,s293]) ).
cnf(s302,plain,
spl0_118,
inference(rat,[],[s236,s145,s116,s117,s297]) ).
cnf(s303,plain,
spl0_140,
inference(rat,[],[s232,s116,s120,s167,s298]) ).
cnf(s306,plain,
~ spl0_103,
inference(rat,[],[s203,s302]) ).
cnf(s308,plain,
spl0_102,
inference(rat,[],[s235,s266,s306,s303]) ).
cnf(s310,plain,
~ spl0_114,
inference(rat,[],[s223,s308]) ).
cnf(s311,plain,
~ spl0_133,
inference(rat,[],[s154,s308]) ).
cnf(s312,plain,
spl0_112,
inference(rat,[],[s221,s295,s123,s110,s120,s310]) ).
cnf(s313,plain,
spl0_135,
inference(rat,[],[s191,s258,s110,s156,s117,s311]) ).
cnf(s314,plain,
$false,
inference(rat,[],[s147,s313,s312]) ).
fof(f1529,plain,
$false,
inference(avatar_sat_refutation,[],[s314]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-8.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 09:26:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 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.83/1.28 % (2358987)Input is clausal, will run a generic CNF schedule.
% 2.83/1.28 % (2358996)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=648357233:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.83/1.28 % (2358996)Instruction limit reached!
% 2.83/1.28 % (2358996)------------------------------
% 2.83/1.28 % (2358996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.28 % (2358996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.28 % (2358996)CaDiCaL version: 2.1.3
% 2.83/1.28 % (2358996)Termination reason: Instruction limit
% 2.83/1.28 % (2358996)Termination phase: Saturation
% 2.83/1.28 % (2358996)Time elapsed: 0.035 s
% 2.83/1.28 % (2358996)Peak memory usage: 88 MB
% 2.83/1.28 % (2358996)Instructions burned: 115 (million)
% 2.83/1.28 % (2358992)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=3065773035:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.83/1.28 % (2358995)lrs+10_1_sil=8000:sp=occurrence:random_seed=949890908:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.83/1.28 % (2358993)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2750814477:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.83/1.28 % (2358994)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1346714804:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.83/1.28 % (2358997)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3066610353:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.83/1.28 % (2358998)dis-21_1_sil=8000:lcm=predicate:random_seed=2489665890: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)
% 2.83/1.28 % (2358998)First to succeed.
% 2.83/1.28 % (2358998)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2358987"
% 2.83/1.28 % (2358997)Also succeeded, but the first one will report.
% 2.83/1.28 % (2358995)Instruction limit reached!
% 2.83/1.28 % (2358995)------------------------------
% 2.83/1.28 % (2358995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.28 % (2358995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.28 % (2358995)CaDiCaL version: 2.1.3
% 2.83/1.28 % (2358995)Termination reason: Instruction limit
% 2.83/1.28 % (2358995)Termination phase: Saturation
% 2.83/1.28 % (2358995)Time elapsed: 0.061 s
% 2.83/1.28 % (2358995)Peak memory usage: 88 MB
% 2.83/1.28 % (2358995)Instructions burned: 108 (million)
% 2.83/1.28 % (2359004)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=1156157920:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.83/1.28 % (2359004)Also succeeded, but the first one will report.
% 2.83/1.28 % (2359007)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2975531845: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)
% 2.83/1.28 % (2359007)Refutation not found, incomplete strategy
% 2.83/1.28 % (2359007)------------------------------
% 2.83/1.28 % (2359007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.28 % (2359007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.28 % (2359007)CaDiCaL version: 2.1.3
% 2.83/1.28 % (2359007)Termination reason: Refutation not found, incomplete strategy
% 2.83/1.28 % (2359007)Time elapsed: 0.002 s
% 2.83/1.28 % (2359007)Peak memory usage: 87 MB
% 2.83/1.28 % (2359007)Instructions burned: 2 (million)
% 2.83/1.28 % (2358998)Refutation found. Thanks to Tanya!
% 2.83/1.28 % SZS status Unsatisfiable for theBenchmark
% 2.83/1.28 % SZS output start Proof for theBenchmark
% See solution above
% 3.71/1.47 % (2358998)------------------------------
% 3.71/1.47 % (2358998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.47 % (2358998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.47 % (2358998)CaDiCaL version: 2.1.3
% 3.71/1.47 % (2358998)Termination reason: Refutation
% 3.71/1.47 % (2358998)Time elapsed: 0.025 s
% 3.71/1.47 % (2358998)Peak memory usage: 89 MB
% 3.71/1.47 % (2358998)Instructions burned: 39 (million)
% 3.71/1.47 % (2358998)------------------------------
% 3.71/1.47 % (2358998)------------------------------
% 3.71/1.47 % (2358987)Success in time 0.442 s
% 3.71/1.47 % Vampire exiting
%------------------------------------------------------------------------------