%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP759+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 : Thu Sep 24 12:35:17 PM UTC 2026
% Result : Unsatisfiable 15.65s 12.65s
% Output : CNFRefutation 15.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 115
% Syntax : Number of formulae : 1024 ( 51 unt; 104 def)
% Number of atoms : 4180 (1800 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 4824 (1668 ~;3052 |; 0 &)
% ( 104 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 106 ( 104 usr; 105 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 323 ( 323 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] : mult(A,i(A)) = e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] : mult(A,e) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [B,A,C] : mult(A,mult(B,C)) = mult(mult(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
mult(op_a,op_b) != mult(op_b,op_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] :
( X = c4
| X = c3
| X = c2
| X = c1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
c1 != c2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
c1 != c3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
c1 != c4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
c2 != c3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
c2 != c4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
c3 != c4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,plain,
! [X0] : mult(X0,i(X0)) = e,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0] : mult(X0,e) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f14,plain,
! [X0,X1,X2] : mult(X0,mult(X1,X2)) = mult(mult(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f15,plain,
mult(op_a,op_b) != mult(op_b,op_a),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
! [X0] :
( X0 = c4
| X0 = c3
| X0 = c2
| X0 = c1 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f17,plain,
c1 != c2,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f18,plain,
c1 != c3,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f19,plain,
c1 != c4,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
c2 != c3,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
c2 != c4,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f22,plain,
c3 != c4,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f23,plain,
( c1 = c4
| c1 = c3
| c1 = c1 ),
inference(resolution,[status(thm)],[f16,f17]) ).
fof(f25,plain,
( c3 = c4
| c3 = c3
| c3 = c1 ),
inference(resolution,[status(thm)],[f16,f20]) ).
fof(f30,plain,
( c2 = c3
| c2 = c2
| c2 = c1 ),
inference(resolution,[status(thm)],[f16,f21]) ).
fof(f32,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f37,plain,
! [X0] :
( X0 = c4
| c2 != c4
| X0 = c3
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f16]) ).
fof(f39,definition,
( sQ0_spl
<=> c1 = c1 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f42,definition,
( sQ1_spl
<=> c1 = c3 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f43,plain,
( ~ sQ1_spl
| c1 = c3 ),
inference(component_clause,[status(thm)],[f42]) ).
fof(f45,definition,
( sQ2_spl
<=> c1 = c4 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f46,plain,
( ~ sQ2_spl
| c1 = c4 ),
inference(component_clause,[status(thm)],[f45]) ).
fof(f48,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f23,f39,f42,f45]) ).
fof(f49,definition,
( sQ3_spl
<=> c4 = c3 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f50,plain,
( ~ sQ3_spl
| c4 = c3 ),
inference(component_clause,[status(thm)],[f49]) ).
fof(f52,definition,
( sQ4_spl
<=> c4 = c4 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f56,definition,
( sQ5_spl
<=> c3 = c3 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f59,plain,
( sQ3_spl
| sQ5_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f25,f42,f56,f49]) ).
fof(f60,definition,
( sQ6_spl
<=> c2 = c1 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f61,plain,
( ~ sQ6_spl
| c2 = c1 ),
inference(component_clause,[status(thm)],[f60]) ).
fof(f63,definition,
( sQ7_spl
<=> c2 = c2 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f66,definition,
( sQ8_spl
<=> c2 = c4 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f72,definition,
( sQ9_spl
<=> c3 = c2 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f73,plain,
( ~ sQ9_spl
| c3 = c2 ),
inference(component_clause,[status(thm)],[f72]) ).
fof(f76,plain,
( sQ9_spl
| sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f30,f60,f63,f72]) ).
fof(f78,definition,
! [X0] :
( sQ10_spl
<=> ( X0 = c1
| X0 = c4
| X0 = c3 ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f79,plain,
! [X0] :
( ~ sQ10_spl
| X0 = c1
| X0 = c4
| X0 = c3 ),
inference(component_clause,[status(thm)],[f78]) ).
fof(f84,plain,
( ~ sQ8_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f37,f78,f66]) ).
fof(f86,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43,f18]) ).
fof(f87,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f86]) ).
fof(f88,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46,f19]) ).
fof(f89,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f88]) ).
fof(f90,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50,f22]) ).
fof(f91,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f90]) ).
fof(f93,plain,
( ~ sQ10_spl
| c2 = c1
| c2 = c3 ),
inference(resolution,[status(thm)],[f79,f21]) ).
fof(f102,plain,
( ~ sQ10_spl
| sQ6_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f93,f72,f60,f78]) ).
fof(f106,definition,
! [X0] :
( sQ11_spl
<=> ( X0 = c3
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f107,plain,
! [X0] :
( ~ sQ11_spl
| X0 = c3
| X0 = c1 ),
inference(component_clause,[status(thm)],[f106]) ).
fof(f111,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73,f20]) ).
fof(f112,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f111]) ).
fof(f113,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f61,f17]) ).
fof(f114,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f113]) ).
fof(f116,plain,
! [X0,X1] : mult(X0,mult(X1,i(mult(X0,X1)))) = e,
inference(paramodulation,[status(thm)],[f12,f14]) ).
fof(f118,plain,
! [X0,X1] : mult(X0,mult(e,X1)) = mult(X0,X1),
inference(paramodulation,[status(thm)],[f13,f14]) ).
fof(f119,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(e,X1),
inference(paramodulation,[status(thm)],[f12,f14]) ).
fof(f133,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f159,plain,
! [X0] : mult(X0,e) = mult(X0,i(e)),
inference(paramodulation,[status(thm)],[f12,f118]) ).
fof(f166,plain,
! [X0] : X0 = mult(X0,i(e)),
inference(forward_demodulation,[status(thm)],[f13,f159]) ).
fof(f173,plain,
! [X0] :
( i(e) = c4
| i(e) = c3
| i(e) = c1
| X0 = mult(X0,c2) ),
inference(paramodulation,[status(thm)],[f16,f166]) ).
fof(f181,definition,
! [X0] :
( sQ12_spl
<=> X0 = mult(X0,c2) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f182,plain,
! [X0] :
( ~ sQ12_spl
| X0 = mult(X0,c2) ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,definition,
( sQ13_spl
<=> i(e) = c1 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( ~ sQ13_spl
| i(e) = c1 ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,definition,
( sQ14_spl
<=> i(e) = c3 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f188,plain,
( ~ sQ14_spl
| i(e) = c3 ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f189,plain,
( sQ14_spl
| i(e) != c3 ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f190,definition,
( sQ15_spl
<=> i(e) = c4 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( ~ sQ15_spl
| i(e) = c4 ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,plain,
( sQ15_spl
| sQ14_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f173,f181,f184,f187,f190]) ).
fof(f199,plain,
! [X0] :
( ~ sQ11_spl
| X0 = c1
| c2 != X0 ),
inference(paramodulation,[status(thm)],[f107,f20]) ).
fof(f204,plain,
( ~ sQ11_spl
| c2 = c1 ),
inference(destructive_equality_resolution,[status(thm)],[f199]) ).
fof(f205,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f204,f17]) ).
fof(f206,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f205]) ).
fof(f208,plain,
( ~ sQ15_spl
| mult(e,c4) = e ),
inference(paramodulation,[status(thm)],[f191,f12]) ).
fof(f218,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f252,plain,
! [X0,X1] :
( ~ sQ12_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = mult(X0,X1) ),
inference(paramodulation,[status(thm)],[f16,f182]) ).
fof(f255,plain,
! [X0,X1] :
( ~ sQ12_spl
| mult(X0,mult(c2,X1)) = mult(X0,X1) ),
inference(paramodulation,[status(thm)],[f182,f14]) ).
fof(f281,plain,
! [X0] :
( ~ sQ12_spl
| mult(X0,e) = mult(X0,i(c2)) ),
inference(paramodulation,[status(thm)],[f12,f255]) ).
fof(f294,plain,
! [X0] :
( ~ sQ12_spl
| X0 = mult(X0,i(c2)) ),
inference(forward_demodulation,[status(thm)],[f13,f281]) ).
fof(f301,plain,
( ~ sQ12_spl
| c2 = e ),
inference(paramodulation,[status(thm)],[f12,f294]) ).
fof(f325,plain,
! [X0] :
( X0 = c4
| X0 = c3
| X0 = c1
| c2 = c4
| c2 = X0
| c2 = c1 ),
inference(resolution,[status(thm)],[f32,f20]) ).
fof(f328,plain,
( c4 = c4
| c4 = c1
| c4 = c4
| c4 = c4
| c4 = c1 ),
inference(resolution,[status(thm)],[f32,f22]) ).
fof(f355,plain,
! [X0] :
( X0 = c3
| c3 != c3
| X0 = c4
| X0 = c1
| X0 = c4
| X0 = X0
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f32]) ).
fof(f364,definition,
! [X0] :
( sQ19_spl
<=> ( X0 = c4
| X0 = c3
| X0 = c1
| c2 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( sQ8_spl
| sQ19_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f325,f60,f364,f66]) ).
fof(f369,definition,
! [X0] :
( sQ20_spl
<=> ( X0 = c4
| X0 = c3
| X0 = c1
| c1 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f370,plain,
! [X0] :
( ~ sQ20_spl
| X0 = c4
| X0 = c3
| X0 = c1
| c1 = X0 ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f373,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f328,f45,f52]) ).
fof(f374,definition,
! [X0] :
( sQ21_spl
<=> ( X0 = c4
| X0 = c3
| X0 = c1
| c4 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f375,plain,
! [X0] :
( ~ sQ21_spl
| X0 = c4
| X0 = c3
| X0 = c1
| c4 = X0 ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f379,definition,
! [X0] :
( sQ22_spl
<=> ( X0 = c4
| X0 = c3
| X0 = c1
| c3 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f380,plain,
! [X0] :
( ~ sQ22_spl
| X0 = c4
| X0 = c3
| X0 = c1
| c3 = X0 ),
inference(component_clause,[status(thm)],[f379]) ).
fof(f407,definition,
! [X0] :
( sQ25_spl
<=> ( X0 = c1
| X0 = c4
| X0 = c3
| X0 = c4
| X0 = X0
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( ~ sQ5_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f355,f407,f56]) ).
fof(f417,definition,
! [X0] :
( sQ27_spl
<=> ( c3 = X0
| X0 != X0
| X0 = c4
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f418,plain,
! [X0] :
( ~ sQ27_spl
| c3 = X0
| X0 != X0
| X0 = c4
| X0 = c1 ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f433,plain,
! [X0] :
( ~ sQ21_spl
| X0 = c3
| X0 = c1
| c4 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f375]) ).
fof(f434,plain,
! [X0] :
( ~ sQ22_spl
| X0 = c4
| X0 = c1
| c3 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f380]) ).
fof(f435,plain,
! [X0] :
( ~ sQ20_spl
| X0 = c4
| X0 = c3
| c1 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f370]) ).
fof(f440,plain,
( ~ sQ12_spl
| e != c4 ),
inference(backward_demodulation,[status(thm)],[f301,f21]) ).
fof(f443,plain,
( ~ sQ12_spl
| e = c3
| e = c1
| e = c3
| e = e
| e = c1 ),
inference(resolution,[status(thm)],[f440,f32]) ).
fof(f444,plain,
! [X0] :
( ~ sQ12_spl
| e = c3
| e = c1
| X0 = c4
| X0 = c3
| X0 = e
| X0 = c1 ),
inference(resolution,[status(thm)],[f440,f32]) ).
fof(f448,definition,
( sQ31_spl
<=> e = c1 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ31_spl
| e = c1 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
( sQ32_spl
<=> e = e ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f454,definition,
( sQ33_spl
<=> e = c3 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ33_spl
| e = c3 ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f456,plain,
( sQ33_spl
| e != c3 ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f457,plain,
( ~ sQ12_spl
| sQ33_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f443,f448,f451,f454,f181]) ).
fof(f458,definition,
! [X0] :
( sQ34_spl
<=> ( X0 = c4
| X0 = c3
| X0 = e
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f459,plain,
! [X0] :
( ~ sQ34_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = c1 ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( ~ sQ12_spl
| sQ33_spl
| sQ31_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f444,f458,f448,f454,f181]) ).
fof(f465,plain,
! [X0] :
( ~ sQ27_spl
| c3 = X0
| X0 = c4
| X0 = c1 ),
inference(trivial_equality_resolution,[status(thm)],[f418]) ).
fof(f468,plain,
( ~ sQ31_spl
| e != c3 ),
inference(backward_demodulation,[status(thm)],[f449,f18]) ).
fof(f470,plain,
! [X0] :
( ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f16]) ).
fof(f476,plain,
! [X0] :
( ~ sQ31_spl
| X0 = e
| c2 != e
| X0 = c4
| X0 = c3 ),
inference(equality_factoring,[status(thm)],[f470]) ).
fof(f481,definition,
( sQ35_spl
<=> c4 = e ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f482,plain,
( ~ sQ35_spl
| c4 = e ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f483,plain,
( sQ35_spl
| c4 != e ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f486,definition,
( sQ36_spl
<=> c2 = e ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( ~ sQ36_spl
| c2 = e ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f488,plain,
( sQ36_spl
| c2 != e ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f491,definition,
! [X0] :
( sQ37_spl
<=> ( X0 = e
| X0 = c4
| X0 = c3 ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f492,plain,
! [X0] :
( ~ sQ37_spl
| X0 = e
| X0 = c4
| X0 = c3 ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,plain,
( ~ sQ31_spl
| ~ sQ36_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f476,f491,f486,f448]) ).
fof(f500,plain,
( ~ sQ35_spl
| c3 != e ),
inference(backward_demodulation,[status(thm)],[f482,f22]) ).
fof(f502,plain,
! [X0] :
( ~ sQ35_spl
| X0 = e
| X0 = c3
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f16]) ).
fof(f512,plain,
! [X0] :
( ~ sQ35_spl
| X0 = e
| c2 != e
| X0 = c3
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f502]) ).
fof(f517,definition,
! [X0] :
( sQ38_spl
<=> ( X0 = c1
| X0 = e
| X0 = c3 ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f518,plain,
! [X0] :
( ~ sQ38_spl
| X0 = c1
| X0 = e
| X0 = c3 ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f523,plain,
( ~ sQ35_spl
| ~ sQ36_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f512,f517,f486,f481]) ).
fof(f563,plain,
( ~ sQ21_spl
| c2 = c3
| c2 = c1 ),
inference(resolution,[status(thm)],[f433,f21]) ).
fof(f572,plain,
( ~ sQ21_spl
| sQ9_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f563,f60,f72,f374]) ).
fof(f579,plain,
( ~ sQ22_spl
| c2 = c1
| c3 = c2 ),
inference(resolution,[status(thm)],[f434,f21]) ).
fof(f588,plain,
( ~ sQ22_spl
| sQ6_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f579,f72,f60,f379]) ).
fof(f594,plain,
( ~ sQ20_spl
| c2 = c4
| c1 = c2 ),
inference(resolution,[status(thm)],[f435,f20]) ).
fof(f607,plain,
( ~ sQ20_spl
| sQ8_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f594,f60,f66,f369]) ).
fof(f614,definition,
! [X0] :
( sQ39_spl
<=> ( X0 = c1
| X0 = c4 ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f615,plain,
! [X0] :
( ~ sQ39_spl
| X0 = c1
| X0 = c4 ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f624,plain,
! [X0] :
( ~ sQ39_spl
| X0 = c1
| c3 != X0 ),
inference(paramodulation,[status(thm)],[f615,f22]) ).
fof(f630,plain,
( ~ sQ39_spl
| c3 = c1 ),
inference(destructive_equality_resolution,[status(thm)],[f624]) ).
fof(f631,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f18]) ).
fof(f632,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f631]) ).
fof(f668,plain,
( ~ sQ27_spl
| c2 = c4
| c2 = c1 ),
inference(resolution,[status(thm)],[f465,f20]) ).
fof(f680,plain,
( ~ sQ27_spl
| sQ8_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f668,f60,f66,f417]) ).
fof(f690,plain,
! [X0] :
( ~ sQ37_spl
| X0 = e
| X0 = c3
| c2 != X0 ),
inference(paramodulation,[status(thm)],[f492,f21]) ).
fof(f691,plain,
! [X0] :
( ~ sQ37_spl
| X0 = e
| X0 = c3
| c1 != X0 ),
inference(paramodulation,[status(thm)],[f492,f19]) ).
fof(f697,plain,
( ~ sQ37_spl
| c2 = e
| c2 = c3 ),
inference(destructive_equality_resolution,[status(thm)],[f690]) ).
fof(f698,plain,
( ~ sQ37_spl
| c2 = e ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f20]) ).
fof(f699,plain,
( ~ sQ37_spl
| c1 = e
| c1 = c3 ),
inference(destructive_equality_resolution,[status(thm)],[f691]) ).
fof(f700,plain,
( ~ sQ37_spl
| c1 = e ),
inference(forward_subsumption_resolution,[status(thm)],[f699,f18]) ).
fof(f701,definition,
! [X0] :
( sQ40_spl
<=> ( X0 = c3
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f702,plain,
! [X0] :
( ~ sQ40_spl
| X0 = c3
| X0 = e ),
inference(component_clause,[status(thm)],[f701]) ).
fof(f707,plain,
( ~ sQ37_spl
| c1 != e ),
inference(backward_demodulation,[status(thm)],[f698,f17]) ).
fof(f717,plain,
( ~ sQ37_spl
| e != e ),
inference(forward_demodulation,[status(thm)],[f700,f707]) ).
fof(f718,plain,
( ~ sQ37_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f717]) ).
fof(f719,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f729,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f751,plain,
( ~ sQ40_spl
| c1 = e ),
inference(resolution,[status(thm)],[f702,f18]) ).
fof(f759,plain,
( ~ sQ40_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f751,f448,f701]) ).
fof(f760,definition,
! [X0] :
( sQ41_spl
<=> ( X0 = c2
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f761,plain,
! [X0] :
( ~ sQ41_spl
| X0 = c2
| X0 = e ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f768,plain,
( ~ sQ41_spl
| c1 = e ),
inference(resolution,[status(thm)],[f761,f17]) ).
fof(f776,plain,
( ~ sQ41_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f768,f448,f760]) ).
fof(f795,plain,
! [X0] :
( ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f455,f16]) ).
fof(f796,plain,
( ~ sQ33_spl
| c2 != e ),
inference(backward_demodulation,[status(thm)],[f455,f20]) ).
fof(f798,plain,
( ~ sQ33_spl
| e != c4 ),
inference(backward_demodulation,[status(thm)],[f455,f22]) ).
fof(f800,plain,
( ~ sQ33_spl
| e = c4
| e = e
| e = c1 ),
inference(resolution,[status(thm)],[f795,f796]) ).
fof(f809,plain,
! [X0] :
( ~ sQ33_spl
| X0 = e
| c2 != e
| X0 = c4
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f795]) ).
fof(f813,plain,
( ~ sQ33_spl
| sQ35_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f800,f448,f451,f481,f454]) ).
fof(f818,definition,
! [X0] :
( sQ42_spl
<=> ( X0 = c1
| X0 = c4
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f819,plain,
! [X0] :
( ~ sQ42_spl
| X0 = c1
| X0 = c4
| X0 = e ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f822,plain,
( ~ sQ33_spl
| ~ sQ36_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f809,f818,f486,f454]) ).
fof(f827,definition,
( sQ43_spl
<=> i(e) = e ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f843,plain,
! [X0,X1] :
( ~ sQ33_spl
| mult(X0,mult(X1,i(mult(X0,X1)))) = c4
| mult(X0,mult(X1,i(mult(X0,X1)))) = e
| mult(X0,mult(X1,i(mult(X0,X1)))) = c1
| c2 = e ),
inference(paramodulation,[status(thm)],[f795,f116]) ).
fof(f860,definition,
! [X0,X1] :
( sQ44_spl
<=> ( mult(X0,mult(X1,i(mult(X0,X1)))) = c4
| mult(X0,mult(X1,i(mult(X0,X1)))) = e
| mult(X0,mult(X1,i(mult(X0,X1)))) = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f863,plain,
( ~ sQ33_spl
| sQ44_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f843,f486,f860,f454]) ).
fof(f884,plain,
( ~ sQ31_spl
| e != c4 ),
inference(backward_demodulation,[status(thm)],[f449,f19]) ).
fof(f889,plain,
( ~ sQ31_spl
| e = c4
| e = c2
| e = e ),
inference(resolution,[status(thm)],[f470,f468]) ).
fof(f903,plain,
( ~ sQ31_spl
| sQ35_spl
| sQ36_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f889,f451,f486,f481,f448]) ).
fof(f912,plain,
( ~ sQ33_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f468]) ).
fof(f913,plain,
( ~ sQ33_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f912]) ).
fof(f924,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f958,plain,
( ~ sQ31_spl
| e = c3
| e = c2
| e = e ),
inference(resolution,[status(thm)],[f470,f884]) ).
fof(f974,plain,
( ~ sQ31_spl
| sQ33_spl
| sQ36_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f958,f451,f486,f454,f448]) ).
fof(f983,plain,
( ~ sQ13_spl
| ~ sQ31_spl
| i(e) = e ),
inference(forward_demodulation,[status(thm)],[f449,f185]) ).
fof(f984,plain,
( ~ sQ31_spl
| ~ sQ13_spl
| i(e) = c4
| i(e) = c3
| i(e) = e
| c2 = e ),
inference(paramodulation,[status(thm)],[f470,f983]) ).
fof(f986,plain,
( ~ sQ31_spl
| ~ sQ13_spl
| sQ15_spl
| sQ14_spl
| sQ43_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f984,f486,f827,f187,f190,f184,f448]) ).
fof(f992,plain,
( ~ sQ12_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f301,f486,f181]) ).
fof(f1012,plain,
! [X0] : mult(X0,e) = mult(e,i(i(X0))),
inference(paramodulation,[status(thm)],[f12,f119]) ).
fof(f1028,plain,
! [X0] : X0 = mult(e,i(i(X0))),
inference(forward_demodulation,[status(thm)],[f13,f1012]) ).
fof(f1040,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,i(i(X1))),
inference(paramodulation,[status(thm)],[f1028,f118]) ).
fof(f1046,plain,
! [X0] : X0 = mult(e,X0),
inference(backward_demodulation,[status(thm)],[f1040,f1028]) ).
fof(f1049,plain,
! [X0] : mult(i(X0),X0) = e,
inference(paramodulation,[status(thm)],[f12,f1040]) ).
fof(f1074,plain,
! [X0] : i(i(X0)) = mult(e,X0),
inference(paramodulation,[status(thm)],[f1040,f1046]) ).
fof(f1087,plain,
! [X0] : i(i(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1046,f1074]) ).
fof(f1101,plain,
! [X0] :
( ~ sQ31_spl
| mult(i(X0),X0) = c4
| mult(i(X0),X0) = c3
| mult(i(X0),X0) = e
| c2 = e ),
inference(paramodulation,[status(thm)],[f470,f1049]) ).
fof(f1106,plain,
e = i(e),
inference(paramodulation,[status(thm)],[f1049,f13]) ).
fof(f1108,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(e,X1),
inference(paramodulation,[status(thm)],[f1049,f14]) ).
fof(f1109,definition,
! [X0] :
( sQ45_spl
<=> ( mult(i(X0),X0) = c4
| mult(i(X0),X0) = c3
| mult(i(X0),X0) = e ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1112,plain,
( ~ sQ31_spl
| sQ45_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1101,f486,f1109,f448]) ).
fof(f1115,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f1046,f1108]) ).
fof(f1127,plain,
! [X0,X1] :
( X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f1158,plain,
( ~ sQ33_spl
| e = e
| e = c2
| e = c1 ),
inference(resolution,[status(thm)],[f795,f798]) ).
fof(f1171,plain,
( ~ sQ33_spl
| sQ32_spl
| sQ36_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1158,f448,f486,f451,f454]) ).
fof(f1204,plain,
( ~ sQ35_spl
| i(e) = e
| i(e) = c3
| i(e) = c1
| e = c2 ),
inference(paramodulation,[status(thm)],[f502,f1106]) ).
fof(f1208,plain,
( ~ sQ35_spl
| sQ43_spl
| sQ14_spl
| sQ13_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1204,f486,f184,f187,f827,f481]) ).
fof(f1210,plain,
( ~ sQ15_spl
| c4 = e ),
inference(forward_demodulation,[status(thm)],[f1046,f208]) ).
fof(f1213,plain,
( sQ14_spl
| e != c3 ),
inference(forward_demodulation,[status(thm)],[f1106,f189]) ).
fof(f1258,plain,
! [X0,X1] : mult(i(X0),e) = mult(X1,i(mult(X0,X1))),
inference(paramodulation,[status(thm)],[f116,f1115]) ).
fof(f1272,plain,
! [X0,X1] : i(X0) = mult(X1,i(mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f13,f1258]) ).
fof(f1277,plain,
! [X0,X1] :
( ~ sQ35_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = e
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f133]) ).
fof(f1278,plain,
! [X0,X1] :
( ~ sQ35_spl
| X1 = e
| X1 = c3
| X1 = c1
| X0 = e
| X0 = c3
| X0 = X1
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f1277]) ).
fof(f1282,plain,
! [X0] :
( ~ sQ35_spl
| X0 = e
| X0 = c3
| X0 = c1
| c2 = e
| c2 = X0
| c2 = c1 ),
inference(resolution,[status(thm)],[f1278,f20]) ).
fof(f1283,plain,
( ~ sQ35_spl
| e = e
| e = c1
| e = e
| e = e
| e = c1 ),
inference(resolution,[status(thm)],[f1278,f500]) ).
fof(f1299,plain,
! [X0,X1] :
( ~ sQ35_spl
| X0 = e
| c3 != e
| X1 = e
| X1 = c3
| X1 = c1
| X0 = X1
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f1278]) ).
fof(f1301,plain,
! [X0] :
( ~ sQ35_spl
| X0 = c3
| c3 != c3
| X0 = e
| X0 = c1
| X0 = e
| X0 = X0
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f1278]) ).
fof(f1314,definition,
! [X0] :
( sQ47_spl
<=> ( X0 = e
| X0 = c3
| X0 = c1
| c2 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
( ~ sQ35_spl
| sQ36_spl
| sQ47_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1282,f60,f1314,f486,f481]) ).
fof(f1318,plain,
( ~ sQ35_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1283,f448,f451,f481]) ).
fof(f1319,definition,
! [X0] :
( sQ48_spl
<=> ( X0 = e
| X0 = c3
| X0 = c1
| e = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1320,plain,
! [X0] :
( ~ sQ48_spl
| X0 = e
| X0 = c3
| X0 = c1
| e = X0 ),
inference(component_clause,[status(thm)],[f1319]) ).
fof(f1337,definition,
! [X0,X1] :
( sQ51_spl
<=> ( X0 = c1
| X1 = e
| X1 = c3
| X1 = c1
| X0 = e
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1341,plain,
( ~ sQ35_spl
| ~ sQ33_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1299,f1337,f454,f481]) ).
fof(f1342,definition,
! [X0] :
( sQ52_spl
<=> ( X0 = c1
| X0 = e
| X0 = c3
| X0 = e
| X0 = X0
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1346,plain,
( ~ sQ35_spl
| ~ sQ5_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1301,f1342,f56,f481]) ).
fof(f1364,plain,
( sQ14_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1213,f454,f187]) ).
fof(f1365,plain,
( ~ sQ15_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1210,f481,f190]) ).
fof(f1367,plain,
( ~ sQ14_spl
| e = c3 ),
inference(forward_demodulation,[status(thm)],[f1106,f188]) ).
fof(f1373,plain,
! [X0] :
( ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f455,f16]) ).
fof(f1451,plain,
! [X0,X1] : i(X0) = mult(i(mult(X1,X0)),i(i(X1))),
inference(paramodulation,[status(thm)],[f1272,f1272]) ).
fof(f1469,plain,
! [X0,X1] : i(X0) = mult(i(mult(X1,X0)),X1),
inference(forward_demodulation,[status(thm)],[f1087,f1451]) ).
fof(f1471,plain,
! [X0,X1] :
( ~ sQ33_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = e
| X0 = X1
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f455,f218]) ).
fof(f1472,plain,
! [X0,X1] :
( ~ sQ33_spl
| X1 = c4
| X1 = e
| X1 = c1
| X0 = c4
| X0 = e
| X0 = X1
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f455,f1471]) ).
fof(f1476,plain,
! [X0] :
( ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = c1
| c2 = e
| c2 = X0
| c2 = c1 ),
inference(resolution,[status(thm)],[f1472,f21]) ).
fof(f1493,plain,
! [X0,X1] :
( ~ sQ33_spl
| X0 = e
| c4 != e
| X1 = c4
| X1 = e
| X1 = c1
| X0 = X1
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f1472]) ).
fof(f1495,plain,
! [X0] :
( ~ sQ33_spl
| X0 = e
| c4 != e
| X0 = c4
| X0 = c1
| X0 = e
| X0 = X0
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f1472]) ).
fof(f1496,plain,
! [X0] :
( ~ sQ33_spl
| X0 = c4
| c4 != c4
| X0 = e
| X0 = c1
| X0 = e
| X0 = X0
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f1472]) ).
fof(f1508,definition,
! [X0] :
( sQ58_spl
<=> ( X0 = c4
| X0 = e
| X0 = c1
| c2 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1511,plain,
( ~ sQ33_spl
| sQ36_spl
| sQ58_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1476,f60,f1508,f486,f454]) ).
fof(f1531,definition,
! [X0,X1] :
( sQ62_spl
<=> ( X0 = c1
| X1 = c4
| X1 = e
| X1 = c1
| X0 = e
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1535,plain,
( ~ sQ33_spl
| ~ sQ35_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1493,f1531,f481,f454]) ).
fof(f1536,definition,
! [X0] :
( sQ63_spl
<=> ( X0 = c1
| X0 = c4
| X0 = e
| X0 = e
| X0 = X0
| X0 = c1 ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1540,plain,
( ~ sQ33_spl
| ~ sQ35_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1495,f1536,f481,f454]) ).
fof(f1541,plain,
( ~ sQ33_spl
| ~ sQ4_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1496,f1536,f52,f454]) ).
fof(f1558,plain,
( ~ sQ14_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1367,f454,f187]) ).
fof(f1560,plain,
( ~ sQ36_spl
| c1 != e ),
inference(backward_demodulation,[status(thm)],[f487,f17]) ).
fof(f1561,plain,
( ~ sQ36_spl
| e != c3 ),
inference(forward_demodulation,[status(thm)],[f487,f20]) ).
fof(f1562,plain,
! [X0] :
( ~ sQ36_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f487,f16]) ).
fof(f1563,plain,
( ~ sQ36_spl
| e = c4
| e = e
| e = c1 ),
inference(resolution,[status(thm)],[f1562,f1561]) ).
fof(f1576,plain,
( ~ sQ36_spl
| sQ35_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1563,f448,f451,f481,f486]) ).
fof(f1620,plain,
! [X0] :
( ~ sQ36_spl
| X0 = c4
| X0 = c3
| X0 = c1
| e = c4
| e = X0
| e = c1 ),
inference(resolution,[status(thm)],[f32,f1561]) ).
fof(f1660,plain,
( ~ sQ36_spl
| sQ35_spl
| sQ34_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1620,f448,f458,f481,f486]) ).
fof(f1950,plain,
! [X0] :
( ~ sQ12_spl
| e = c4
| e = c3
| e = c1
| X0 = X0 ),
inference(paramodulation,[status(thm)],[f13,f252]) ).
fof(f1971,definition,
! [X0] :
( sQ68_spl
<=> X0 = X0 ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1974,plain,
( ~ sQ12_spl
| sQ35_spl
| sQ33_spl
| sQ31_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1950,f1971,f448,f454,f481,f181]) ).
fof(f1977,definition,
( sQ69_spl
<=> mult(op_a,op_b) = op_b ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1978,plain,
( ~ sQ69_spl
| mult(op_a,op_b) = op_b ),
inference(component_clause,[status(thm)],[f1977]) ).
fof(f1979,plain,
( sQ69_spl
| mult(op_a,op_b) != op_b ),
inference(component_clause,[status(thm)],[f1977]) ).
fof(f1980,definition,
( sQ70_spl
<=> op_a = c1 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1981,plain,
( ~ sQ70_spl
| op_a = c1 ),
inference(component_clause,[status(thm)],[f1980]) ).
fof(f1983,definition,
( sQ71_spl
<=> op_a = c3 ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1984,plain,
( ~ sQ71_spl
| op_a = c3 ),
inference(component_clause,[status(thm)],[f1983]) ).
fof(f1985,plain,
( sQ71_spl
| op_a != c3 ),
inference(component_clause,[status(thm)],[f1983]) ).
fof(f1986,definition,
( sQ72_spl
<=> op_a = c4 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1987,plain,
( ~ sQ72_spl
| op_a = c4 ),
inference(component_clause,[status(thm)],[f1986]) ).
fof(f1988,plain,
( sQ72_spl
| op_a != c4 ),
inference(component_clause,[status(thm)],[f1986]) ).
fof(f1995,plain,
! [X0] :
( ~ sQ48_spl
| X0 = c3
| X0 = c1
| e = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f1320]) ).
fof(f2000,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = c3
| X0 = e
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1987,f1562]) ).
fof(f2001,plain,
( ~ sQ72_spl
| c3 != op_a ),
inference(backward_demodulation,[status(thm)],[f1987,f22]) ).
fof(f2007,plain,
( ~ sQ72_spl
| ~ sQ36_spl
| op_a = op_a
| op_a = e
| op_a = c1 ),
inference(resolution,[status(thm)],[f2000,f2001]) ).
fof(f2015,definition,
( sQ73_spl
<=> e = op_a ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2016,plain,
( ~ sQ73_spl
| e = op_a ),
inference(component_clause,[status(thm)],[f2015]) ).
fof(f2017,plain,
( sQ73_spl
| e != op_a ),
inference(component_clause,[status(thm)],[f2015]) ).
fof(f2020,definition,
( sQ74_spl
<=> op_a = op_a ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f2023,plain,
( ~ sQ72_spl
| ~ sQ36_spl
| sQ74_spl
| sQ73_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2007,f1980,f2015,f2020,f486,f1986]) ).
fof(f2024,definition,
! [X0] :
( sQ75_spl
<=> ( X0 = c1
| X0 = op_a
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2025,plain,
! [X0] :
( ~ sQ75_spl
| X0 = c1
| X0 = op_a
| X0 = e ),
inference(component_clause,[status(thm)],[f2024]) ).
fof(f2030,plain,
( ~ sQ70_spl
| op_a != c3 ),
inference(backward_demodulation,[status(thm)],[f1981,f18]) ).
fof(f2032,plain,
( ~ sQ70_spl
| op_a != c4 ),
inference(forward_demodulation,[status(thm)],[f1981,f19]) ).
fof(f2033,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f1562]) ).
fof(f2034,plain,
( ~ sQ70_spl
| ~ sQ36_spl
| op_a = c4
| op_a = e
| op_a = op_a ),
inference(resolution,[status(thm)],[f2033,f2030]) ).
fof(f2047,plain,
( ~ sQ70_spl
| ~ sQ36_spl
| sQ72_spl
| sQ73_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f2034,f2020,f2015,f1986,f486,f1980]) ).
fof(f2060,plain,
( ~ sQ73_spl
| mult(op_a,op_b) != mult(op_b,e) ),
inference(backward_demodulation,[status(thm)],[f2016,f15]) ).
fof(f2061,plain,
( ~ sQ73_spl
| mult(e,op_b) != mult(op_b,e) ),
inference(forward_demodulation,[status(thm)],[f2016,f2060]) ).
fof(f2062,plain,
( ~ sQ73_spl
| op_b != mult(op_b,e) ),
inference(forward_demodulation,[status(thm)],[f1046,f2061]) ).
fof(f2063,plain,
( ~ sQ73_spl
| op_b != op_b ),
inference(forward_demodulation,[status(thm)],[f13,f2062]) ).
fof(f2064,plain,
( ~ sQ73_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2063]) ).
fof(f2065,plain,
~ sQ73_spl,
inference(contradiction_clause,[status(thm)],[f2064]) ).
fof(f2089,plain,
( ~ sQ36_spl
| sQ69_spl
| mult(op_a,op_b) = c4
| mult(op_a,op_b) = e
| mult(op_a,op_b) = c1
| c3 != op_b ),
inference(paramodulation,[status(thm)],[f1562,f1979]) ).
fof(f2090,definition,
( sQ77_spl
<=> c3 = op_b ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2091,plain,
( ~ sQ77_spl
| c3 = op_b ),
inference(component_clause,[status(thm)],[f2090]) ).
fof(f2092,plain,
( sQ77_spl
| c3 != op_b ),
inference(component_clause,[status(thm)],[f2090]) ).
fof(f2093,definition,
( sQ78_spl
<=> mult(op_a,op_b) = c1 ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2094,plain,
( ~ sQ78_spl
| mult(op_a,op_b) = c1 ),
inference(component_clause,[status(thm)],[f2093]) ).
fof(f2095,plain,
( sQ78_spl
| mult(op_a,op_b) != c1 ),
inference(component_clause,[status(thm)],[f2093]) ).
fof(f2096,definition,
( sQ79_spl
<=> mult(op_a,op_b) = e ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f2097,plain,
( ~ sQ79_spl
| mult(op_a,op_b) = e ),
inference(component_clause,[status(thm)],[f2096]) ).
fof(f2098,plain,
( sQ79_spl
| mult(op_a,op_b) != e ),
inference(component_clause,[status(thm)],[f2096]) ).
fof(f2099,definition,
( sQ80_spl
<=> mult(op_a,op_b) = c4 ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f2100,plain,
( ~ sQ80_spl
| mult(op_a,op_b) = c4 ),
inference(component_clause,[status(thm)],[f2099]) ).
fof(f2101,plain,
( sQ80_spl
| mult(op_a,op_b) != c4 ),
inference(component_clause,[status(thm)],[f2099]) ).
fof(f2102,plain,
( ~ sQ36_spl
| sQ69_spl
| sQ80_spl
| sQ79_spl
| sQ78_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f2089,f2090,f2093,f2096,f2099,f1977,f486]) ).
fof(f2115,plain,
( ~ sQ36_spl
| sQ77_spl
| op_b = c4
| op_b = e
| op_b = c1 ),
inference(resolution,[status(thm)],[f2092,f1562]) ).
fof(f2117,definition,
( sQ81_spl
<=> op_b = c1 ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f2118,plain,
( ~ sQ81_spl
| op_b = c1 ),
inference(component_clause,[status(thm)],[f2117]) ).
fof(f2119,plain,
( sQ81_spl
| op_b != c1 ),
inference(component_clause,[status(thm)],[f2117]) ).
fof(f2120,definition,
( sQ82_spl
<=> op_b = e ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f2121,plain,
( ~ sQ82_spl
| op_b = e ),
inference(component_clause,[status(thm)],[f2120]) ).
fof(f2122,plain,
( sQ82_spl
| op_b != e ),
inference(component_clause,[status(thm)],[f2120]) ).
fof(f2123,definition,
( sQ83_spl
<=> op_b = c4 ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f2124,plain,
( ~ sQ83_spl
| op_b = c4 ),
inference(component_clause,[status(thm)],[f2123]) ).
fof(f2125,plain,
( sQ83_spl
| op_b != c4 ),
inference(component_clause,[status(thm)],[f2123]) ).
fof(f2126,plain,
( ~ sQ36_spl
| sQ77_spl
| sQ83_spl
| sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f2115,f2117,f2120,f2123,f2090,f486]) ).
fof(f2128,plain,
( ~ sQ36_spl
| sQ72_spl
| op_a = c3
| op_a = e
| op_a = c1 ),
inference(resolution,[status(thm)],[f1988,f1562]) ).
fof(f2130,plain,
( ~ sQ36_spl
| sQ72_spl
| sQ71_spl
| sQ73_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2128,f1980,f2015,f1983,f1986,f486]) ).
fof(f2132,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = e
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f1562]) ).
fof(f2134,plain,
( ~ sQ71_spl
| op_a != c4 ),
inference(backward_demodulation,[status(thm)],[f1984,f22]) ).
fof(f2139,plain,
( ~ sQ82_spl
| mult(op_a,op_b) != mult(e,op_a) ),
inference(backward_demodulation,[status(thm)],[f2121,f15]) ).
fof(f2141,plain,
( ~ sQ82_spl
| mult(op_a,e) != mult(e,op_a) ),
inference(forward_demodulation,[status(thm)],[f2121,f2139]) ).
fof(f2142,plain,
( ~ sQ82_spl
| op_a != mult(e,op_a) ),
inference(forward_demodulation,[status(thm)],[f13,f2141]) ).
fof(f2143,plain,
( ~ sQ82_spl
| op_a != op_a ),
inference(forward_demodulation,[status(thm)],[f1046,f2142]) ).
fof(f2144,plain,
( ~ sQ82_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2143]) ).
fof(f2145,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f2144]) ).
fof(f2148,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| X0 = c4
| X0 = op_a
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f2132]) ).
fof(f2155,definition,
( sQ84_spl
<=> op_a = op_b ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2156,plain,
( ~ sQ84_spl
| op_a = op_b ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2157,plain,
( sQ84_spl
| op_a != op_b ),
inference(component_clause,[status(thm)],[f2155]) ).
fof(f2159,definition,
! [X0] :
( sQ85_spl
<=> ( X0 = op_b
| X0 = op_a
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2166,plain,
( ~ sQ84_spl
| mult(op_a,op_a) != mult(op_b,op_a) ),
inference(forward_demodulation,[status(thm)],[f2156,f15]) ).
fof(f2167,plain,
( ~ sQ84_spl
| mult(op_a,op_a) != mult(op_a,op_a) ),
inference(forward_demodulation,[status(thm)],[f2156,f2166]) ).
fof(f2168,plain,
( ~ sQ84_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2167]) ).
fof(f2169,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f2168]) ).
fof(f2184,definition,
( sQ86_spl
<=> op_b = op_b ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2196,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f1562]) ).
fof(f2229,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| mult(op_a,op_b) = op_b ),
inference(forward_demodulation,[status(thm)],[f2124,f2100]) ).
fof(f2231,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| i(op_a) = mult(op_b,i(op_b)) ),
inference(paramodulation,[status(thm)],[f2229,f1272]) ).
fof(f2234,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| i(op_a) = e ),
inference(forward_demodulation,[status(thm)],[f12,f2231]) ).
fof(f2241,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| mult(e,op_a) = e ),
inference(paramodulation,[status(thm)],[f2234,f1049]) ).
fof(f2250,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f1046,f2241]) ).
fof(f2251,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2250,f2017]) ).
fof(f2252,plain,
( ~ sQ80_spl
| ~ sQ83_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f2251]) ).
fof(f2253,plain,
( ~ sQ81_spl
| ~ sQ70_spl
| op_b = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f2118]) ).
fof(f2254,plain,
( ~ sQ81_spl
| ~ sQ70_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2253,f2157]) ).
fof(f2255,plain,
( ~ sQ81_spl
| ~ sQ70_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f2254]) ).
fof(f2258,plain,
( sQ83_spl
| ~ sQ36_spl
| ~ sQ71_spl
| op_b = op_a
| op_b = e
| op_b = c1 ),
inference(resolution,[status(thm)],[f2132,f2125]) ).
fof(f2259,plain,
( ~ sQ71_spl
| ~ sQ36_spl
| op_a = op_a
| op_a = e
| op_a = c1 ),
inference(resolution,[status(thm)],[f2132,f2134]) ).
fof(f2268,plain,
( sQ83_spl
| ~ sQ36_spl
| ~ sQ71_spl
| sQ84_spl
| sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f2258,f2117,f2120,f2155,f1983,f486,f2123]) ).
fof(f2269,plain,
( ~ sQ71_spl
| ~ sQ36_spl
| sQ74_spl
| sQ73_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2259,f1980,f2015,f2020,f486,f1983]) ).
fof(f2278,plain,
( ~ sQ81_spl
| op_b != c4 ),
inference(forward_demodulation,[status(thm)],[f2118,f19]) ).
fof(f2301,plain,
( ~ sQ79_spl
| i(op_b) = mult(i(e),op_a) ),
inference(paramodulation,[status(thm)],[f2097,f1469]) ).
fof(f2305,definition,
( sQ87_spl
<=> mult(op_a,op_b) = op_a ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2306,plain,
( ~ sQ87_spl
| mult(op_a,op_b) = op_a ),
inference(component_clause,[status(thm)],[f2305]) ).
fof(f2307,plain,
( sQ87_spl
| mult(op_a,op_b) != op_a ),
inference(component_clause,[status(thm)],[f2305]) ).
fof(f2309,plain,
( ~ sQ79_spl
| i(op_b) = mult(e,op_a) ),
inference(forward_demodulation,[status(thm)],[f1106,f2301]) ).
fof(f2310,plain,
( ~ sQ79_spl
| i(op_b) = op_a ),
inference(forward_demodulation,[status(thm)],[f1046,f2309]) ).
fof(f2324,plain,
( ~ sQ79_spl
| mult(op_b,op_a) = e ),
inference(paramodulation,[status(thm)],[f2310,f12]) ).
fof(f2325,definition,
( sQ88_spl
<=> i(op_b) = op_b ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2326,plain,
( ~ sQ88_spl
| i(op_b) = op_b ),
inference(component_clause,[status(thm)],[f2325]) ).
fof(f2328,definition,
( sQ89_spl
<=> i(op_b) = e ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2329,plain,
( ~ sQ89_spl
| i(op_b) = e ),
inference(component_clause,[status(thm)],[f2328]) ).
fof(f2330,plain,
( sQ89_spl
| i(op_b) != e ),
inference(component_clause,[status(thm)],[f2328]) ).
fof(f2331,definition,
( sQ90_spl
<=> i(op_b) = op_a ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2332,plain,
( ~ sQ90_spl
| i(op_b) = op_a ),
inference(component_clause,[status(thm)],[f2331]) ).
fof(f2333,plain,
( sQ90_spl
| i(op_b) != op_a ),
inference(component_clause,[status(thm)],[f2331]) ).
fof(f2335,plain,
( ~ sQ78_spl
| ~ sQ81_spl
| mult(op_a,op_b) = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f2094]) ).
fof(f2344,plain,
( ~ sQ90_spl
| i(op_a) = op_b ),
inference(paramodulation,[status(thm)],[f2332,f1087]) ).
fof(f2345,plain,
( ~ sQ90_spl
| mult(op_b,op_a) = e ),
inference(paramodulation,[status(thm)],[f2332,f12]) ).
fof(f2391,plain,
( ~ sQ79_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2310,f2331,f2096]) ).
fof(f2423,plain,
( ~ sQ89_spl
| mult(e,op_b) = e ),
inference(paramodulation,[status(thm)],[f2329,f1049]) ).
fof(f2433,plain,
( ~ sQ89_spl
| op_b = e ),
inference(forward_demodulation,[status(thm)],[f1046,f2423]) ).
fof(f2434,plain,
( ~ sQ89_spl
| sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2433,f2122]) ).
fof(f2435,plain,
( ~ sQ89_spl
| sQ82_spl ),
inference(contradiction_clause,[status(thm)],[f2434]) ).
fof(f2450,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_b
| mult(op_a,op_b) != c4 ),
inference(paramodulation,[status(thm)],[f2148,f15]) ).
fof(f2451,definition,
( sQ94_spl
<=> mult(op_b,op_a) = op_b ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f2452,plain,
( ~ sQ94_spl
| mult(op_b,op_a) = op_b ),
inference(component_clause,[status(thm)],[f2451]) ).
fof(f2453,plain,
( sQ94_spl
| mult(op_b,op_a) != op_b ),
inference(component_clause,[status(thm)],[f2451]) ).
fof(f2454,definition,
( sQ95_spl
<=> mult(op_b,op_a) = e ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2455,plain,
( ~ sQ95_spl
| mult(op_b,op_a) = e ),
inference(component_clause,[status(thm)],[f2454]) ).
fof(f2456,plain,
( sQ95_spl
| mult(op_b,op_a) != e ),
inference(component_clause,[status(thm)],[f2454]) ).
fof(f2457,definition,
( sQ96_spl
<=> mult(op_b,op_a) = op_a ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2458,plain,
( ~ sQ96_spl
| mult(op_b,op_a) = op_a ),
inference(component_clause,[status(thm)],[f2457]) ).
fof(f2459,plain,
( sQ96_spl
| mult(op_b,op_a) != op_a ),
inference(component_clause,[status(thm)],[f2457]) ).
fof(f2460,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| sQ96_spl
| sQ95_spl
| sQ94_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f2450,f2099,f2451,f2454,f2457,f2117,f1983,f486]) ).
fof(f2482,plain,
( ~ sQ87_spl
| mult(i(op_a),op_a) = op_b ),
inference(paramodulation,[status(thm)],[f2306,f1115]) ).
fof(f2499,definition,
( sQ97_spl
<=> i(op_a) = op_b ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f2500,plain,
( ~ sQ97_spl
| i(op_a) = op_b ),
inference(component_clause,[status(thm)],[f2499]) ).
fof(f2501,plain,
( sQ97_spl
| i(op_a) != op_b ),
inference(component_clause,[status(thm)],[f2499]) ).
fof(f2502,definition,
( sQ98_spl
<=> i(op_a) = e ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2503,plain,
( ~ sQ98_spl
| i(op_a) = e ),
inference(component_clause,[status(thm)],[f2502]) ).
fof(f2504,plain,
( sQ98_spl
| i(op_a) != e ),
inference(component_clause,[status(thm)],[f2502]) ).
fof(f2505,definition,
( sQ99_spl
<=> i(op_a) = op_a ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2506,plain,
( ~ sQ99_spl
| i(op_a) = op_a ),
inference(component_clause,[status(thm)],[f2505]) ).
fof(f2507,plain,
( sQ99_spl
| i(op_a) != op_a ),
inference(component_clause,[status(thm)],[f2505]) ).
fof(f2509,plain,
( ~ sQ99_spl
| ~ sQ90_spl
| op_b = op_a ),
inference(forward_demodulation,[status(thm)],[f2344,f2506]) ).
fof(f2510,plain,
( ~ sQ99_spl
| ~ sQ90_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2509,f2157]) ).
fof(f2511,plain,
( ~ sQ99_spl
| ~ sQ90_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f2510]) ).
fof(f2525,plain,
( ~ sQ98_spl
| mult(e,op_a) = e ),
inference(paramodulation,[status(thm)],[f2503,f1049]) ).
fof(f2535,plain,
( ~ sQ98_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f1046,f2525]) ).
fof(f2536,plain,
( ~ sQ98_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2535,f2017]) ).
fof(f2537,plain,
( ~ sQ98_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f2536]) ).
fof(f2546,plain,
( ~ sQ97_spl
| i(op_b) = op_a ),
inference(paramodulation,[status(thm)],[f2500,f1087]) ).
fof(f2547,plain,
( ~ sQ97_spl
| mult(op_a,op_b) = e ),
inference(paramodulation,[status(thm)],[f2500,f12]) ).
fof(f2549,plain,
( ~ sQ97_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2546,f2331,f2499]) ).
fof(f2550,plain,
( ~ sQ97_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f2547,f2096,f2499]) ).
fof(f2553,plain,
! [X0,X1] :
( ~ sQ81_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f729]) ).
fof(f2554,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1984,f2553]) ).
fof(f2555,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = c3
| X1 = op_b
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f2554]) ).
fof(f2556,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = op_a
| X1 = op_b
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1984,f2555]) ).
fof(f2561,plain,
( sQ35_spl
| ~ sQ81_spl
| ~ sQ71_spl
| e = op_a
| e = op_b
| e = op_a
| e = e
| e = op_b ),
inference(resolution,[status(thm)],[f2556,f483]) ).
fof(f2582,plain,
! [X0] :
( ~ sQ81_spl
| ~ sQ71_spl
| X0 = c4
| c4 != c4
| X0 = op_a
| X0 = op_b
| X0 = op_a
| X0 = X0
| X0 = op_b ),
inference(equality_factoring,[status(thm)],[f2556]) ).
fof(f2594,definition,
! [X0] :
( sQ101_spl
<=> ( X0 = c4
| X0 = op_a
| X0 = op_b
| op_a = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2595,plain,
! [X0] :
( ~ sQ101_spl
| X0 = c4
| X0 = op_a
| X0 = op_b
| op_a = X0 ),
inference(component_clause,[status(thm)],[f2594]) ).
fof(f2598,plain,
( sQ35_spl
| ~ sQ81_spl
| ~ sQ71_spl
| sQ73_spl
| sQ32_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f2561,f2120,f451,f2015,f1983,f2117,f481]) ).
fof(f2599,definition,
! [X0] :
( sQ102_spl
<=> ( X0 = c4
| X0 = op_a
| X0 = op_b
| e = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2606,definition,
( sQ104_spl
<=> i(op_b) = c4 ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f2607,plain,
( ~ sQ104_spl
| i(op_b) = c4 ),
inference(component_clause,[status(thm)],[f2606]) ).
fof(f2608,plain,
( sQ104_spl
| i(op_b) != c4 ),
inference(component_clause,[status(thm)],[f2606]) ).
fof(f2625,definition,
! [X0] :
( sQ107_spl
<=> ( X0 = op_b
| X0 = c4
| X0 = op_a
| X0 = op_a
| X0 = X0
| X0 = op_b ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2630,plain,
( ~ sQ81_spl
| ~ sQ71_spl
| ~ sQ4_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f2582,f2625,f52,f1983,f2117]) ).
fof(f2647,plain,
! [X0] :
( ~ sQ101_spl
| X0 = c4
| X0 = op_b
| op_a = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f2595]) ).
fof(f2661,definition,
( sQ113_spl
<=> i(op_a) = c4 ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f2662,plain,
( ~ sQ113_spl
| i(op_a) = c4 ),
inference(component_clause,[status(thm)],[f2661]) ).
fof(f2667,plain,
( ~ sQ70_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f2032,f1986,f1980]) ).
fof(f2668,plain,
( ~ sQ90_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f2344,f2499,f2331]) ).
fof(f2704,plain,
( ~ sQ70_spl
| op_a != c4 ),
inference(backward_demodulation,[status(thm)],[f1981,f19]) ).
fof(f2707,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(backward_demodulation,[status(thm)],[f1981,f1562]) ).
fof(f2778,plain,
( ~ sQ81_spl
| op_b != c3 ),
inference(forward_demodulation,[status(thm)],[f2118,f18]) ).
fof(f2801,plain,
( sQ99_spl
| ~ sQ113_spl
| c4 != op_a ),
inference(backward_demodulation,[status(thm)],[f2662,f2507]) ).
fof(f2821,plain,
( ~ sQ97_spl
| mult(op_b,op_a) = e ),
inference(paramodulation,[status(thm)],[f2500,f1049]) ).
fof(f2845,plain,
( ~ sQ96_spl
| i(op_b) = mult(op_a,i(op_a)) ),
inference(paramodulation,[status(thm)],[f2458,f1272]) ).
fof(f2870,plain,
( ~ sQ99_spl
| mult(op_a,op_a) = e ),
inference(paramodulation,[status(thm)],[f2506,f1049]) ).
fof(f2886,plain,
! [X0,X1] :
( ~ sQ81_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f924]) ).
fof(f2887,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1984,f2886]) ).
fof(f2888,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = c3
| X1 = op_b
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f2887]) ).
fof(f2889,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ71_spl
| X1 = c4
| X1 = op_a
| X1 = op_b
| X0 = c4
| X0 = op_a
| X0 = X1
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1984,f2888]) ).
fof(f2943,plain,
( ~ sQ95_spl
| mult(op_a,op_b) != e ),
inference(backward_demodulation,[status(thm)],[f2455,f15]) ).
fof(f2946,plain,
( ~ sQ95_spl
| i(op_a) = mult(i(e),op_b) ),
inference(paramodulation,[status(thm)],[f2455,f1469]) ).
fof(f2948,plain,
( ~ sQ95_spl
| mult(i(op_b),e) = op_a ),
inference(paramodulation,[status(thm)],[f2455,f1115]) ).
fof(f2951,definition,
! [X0] :
( sQ114_spl
<=> ( X0 = c4
| X0 = op_a
| X0 = op_b
| mult(op_b,op_a) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f2955,plain,
( ~ sQ95_spl
| ~ sQ99_spl
| op_a = mult(i(e),op_b) ),
inference(forward_demodulation,[status(thm)],[f2506,f2946]) ).
fof(f2956,plain,
( ~ sQ95_spl
| ~ sQ99_spl
| op_a = mult(e,op_b) ),
inference(forward_demodulation,[status(thm)],[f1106,f2955]) ).
fof(f2957,plain,
( ~ sQ95_spl
| ~ sQ99_spl
| op_a = op_b ),
inference(forward_demodulation,[status(thm)],[f1046,f2956]) ).
fof(f2958,plain,
( ~ sQ95_spl
| ~ sQ99_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2957,f2157]) ).
fof(f2959,plain,
( ~ sQ95_spl
| ~ sQ99_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f2958]) ).
fof(f2964,plain,
( ~ sQ94_spl
| mult(i(op_b),op_b) = op_a ),
inference(paramodulation,[status(thm)],[f2452,f1115]) ).
fof(f2992,plain,
! [X0] :
( ~ sQ81_spl
| ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = op_b
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = X0
| mult(op_b,op_a) = op_b
| mult(op_a,op_b) != c4 ),
inference(paramodulation,[status(thm)],[f2889,f15]) ).
fof(f2994,plain,
( ~ sQ81_spl
| ~ sQ71_spl
| sQ96_spl
| sQ114_spl
| sQ94_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f2992,f2099,f2451,f2951,f2457,f1983,f2117]) ).
fof(f2999,plain,
( ~ sQ77_spl
| ~ sQ71_spl
| op_a = op_b ),
inference(forward_demodulation,[status(thm)],[f1984,f2091]) ).
fof(f3000,plain,
( ~ sQ77_spl
| ~ sQ71_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2999,f2157]) ).
fof(f3001,plain,
( ~ sQ77_spl
| ~ sQ71_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f3000]) ).
fof(f3045,plain,
( ~ sQ69_spl
| i(op_a) = mult(op_b,i(op_b)) ),
inference(paramodulation,[status(thm)],[f1978,f1272]) ).
fof(f3049,plain,
( ~ sQ69_spl
| i(op_a) = e ),
inference(forward_demodulation,[status(thm)],[f12,f3045]) ).
fof(f3050,plain,
( ~ sQ69_spl
| sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3049,f2504]) ).
fof(f3051,plain,
( ~ sQ69_spl
| sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f3050]) ).
fof(f3052,plain,
( ~ sQ81_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f2278,f2123,f2117]) ).
fof(f3056,plain,
( ~ sQ87_spl
| e = op_b ),
inference(forward_demodulation,[status(thm)],[f1049,f2482]) ).
fof(f3057,plain,
( ~ sQ87_spl
| sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3056,f2122]) ).
fof(f3058,plain,
( ~ sQ87_spl
| sQ82_spl ),
inference(contradiction_clause,[status(thm)],[f3057]) ).
fof(f3076,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| X0 = c4
| X0 = op_a
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f2132]) ).
fof(f3090,plain,
( ~ sQ81_spl
| op_b != c4 ),
inference(forward_demodulation,[status(thm)],[f2118,f19]) ).
fof(f3128,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| sQ80_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_b ),
inference(resolution,[status(thm)],[f2101,f3076]) ).
fof(f3130,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ81_spl
| sQ80_spl
| sQ87_spl
| sQ79_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f3128,f1977,f2096,f2305,f2099,f2117,f1983,f486]) ).
fof(f3134,plain,
( ~ sQ94_spl
| e = op_a ),
inference(forward_demodulation,[status(thm)],[f1049,f2964]) ).
fof(f3135,plain,
( ~ sQ94_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3134,f2017]) ).
fof(f3136,plain,
( ~ sQ94_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f3135]) ).
fof(f3139,plain,
( ~ sQ95_spl
| i(op_b) = op_a ),
inference(forward_demodulation,[status(thm)],[f13,f2948]) ).
fof(f3141,plain,
( ~ sQ95_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f2943,f2096,f2454]) ).
fof(f3159,plain,
( ~ sQ96_spl
| i(op_b) = e ),
inference(forward_demodulation,[status(thm)],[f12,f2845]) ).
fof(f3180,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f1562]) ).
fof(f3200,plain,
( ~ sQ96_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f3159,f2328,f2457]) ).
fof(f3203,plain,
( ~ sQ95_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f3139,f2331,f2454]) ).
fof(f3206,plain,
( ~ sQ97_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2821,f2454,f2499]) ).
fof(f3210,plain,
( ~ sQ90_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2345,f2454,f2331]) ).
fof(f3219,plain,
( ~ sQ79_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2324,f2454,f2096]) ).
fof(f3225,plain,
( ~ sQ81_spl
| ~ sQ36_spl
| op_b = c3
| op_b = e
| op_b = op_b ),
inference(resolution,[status(thm)],[f3180,f3090]) ).
fof(f3240,plain,
( ~ sQ81_spl
| ~ sQ36_spl
| sQ77_spl
| sQ82_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f3225,f2184,f2120,f2090,f486,f2117]) ).
fof(f3262,plain,
( ~ sQ13_spl
| e = c1 ),
inference(forward_demodulation,[status(thm)],[f1106,f185]) ).
fof(f3267,plain,
( sQ71_spl
| op_a = c4
| op_a = c2
| op_a = c1 ),
inference(resolution,[status(thm)],[f16,f1985]) ).
fof(f3284,definition,
( sQ117_spl
<=> op_a = c2 ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f3285,plain,
( ~ sQ117_spl
| op_a = c2 ),
inference(component_clause,[status(thm)],[f3284]) ).
fof(f3287,plain,
( sQ71_spl
| sQ72_spl
| sQ117_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f3267,f1980,f3284,f1986,f1983]) ).
fof(f3298,plain,
( ~ sQ31_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f884,f481,f448]) ).
fof(f3306,plain,
( sQ83_spl
| op_b = c3
| op_b = c2
| op_b = c1 ),
inference(resolution,[status(thm)],[f2125,f16]) ).
fof(f3308,definition,
( sQ118_spl
<=> op_b = c2 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f3309,plain,
( ~ sQ118_spl
| op_b = c2 ),
inference(component_clause,[status(thm)],[f3308]) ).
fof(f3310,plain,
( sQ118_spl
| op_b != c2 ),
inference(component_clause,[status(thm)],[f3308]) ).
fof(f3311,plain,
( sQ83_spl
| sQ77_spl
| sQ118_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f3306,f2117,f3308,f2090,f2123]) ).
fof(f3325,plain,
! [X0] :
( ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = e ),
inference(backward_demodulation,[status(thm)],[f449,f16]) ).
fof(f3331,plain,
( sQ71_spl
| ~ sQ31_spl
| op_a = c4
| op_a = c2
| op_a = e ),
inference(resolution,[status(thm)],[f470,f1985]) ).
fof(f3336,plain,
( sQ83_spl
| ~ sQ31_spl
| op_b = c3
| op_b = c2
| op_b = e ),
inference(resolution,[status(thm)],[f470,f2125]) ).
fof(f3348,plain,
( sQ71_spl
| ~ sQ31_spl
| sQ72_spl
| sQ117_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f3331,f2015,f3284,f1986,f448,f1983]) ).
fof(f3353,plain,
( sQ83_spl
| ~ sQ31_spl
| sQ77_spl
| sQ118_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f3336,f2120,f3308,f2090,f448,f2123]) ).
fof(f3363,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = c2
| X0 = e ),
inference(backward_demodulation,[status(thm)],[f2091,f470]) ).
fof(f3364,plain,
( ~ sQ77_spl
| c2 != op_b ),
inference(backward_demodulation,[status(thm)],[f2091,f20]) ).
fof(f3367,plain,
( ~ sQ77_spl
| op_b != c4 ),
inference(backward_demodulation,[status(thm)],[f2091,f22]) ).
fof(f3369,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2091,f3325]) ).
fof(f3372,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ77_spl
| mult(op_a,op_b) = c4
| mult(op_a,op_b) = c2
| mult(op_a,op_b) = e ),
inference(resolution,[status(thm)],[f3369,f1979]) ).
fof(f3387,definition,
( sQ119_spl
<=> mult(op_a,op_b) = c2 ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f3388,plain,
( ~ sQ119_spl
| mult(op_a,op_b) = c2 ),
inference(component_clause,[status(thm)],[f3387]) ).
fof(f3390,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ77_spl
| sQ80_spl
| sQ119_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f3372,f2096,f3387,f2099,f2090,f448,f1977]) ).
fof(f3403,plain,
( ~ sQ117_spl
| op_a != c4 ),
inference(backward_demodulation,[status(thm)],[f3285,f21]) ).
fof(f3405,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ77_spl
| ~ sQ117_spl
| X0 = c4
| X0 = op_b
| X0 = op_a
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f3285,f3363]) ).
fof(f3414,plain,
( ~ sQ117_spl
| ~ sQ31_spl
| ~ sQ77_spl
| op_a = op_b
| op_a = op_a
| op_a = e ),
inference(resolution,[status(thm)],[f3405,f3403]) ).
fof(f3434,plain,
( ~ sQ117_spl
| ~ sQ31_spl
| ~ sQ77_spl
| sQ84_spl
| sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f3414,f2015,f2020,f2155,f2090,f448,f3284]) ).
fof(f3494,definition,
( sQ120_spl
<=> mult(op_a,op_a) = op_a ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f3495,plain,
( ~ sQ120_spl
| mult(op_a,op_a) = op_a ),
inference(component_clause,[status(thm)],[f3494]) ).
fof(f3498,plain,
( ~ sQ31_spl
| ~ sQ77_spl
| ~ sQ117_spl
| sQ94_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f2453,f3405]) ).
fof(f3502,definition,
( sQ121_spl
<=> mult(op_b,op_a) = c4 ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f3503,plain,
( ~ sQ121_spl
| mult(op_b,op_a) = c4 ),
inference(component_clause,[status(thm)],[f3502]) ).
fof(f3505,plain,
( ~ sQ31_spl
| ~ sQ77_spl
| ~ sQ117_spl
| sQ94_spl
| sQ121_spl
| sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f3498,f2454,f2457,f3502,f2451,f3284,f2090,f448]) ).
fof(f3526,plain,
! [X0,X1] :
( ~ sQ31_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f1127]) ).
fof(f3527,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ sQ77_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = op_b
| X0 = X1
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2091,f3526]) ).
fof(f3528,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ sQ77_spl
| X1 = c4
| X1 = c3
| X1 = e
| X0 = c4
| X0 = op_b
| X0 = X1
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f3527]) ).
fof(f3529,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ sQ77_spl
| X1 = c4
| X1 = op_b
| X1 = e
| X0 = c4
| X0 = op_b
| X0 = X1
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2091,f3528]) ).
fof(f3535,plain,
! [X0] :
( sQ84_spl
| ~ sQ31_spl
| ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = e
| op_a = c4
| op_a = X0
| op_a = e ),
inference(resolution,[status(thm)],[f3529,f2157]) ).
fof(f3575,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ77_spl
| X0 = op_b
| op_b != op_b
| X0 = c4
| X0 = e
| X0 = c4
| X0 = X0
| X0 = e ),
inference(equality_factoring,[status(thm)],[f3529]) ).
fof(f3600,plain,
( sQ84_spl
| ~ sQ31_spl
| ~ sQ77_spl
| sQ72_spl
| sQ102_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f3535,f2015,f2599,f1986,f2090,f448,f2155]) ).
fof(f3643,definition,
! [X0] :
( sQ133_spl
<=> ( X0 = e
| X0 = c4
| X0 = op_b
| X0 = c4
| X0 = X0
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f3647,plain,
( ~ sQ31_spl
| ~ sQ77_spl
| ~ sQ86_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f3575,f3643,f2184,f2090,f448]) ).
fof(f3691,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f2091,f1562]) ).
fof(f3692,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2091,f2707]) ).
fof(f3698,plain,
! [X0] :
( ~ sQ77_spl
| X0 = c4
| X0 = op_b
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f2091,f16]) ).
fof(f3743,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ77_spl
| X0 = e
| c4 != e
| X0 = op_b
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f3691]) ).
fof(f3747,definition,
! [X0] :
( sQ139_spl
<=> ( X0 = c1
| X0 = op_b
| X0 = e ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f3748,plain,
! [X0] :
( ~ sQ139_spl
| X0 = c1
| X0 = op_b
| X0 = e ),
inference(component_clause,[status(thm)],[f3747]) ).
fof(f3751,plain,
( ~ sQ36_spl
| ~ sQ77_spl
| ~ sQ35_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f3743,f3747,f481,f2090,f486]) ).
fof(f3763,plain,
( sQ94_spl
| ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ77_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f3692,f2453]) ).
fof(f3785,plain,
( sQ94_spl
| ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ77_spl
| sQ121_spl
| sQ95_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f3763,f2457,f2454,f3502,f2090,f1980,f486,f2451]) ).
fof(f3817,plain,
( ~ sQ81_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f2778,f2090,f2117]) ).
fof(f3828,plain,
! [X0] :
( ~ sQ77_spl
| ~ sQ36_spl
| X0 = c4
| X0 = op_b
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f487,f3698]) ).
fof(f3854,plain,
( ~ sQ80_spl
| ~ sQ72_spl
| mult(op_a,op_b) = op_a ),
inference(forward_demodulation,[status(thm)],[f1987,f2100]) ).
fof(f3855,plain,
( ~ sQ80_spl
| ~ sQ72_spl
| sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3854,f2307]) ).
fof(f3856,plain,
( ~ sQ80_spl
| ~ sQ72_spl
| sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f3855]) ).
fof(f3858,plain,
( sQ79_spl
| ~ sQ78_spl
| c1 != e ),
inference(backward_demodulation,[status(thm)],[f2094,f2098]) ).
fof(f3860,plain,
( ~ sQ78_spl
| c1 != mult(op_b,op_a) ),
inference(backward_demodulation,[status(thm)],[f2094,f15]) ).
fof(f3865,plain,
( ~ sQ78_spl
| mult(i(op_a),c1) = op_b ),
inference(paramodulation,[status(thm)],[f2094,f1115]) ).
fof(f3877,plain,
! [X0] :
( ~ sQ36_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f487,f16]) ).
fof(f3914,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f1984,f3877]) ).
fof(f3915,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = op_a
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f2124,f3914]) ).
fof(f3918,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| e = op_b
| e = op_a
| e = e ),
inference(resolution,[status(thm)],[f3915,f1560]) ).
fof(f3928,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ82_spl
| sQ73_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f3918,f451,f2015,f2120,f2123,f1983,f486]) ).
fof(f3942,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ87_spl
| mult(op_a,op_b) = op_b
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| c1 != op_a ),
inference(paramodulation,[status(thm)],[f3915,f2307]) ).
fof(f3943,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ69_spl
| sQ87_spl
| sQ79_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f3942,f1980,f2096,f2305,f1977,f2123,f1983,f486]) ).
fof(f3956,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e
| mult(op_a,op_b) != c1 ),
inference(paramodulation,[status(thm)],[f3915,f15]) ).
fof(f3957,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ94_spl
| sQ96_spl
| sQ95_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f3956,f2093,f2454,f2457,f2451,f2123,f1983,f486]) ).
fof(f3958,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ78_spl
| mult(op_a,op_b) = op_b
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e ),
inference(resolution,[status(thm)],[f2095,f3915]) ).
fof(f3959,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ78_spl
| mult(op_a,op_b) = op_b
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| c1 != c1 ),
inference(paramodulation,[status(thm)],[f3915,f2095]) ).
fof(f3960,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ78_spl
| sQ69_spl
| sQ87_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f3958,f2096,f2305,f1977,f2093,f2123,f1983,f486]) ).
fof(f3961,plain,
( ~ sQ36_spl
| ~ sQ71_spl
| ~ sQ83_spl
| sQ78_spl
| sQ69_spl
| sQ87_spl
| sQ79_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f3959,f39,f2096,f2305,f1977,f2093,f2123,f1983,f486]) ).
fof(f3969,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| op_b = op_b
| op_b = e
| op_b = c1 ),
inference(resolution,[status(thm)],[f3691,f3367]) ).
fof(f3975,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| sQ86_spl
| sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f3969,f2117,f2120,f2184,f486,f2090]) ).
fof(f4002,plain,
! [X0] :
( ~ sQ77_spl
| ~ sQ36_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = op_b
| X0 = e
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f1987,f3828]) ).
fof(f4027,plain,
( ~ sQ78_spl
| c1 != mult(op_b,op_a) ),
inference(backward_demodulation,[status(thm)],[f2094,f15]) ).
fof(f4036,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| ~ sQ72_spl
| ~ sQ78_spl
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f3860,f4002]) ).
fof(f4037,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| ~ sQ72_spl
| ~ sQ78_spl
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = e
| c1 != c1 ),
inference(paramodulation,[status(thm)],[f4002,f3860]) ).
fof(f4038,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| ~ sQ72_spl
| ~ sQ78_spl
| sQ96_spl
| sQ94_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f4036,f2454,f2451,f2457,f2093,f1986,f486,f2090]) ).
fof(f4039,plain,
( ~ sQ77_spl
| ~ sQ36_spl
| ~ sQ72_spl
| ~ sQ78_spl
| sQ96_spl
| sQ94_spl
| sQ95_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f4037,f39,f2454,f2451,f2457,f2093,f1986,f486,f2090]) ).
fof(f4050,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f3877]) ).
fof(f4117,plain,
( sQ95_spl
| ~ sQ121_spl
| c4 != e ),
inference(backward_demodulation,[status(thm)],[f3503,f2456]) ).
fof(f4118,plain,
( sQ96_spl
| ~ sQ121_spl
| c4 != op_a ),
inference(backward_demodulation,[status(thm)],[f3503,f2459]) ).
fof(f4119,plain,
( sQ94_spl
| ~ sQ121_spl
| c4 != op_b ),
inference(backward_demodulation,[status(thm)],[f3503,f2453]) ).
fof(f4159,plain,
( sQ79_spl
| ~ sQ80_spl
| c4 != e ),
inference(forward_demodulation,[status(thm)],[f2100,f2098]) ).
fof(f4166,definition,
( sQ141_spl
<=> mult(op_a,op_a) = c4 ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f4167,plain,
( ~ sQ141_spl
| mult(op_a,op_a) = c4 ),
inference(component_clause,[status(thm)],[f4166]) ).
fof(f4177,plain,
! [X0] :
( ~ sQ75_spl
| ~ sQ70_spl
| X0 = op_a
| X0 = op_a
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f1981,f2025]) ).
fof(f4178,plain,
! [X0] :
( ~ sQ75_spl
| ~ sQ70_spl
| X0 = op_a
| X0 = e ),
inference(duplicate_literals_removal,[status(thm)],[f4177]) ).
fof(f4207,plain,
( ~ sQ141_spl
| ~ sQ99_spl
| e = c4 ),
inference(forward_demodulation,[status(thm)],[f2870,f4167]) ).
fof(f4208,plain,
( ~ sQ141_spl
| ~ sQ99_spl
| sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4207,f483]) ).
fof(f4209,plain,
( ~ sQ141_spl
| ~ sQ99_spl
| sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f4208]) ).
fof(f4210,plain,
( ~ sQ120_spl
| ~ sQ99_spl
| e = op_a ),
inference(forward_demodulation,[status(thm)],[f2870,f3495]) ).
fof(f4211,plain,
( ~ sQ120_spl
| ~ sQ99_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4210,f2017]) ).
fof(f4212,plain,
( ~ sQ120_spl
| ~ sQ99_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f4211]) ).
fof(f4365,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2124,f4050]) ).
fof(f4368,plain,
( sQ77_spl
| ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| op_b = op_b
| op_b = e
| op_b = op_a ),
inference(resolution,[status(thm)],[f4365,f2092]) ).
fof(f4381,plain,
( sQ77_spl
| ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ86_spl
| sQ82_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f4368,f2155,f2120,f2184,f2123,f1980,f486,f2090]) ).
fof(f4389,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ97_spl
| i(op_a) = op_b
| i(op_a) = e
| i(op_a) = op_a
| c3 != op_b ),
inference(paramodulation,[status(thm)],[f4365,f2501]) ).
fof(f4390,definition,
( sQ145_spl
<=> i(op_a) = c3 ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f4391,plain,
( ~ sQ145_spl
| i(op_a) = c3 ),
inference(component_clause,[status(thm)],[f4390]) ).
fof(f4392,plain,
( sQ145_spl
| i(op_a) != c3 ),
inference(component_clause,[status(thm)],[f4390]) ).
fof(f4394,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ97_spl
| sQ98_spl
| sQ99_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f4389,f2090,f2505,f2502,f2499,f2123,f1980,f486]) ).
fof(f4406,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ99_spl
| i(op_a) = op_b
| i(op_a) = e
| i(op_a) = op_a
| c3 != op_a ),
inference(paramodulation,[status(thm)],[f4365,f2507]) ).
fof(f4407,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ97_spl
| sQ98_spl
| sQ99_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f4406,f1983,f2505,f2502,f2499,f2123,f1980,f486]) ).
fof(f4411,plain,
( sQ98_spl
| ~ sQ145_spl
| c3 != e ),
inference(backward_demodulation,[status(thm)],[f4391,f2504]) ).
fof(f4451,definition,
( sQ148_spl
<=> i(c3) = e ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f4452,plain,
( ~ sQ148_spl
| i(c3) = e ),
inference(component_clause,[status(thm)],[f4451]) ).
fof(f4462,plain,
! [X0] :
( ~ sQ42_spl
| ~ sQ83_spl
| X0 = c1
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2124,f819]) ).
fof(f4640,plain,
( sQ90_spl
| ~ sQ75_spl
| ~ sQ70_spl
| i(op_b) = e ),
inference(resolution,[status(thm)],[f4178,f2333]) ).
fof(f4642,plain,
( ~ sQ70_spl
| ~ sQ75_spl
| c4 = e ),
inference(resolution,[status(thm)],[f4178,f2704]) ).
fof(f4643,plain,
( sQ84_spl
| ~ sQ75_spl
| ~ sQ70_spl
| op_b = e ),
inference(resolution,[status(thm)],[f4178,f2157]) ).
fof(f4650,plain,
( sQ90_spl
| ~ sQ75_spl
| ~ sQ70_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f4640,f2328,f1980,f2024,f2331]) ).
fof(f4651,plain,
( ~ sQ70_spl
| ~ sQ75_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f4642,f481,f2024,f1980]) ).
fof(f4652,plain,
( sQ84_spl
| ~ sQ75_spl
| ~ sQ70_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f4643,f2120,f1980,f2024,f2155]) ).
fof(f4689,plain,
( ~ sQ148_spl
| ~ sQ77_spl
| i(op_b) = e ),
inference(forward_demodulation,[status(thm)],[f2091,f4452]) ).
fof(f4690,plain,
( ~ sQ148_spl
| ~ sQ77_spl
| sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4689,f2330]) ).
fof(f4691,plain,
( ~ sQ148_spl
| ~ sQ77_spl
| sQ89_spl ),
inference(contradiction_clause,[status(thm)],[f4690]) ).
fof(f4733,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = c3
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2124,f2196]) ).
fof(f4785,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ79_spl
| mult(op_a,op_b) = op_b
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_a
| c3 != e ),
inference(paramodulation,[status(thm)],[f4733,f2098]) ).
fof(f4786,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| sQ79_spl
| sQ87_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f4785,f454,f2305,f2096,f1977,f2123,f1980,f486]) ).
fof(f4790,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| mult(op_a,op_b) = c3
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_a ),
inference(resolution,[status(thm)],[f1979,f4733]) ).
fof(f4792,definition,
( sQ151_spl
<=> mult(op_a,op_b) = c3 ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f4793,plain,
( ~ sQ151_spl
| mult(op_a,op_b) = c3 ),
inference(component_clause,[status(thm)],[f4792]) ).
fof(f4794,plain,
( sQ151_spl
| mult(op_a,op_b) != c3 ),
inference(component_clause,[status(thm)],[f4792]) ).
fof(f4795,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| sQ151_spl
| sQ79_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f4790,f2305,f2096,f4792,f1977,f2123,f1980,f486]) ).
fof(f4801,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ94_spl
| mult(op_b,op_a) = c3
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f2453,f4733]) ).
fof(f4803,definition,
( sQ152_spl
<=> mult(op_b,op_a) = c3 ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f4804,plain,
( ~ sQ152_spl
| mult(op_b,op_a) = c3 ),
inference(component_clause,[status(thm)],[f4803]) ).
fof(f4805,plain,
( sQ152_spl
| mult(op_b,op_a) != c3 ),
inference(component_clause,[status(thm)],[f4803]) ).
fof(f4806,plain,
( ~ sQ36_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ94_spl
| sQ152_spl
| sQ95_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f4801,f2457,f2454,f4803,f2451,f2123,f1980,f486]) ).
fof(f4840,plain,
( sQ69_spl
| ~ sQ151_spl
| c3 != op_b ),
inference(backward_demodulation,[status(thm)],[f4793,f1979]) ).
fof(f4841,plain,
( sQ87_spl
| ~ sQ151_spl
| c3 != op_a ),
inference(backward_demodulation,[status(thm)],[f4793,f2307]) ).
fof(f4842,plain,
( sQ79_spl
| ~ sQ151_spl
| c3 != e ),
inference(backward_demodulation,[status(thm)],[f4793,f2098]) ).
fof(f4843,plain,
( ~ sQ151_spl
| c3 != mult(op_b,op_a) ),
inference(backward_demodulation,[status(thm)],[f4793,f15]) ).
fof(f4845,plain,
( ~ sQ151_spl
| i(op_b) = mult(i(c3),op_a) ),
inference(paramodulation,[status(thm)],[f4793,f1469]) ).
fof(f4850,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| op_b = mult(i(c3),op_a) ),
inference(forward_demodulation,[status(thm)],[f2326,f4845]) ).
fof(f4865,plain,
( ~ sQ151_spl
| ~ sQ152_spl
| c3 != c3 ),
inference(forward_demodulation,[status(thm)],[f4804,f4843]) ).
fof(f4866,plain,
( ~ sQ151_spl
| ~ sQ152_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4865]) ).
fof(f4867,plain,
( ~ sQ151_spl
| ~ sQ152_spl ),
inference(contradiction_clause,[status(thm)],[f4866]) ).
fof(f4868,plain,
! [X0] :
( ~ sQ83_spl
| X0 = op_b
| X0 = c3
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f2124,f16]) ).
fof(f4869,plain,
( ~ sQ83_spl
| c2 != op_b ),
inference(forward_demodulation,[status(thm)],[f2124,f21]) ).
fof(f4898,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = c3
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2124,f3325]) ).
fof(f4900,plain,
( ~ sQ71_spl
| c2 != op_a ),
inference(backward_demodulation,[status(thm)],[f1984,f20]) ).
fof(f4903,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ71_spl
| X0 = op_b
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f1984,f4868]) ).
fof(f4905,plain,
( sQ36_spl
| ~ sQ83_spl
| ~ sQ71_spl
| e = op_b
| e = op_a
| e = c1 ),
inference(resolution,[status(thm)],[f4903,f488]) ).
fof(f4906,plain,
( ~ sQ83_spl
| ~ sQ71_spl
| op_b = op_b
| op_b = op_a
| op_b = c1 ),
inference(resolution,[status(thm)],[f4903,f4869]) ).
fof(f4915,plain,
( sQ36_spl
| ~ sQ83_spl
| ~ sQ71_spl
| sQ82_spl
| sQ73_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f4905,f448,f2015,f2120,f1983,f2123,f486]) ).
fof(f4916,plain,
( ~ sQ83_spl
| ~ sQ71_spl
| sQ86_spl
| sQ84_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f4906,f2117,f2155,f2184,f1983,f2123]) ).
fof(f4930,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ83_spl
| ~ sQ71_spl
| X0 = op_b
| X0 = op_a
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f1984,f4898]) ).
fof(f4959,plain,
( sQ145_spl
| ~ sQ71_spl
| i(op_a) != op_a ),
inference(forward_demodulation,[status(thm)],[f1984,f4392]) ).
fof(f4962,definition,
( sQ154_spl
<=> i(op_a) = c2 ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f4963,plain,
( ~ sQ154_spl
| i(op_a) = c2 ),
inference(component_clause,[status(thm)],[f4962]) ).
fof(f4964,plain,
( sQ154_spl
| i(op_a) != c2 ),
inference(component_clause,[status(thm)],[f4962]) ).
fof(f4974,plain,
( ~ sQ99_spl
| sQ145_spl
| ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2506,f4959]) ).
fof(f4975,plain,
( ~ sQ99_spl
| sQ145_spl
| ~ sQ71_spl ),
inference(contradiction_clause,[status(thm)],[f4974]) ).
fof(f4986,plain,
( ~ sQ31_spl
| ~ sQ83_spl
| ~ sQ71_spl
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e
| mult(op_a,op_b) != c2 ),
inference(paramodulation,[status(thm)],[f4930,f15]) ).
fof(f4987,plain,
( ~ sQ31_spl
| ~ sQ83_spl
| ~ sQ71_spl
| sQ94_spl
| sQ96_spl
| sQ95_spl
| ~ sQ119_spl ),
inference(split_clause,[status(thm)],[f4986,f3387,f2454,f2457,f2451,f1983,f2123,f448]) ).
fof(f4990,plain,
( ~ sQ145_spl
| ~ sQ71_spl
| i(op_a) = op_a ),
inference(forward_demodulation,[status(thm)],[f1984,f4391]) ).
fof(f5010,plain,
( sQ97_spl
| ~ sQ154_spl
| c2 != op_b ),
inference(backward_demodulation,[status(thm)],[f4963,f2501]) ).
fof(f5020,plain,
( ~ sQ154_spl
| i(c2) = op_a ),
inference(paramodulation,[status(thm)],[f4963,f1087]) ).
fof(f5039,plain,
( sQ99_spl
| ~ sQ154_spl
| c2 != op_a ),
inference(forward_demodulation,[status(thm)],[f4963,f2507]) ).
fof(f5052,definition,
( sQ156_spl
<=> i(c2) = e ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f5053,plain,
( ~ sQ156_spl
| i(c2) = e ),
inference(component_clause,[status(thm)],[f5052]) ).
fof(f5055,definition,
( sQ157_spl
<=> i(c2) = op_a ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f5056,plain,
( ~ sQ157_spl
| i(c2) = op_a ),
inference(component_clause,[status(thm)],[f5055]) ).
fof(f5058,definition,
( sQ158_spl
<=> i(c2) = op_b ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f5059,plain,
( ~ sQ158_spl
| i(c2) = op_b ),
inference(component_clause,[status(thm)],[f5058]) ).
fof(f5070,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f459]) ).
fof(f5081,plain,
! [X0] :
( ~ sQ139_spl
| ~ sQ31_spl
| X0 = e
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f3748]) ).
fof(f5082,plain,
! [X0] :
( ~ sQ139_spl
| ~ sQ31_spl
| X0 = op_b
| X0 = e ),
inference(duplicate_literals_removal,[status(thm)],[f5081]) ).
fof(f5086,plain,
! [X0] :
( ~ sQ38_spl
| ~ sQ71_spl
| X0 = c1
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1984,f518]) ).
fof(f5087,plain,
! [X0] :
( ~ sQ38_spl
| ~ sQ71_spl
| ~ sQ31_spl
| X0 = e
| X0 = e
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f449,f5086]) ).
fof(f5088,plain,
! [X0] :
( ~ sQ38_spl
| ~ sQ71_spl
| ~ sQ31_spl
| X0 = e
| X0 = op_a ),
inference(duplicate_literals_removal,[status(thm)],[f5087]) ).
fof(f5105,plain,
! [X0] :
( ~ sQ101_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = op_b
| op_a = X0 ),
inference(forward_demodulation,[status(thm)],[f2124,f2647]) ).
fof(f5106,plain,
! [X0] :
( ~ sQ101_spl
| ~ sQ83_spl
| X0 = op_b
| op_a = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5105]) ).
fof(f5118,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ31_spl
| X0 = c3
| X0 = e
| e = X0 ),
inference(forward_demodulation,[status(thm)],[f449,f1995]) ).
fof(f5119,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ31_spl
| ~ sQ71_spl
| X0 = op_a
| X0 = e
| e = X0 ),
inference(forward_demodulation,[status(thm)],[f1984,f5118]) ).
fof(f5120,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ31_spl
| ~ sQ71_spl
| X0 = op_a
| e = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5119]) ).
fof(f5130,plain,
( ~ sQ158_spl
| ~ sQ154_spl
| op_a = op_b ),
inference(forward_demodulation,[status(thm)],[f5020,f5059]) ).
fof(f5131,plain,
( ~ sQ158_spl
| ~ sQ154_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5130,f2157]) ).
fof(f5132,plain,
( ~ sQ158_spl
| ~ sQ154_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f5131]) ).
fof(f5133,plain,
( ~ sQ156_spl
| ~ sQ154_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f5020,f5053]) ).
fof(f5134,plain,
( ~ sQ156_spl
| ~ sQ154_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5133,f2017]) ).
fof(f5135,plain,
( ~ sQ156_spl
| ~ sQ154_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f5134]) ).
fof(f5140,definition,
( sQ159_spl
<=> mult(op_b,op_a) = c2 ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f5141,plain,
( ~ sQ159_spl
| mult(op_b,op_a) = c2 ),
inference(component_clause,[status(thm)],[f5140]) ).
fof(f5152,plain,
( ~ sQ31_spl
| ~ sQ83_spl
| ~ sQ71_spl
| sQ69_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = c2
| mult(op_a,op_b) = e ),
inference(resolution,[status(thm)],[f1979,f4930]) ).
fof(f5154,plain,
( ~ sQ31_spl
| ~ sQ83_spl
| ~ sQ71_spl
| sQ69_spl
| sQ87_spl
| sQ119_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f5152,f2096,f3387,f2305,f1977,f1983,f2123,f448]) ).
fof(f5157,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f1984,f470]) ).
fof(f5183,plain,
! [X0] :
( ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f16]) ).
fof(f5186,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| op_a = c4
| op_a = op_a
| op_a = e ),
inference(resolution,[status(thm)],[f5157,f4900]) ).
fof(f5188,plain,
( sQ96_spl
| ~ sQ31_spl
| ~ sQ71_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f5157,f2459]) ).
fof(f5200,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| sQ72_spl
| sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f5186,f2015,f2020,f1986,f448,f1983]) ).
fof(f5202,plain,
( sQ96_spl
| ~ sQ31_spl
| ~ sQ71_spl
| sQ121_spl
| sQ159_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f5188,f2454,f5140,f3502,f1983,f448,f2457]) ).
fof(f5336,plain,
! [X0] :
( ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f16]) ).
fof(f5537,plain,
! [X0] :
( ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f16]) ).
fof(f5677,plain,
( ~ sQ71_spl
| c2 != op_a ),
inference(backward_demodulation,[status(thm)],[f1984,f20]) ).
fof(f5797,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(backward_demodulation,[status(thm)],[f2118,f1562]) ).
fof(f5819,plain,
( sQ145_spl
| i(op_a) = c4
| i(op_a) = c2
| i(op_a) = c1 ),
inference(resolution,[status(thm)],[f16,f4392]) ).
fof(f5829,definition,
( sQ160_spl
<=> i(op_a) = c1 ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f5830,plain,
( ~ sQ160_spl
| i(op_a) = c1 ),
inference(component_clause,[status(thm)],[f5829]) ).
fof(f5832,plain,
( sQ145_spl
| sQ113_spl
| sQ154_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f5819,f5829,f4962,f2661,f4390]) ).
fof(f5866,plain,
( sQ36_spl
| ~ sQ71_spl
| e = c4
| e = op_a
| e = c1 ),
inference(resolution,[status(thm)],[f5336,f488]) ).
fof(f5877,plain,
( sQ36_spl
| ~ sQ71_spl
| sQ35_spl
| sQ73_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f5866,f448,f2015,f481,f1983,f486]) ).
fof(f5889,plain,
( ~ sQ71_spl
| op_a = c4
| op_a = op_a
| op_a = c1 ),
inference(resolution,[status(thm)],[f5677,f5336]) ).
fof(f5891,plain,
( ~ sQ71_spl
| sQ72_spl
| sQ74_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f5889,f1980,f2020,f1986,f1983]) ).
fof(f6044,plain,
! [X0] :
( ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f16]) ).
fof(f6158,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(backward_demodulation,[status(thm)],[f1987,f5797]) ).
fof(f6161,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f1562]) ).
fof(f6162,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1987,f6161]) ).
fof(f6202,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ87_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_b
| c3 != op_a ),
inference(paramodulation,[status(thm)],[f6162,f2307]) ).
fof(f6203,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ87_spl
| sQ79_spl
| sQ69_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f6202,f1983,f1977,f2096,f2305,f1986,f2117,f486]) ).
fof(f6242,plain,
! [X0] :
( ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f16]) ).
fof(f6373,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ79_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_b
| c3 != e ),
inference(paramodulation,[status(thm)],[f6158,f2098]) ).
fof(f6374,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ87_spl
| sQ79_spl
| sQ69_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f6373,f454,f1977,f2096,f2305,f1986,f2117,f486]) ).
fof(f6516,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ31_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f449,f6242]) ).
fof(f6517,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ118_spl
| X0 = c4
| X0 = op_a
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f3309,f6516]) ).
fof(f6519,plain,
( sQ94_spl
| ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ118_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f6517,f2453]) ).
fof(f6529,plain,
( sQ84_spl
| ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ118_spl
| op_b = c4
| op_b = op_b
| op_b = e ),
inference(resolution,[status(thm)],[f6517,f2157]) ).
fof(f6551,plain,
( sQ94_spl
| ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ118_spl
| sQ121_spl
| sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f6519,f2454,f2457,f3502,f3308,f448,f1983,f2451]) ).
fof(f6561,plain,
( sQ84_spl
| ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ118_spl
| sQ83_spl
| sQ86_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f6529,f2120,f2184,f2123,f3308,f448,f1983,f2155]) ).
fof(f6679,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ152_spl
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_b ),
inference(resolution,[status(thm)],[f4805,f6158]) ).
fof(f6681,plain,
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ152_spl
| sQ96_spl
| sQ95_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f6679,f2451,f2454,f2457,f4803,f1986,f2117,f486]) ).
fof(f6688,plain,
( sQ152_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = c1 ),
inference(resolution,[status(thm)],[f16,f4805]) ).
fof(f6700,definition,
( sQ162_spl
<=> mult(op_b,op_a) = c1 ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f6701,plain,
( ~ sQ162_spl
| mult(op_b,op_a) = c1 ),
inference(component_clause,[status(thm)],[f6700]) ).
fof(f6703,plain,
( sQ152_spl
| sQ121_spl
| sQ159_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f6688,f6700,f5140,f3502,f4803]) ).
fof(f6732,plain,
! [X0] :
( ~ sQ71_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1984,f16]) ).
fof(f6871,plain,
( ~ sQ113_spl
| i(c4) = op_a ),
inference(paramodulation,[status(thm)],[f2662,f1087]) ).
fof(f6874,plain,
( sQ97_spl
| ~ sQ113_spl
| c4 != op_b ),
inference(forward_demodulation,[status(thm)],[f2662,f2501]) ).
fof(f6893,definition,
( sQ163_spl
<=> i(c4) = e ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f6894,plain,
( ~ sQ163_spl
| i(c4) = e ),
inference(component_clause,[status(thm)],[f6893]) ).
fof(f7028,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| X0 = c4
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f1562]) ).
fof(f7035,plain,
! [X0] :
( ~ sQ81_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f16]) ).
fof(f7072,plain,
( ~ sQ145_spl
| ~ sQ71_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f4990,f2505,f1983,f4390]) ).
fof(f7074,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = e ),
inference(duplicate_literals_removal,[status(thm)],[f5070]) ).
fof(f7225,plain,
( sQ94_spl
| ~ sQ139_spl
| ~ sQ31_spl
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f5082,f2453]) ).
fof(f7227,plain,
( sQ84_spl
| ~ sQ139_spl
| ~ sQ31_spl
| op_a = e ),
inference(resolution,[status(thm)],[f5082,f2157]) ).
fof(f7245,plain,
( sQ94_spl
| ~ sQ139_spl
| ~ sQ31_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f7225,f2454,f448,f3747,f2451]) ).
fof(f7247,plain,
( sQ84_spl
| ~ sQ139_spl
| ~ sQ31_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f7227,f2015,f448,f3747,f2155]) ).
fof(f7256,plain,
( ~ sQ71_spl
| ~ sQ38_spl
| ~ sQ31_spl
| c4 = e ),
inference(resolution,[status(thm)],[f5088,f2134]) ).
fof(f7271,plain,
( ~ sQ71_spl
| ~ sQ38_spl
| ~ sQ31_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f7256,f481,f448,f517,f1983]) ).
fof(f7281,plain,
( ~ sQ71_spl
| ~ sQ48_spl
| ~ sQ31_spl
| e = c4 ),
inference(resolution,[status(thm)],[f5120,f2134]) ).
fof(f7296,plain,
( ~ sQ71_spl
| ~ sQ48_spl
| ~ sQ31_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f7281,f481,f448,f1319,f1983]) ).
fof(f7488,plain,
( sQ154_spl
| ~ sQ99_spl
| op_a != c2 ),
inference(forward_demodulation,[status(thm)],[f2506,f4964]) ).
fof(f7514,plain,
( ~ sQ34_spl
| ~ sQ31_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f7074,f491,f448,f458]) ).
fof(f7520,plain,
( ~ sQ145_spl
| ~ sQ99_spl
| op_a = c3 ),
inference(forward_demodulation,[status(thm)],[f2506,f4391]) ).
fof(f7608,plain,
( sQ154_spl
| ~ sQ99_spl
| op_a = c4
| op_a = c3
| op_a = c1 ),
inference(resolution,[status(thm)],[f7488,f16]) ).
fof(f7610,plain,
( sQ154_spl
| ~ sQ99_spl
| sQ72_spl
| sQ71_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f7608,f1980,f1983,f1986,f2505,f4962]) ).
fof(f7647,definition,
! [X0] :
( sQ166_spl
<=> ( X0 = op_a
| X0 = c2
| X0 = e
| X0 = op_b ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f7728,plain,
( sQ95_spl
| ~ sQ152_spl
| c3 != e ),
inference(backward_demodulation,[status(thm)],[f4804,f2456]) ).
fof(f7751,plain,
( ~ sQ160_spl
| ~ sQ99_spl
| op_a = c1 ),
inference(forward_demodulation,[status(thm)],[f2506,f5830]) ).
fof(f7752,plain,
( ~ sQ160_spl
| ~ sQ99_spl
| ~ sQ81_spl
| op_a = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f7751]) ).
fof(f7753,plain,
( ~ sQ160_spl
| ~ sQ99_spl
| ~ sQ81_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7752,f2157]) ).
fof(f7754,plain,
( ~ sQ160_spl
| ~ sQ99_spl
| ~ sQ81_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f7753]) ).
fof(f7756,plain,
( ~ sQ145_spl
| ~ sQ99_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f7520,f1983,f2505,f4390]) ).
fof(f7759,plain,
( ~ sQ154_spl
| ~ sQ99_spl
| op_a = c2 ),
inference(forward_demodulation,[status(thm)],[f2506,f4963]) ).
fof(f7760,plain,
( ~ sQ154_spl
| ~ sQ99_spl
| ~ sQ36_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f487,f7759]) ).
fof(f7761,plain,
( ~ sQ154_spl
| ~ sQ99_spl
| ~ sQ36_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7760,f2017]) ).
fof(f7762,plain,
( ~ sQ154_spl
| ~ sQ99_spl
| ~ sQ36_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f7761]) ).
fof(f7764,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = c3
| X0 = e
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f1987,f7028]) ).
fof(f7765,plain,
( sQ151_spl
| ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_b ),
inference(resolution,[status(thm)],[f7764,f4794]) ).
fof(f7776,plain,
( sQ151_spl
| ~ sQ36_spl
| ~ sQ81_spl
| ~ sQ72_spl
| sQ87_spl
| sQ79_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f7765,f1977,f2096,f2305,f1986,f2117,f486,f4792]) ).
fof(f7783,plain,
( ~ sQ42_spl
| ~ sQ83_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f4462,f3747,f2123,f818]) ).
fof(f7785,plain,
( sQ97_spl
| ~ sQ113_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f6874,f2123,f2661,f2499]) ).
fof(f7790,plain,
( sQ151_spl
| mult(op_a,op_b) = c4
| mult(op_a,op_b) = c2
| mult(op_a,op_b) = c1 ),
inference(resolution,[status(thm)],[f16,f4794]) ).
fof(f7809,plain,
( sQ151_spl
| sQ80_spl
| sQ119_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f7790,f2093,f3387,f2099,f4792]) ).
fof(f7827,plain,
! [X0] :
( ~ sQ31_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = e ),
inference(backward_demodulation,[status(thm)],[f449,f16]) ).
fof(f7868,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ117_spl
| X0 = c4
| X0 = c3
| X0 = op_a
| X0 = e ),
inference(backward_demodulation,[status(thm)],[f3285,f5183]) ).
fof(f7870,plain,
( ~ sQ117_spl
| op_a != c4 ),
inference(backward_demodulation,[status(thm)],[f3285,f21]) ).
fof(f7872,plain,
( ~ sQ118_spl
| ~ sQ117_spl
| op_b = op_a ),
inference(forward_demodulation,[status(thm)],[f3285,f3309]) ).
fof(f7873,plain,
( ~ sQ118_spl
| ~ sQ117_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7872,f2157]) ).
fof(f7874,plain,
( ~ sQ118_spl
| ~ sQ117_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f7873]) ).
fof(f7875,plain,
( sQ99_spl
| ~ sQ113_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f2801,f1986,f2661,f2505]) ).
fof(f7885,plain,
( sQ97_spl
| ~ sQ154_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f5010,f3308,f4962,f2499]) ).
fof(f7890,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ118_spl
| X0 = c4
| X0 = c3
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f3309,f7827]) ).
fof(f7892,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ118_spl
| mult(op_a,op_b) = c4
| mult(op_a,op_b) = c3
| mult(op_a,op_b) = e ),
inference(resolution,[status(thm)],[f7890,f1979]) ).
fof(f7900,plain,
( sQ77_spl
| ~ sQ31_spl
| ~ sQ118_spl
| op_b = c4
| op_b = op_b
| op_b = e ),
inference(resolution,[status(thm)],[f7890,f2092]) ).
fof(f7915,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ118_spl
| X0 = c3
| op_b != c3
| X0 = c4
| X0 = e ),
inference(equality_factoring,[status(thm)],[f7890]) ).
fof(f7917,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ118_spl
| X0 = c4
| op_b != c4
| X0 = c3
| X0 = e ),
inference(equality_factoring,[status(thm)],[f7890]) ).
fof(f7920,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ118_spl
| sQ80_spl
| sQ151_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f7892,f2096,f4792,f2099,f3308,f448,f1977]) ).
fof(f7928,plain,
( sQ77_spl
| ~ sQ31_spl
| ~ sQ118_spl
| sQ83_spl
| sQ86_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f7900,f2120,f2184,f2123,f3308,f448,f2090]) ).
fof(f7935,plain,
( ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ77_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f7915,f491,f2090,f3308,f448]) ).
fof(f7937,plain,
( ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ83_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f7917,f491,f2123,f3308,f448]) ).
fof(f7944,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ118_spl
| X0 = c4
| X0 = c3
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f3309,f5183]) ).
fof(f7945,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = c3
| X0 = op_b
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f1987,f7944]) ).
fof(f7948,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ72_spl
| mult(op_a,op_b) = op_a
| mult(op_a,op_b) = c3
| mult(op_a,op_b) = e ),
inference(resolution,[status(thm)],[f7945,f1979]) ).
fof(f7949,plain,
( sQ84_spl
| ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ72_spl
| op_a = op_a
| op_a = c3
| op_a = e ),
inference(resolution,[status(thm)],[f7945,f2157]) ).
fof(f7975,plain,
( sQ69_spl
| ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ72_spl
| sQ87_spl
| sQ151_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f7948,f2096,f4792,f2305,f1986,f3308,f448,f1977]) ).
fof(f7976,plain,
( sQ84_spl
| ~ sQ31_spl
| ~ sQ118_spl
| ~ sQ72_spl
| sQ74_spl
| sQ71_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f7949,f2015,f1983,f2020,f1986,f3308,f448,f2155]) ).
fof(f7987,definition,
! [X0] :
( sQ167_spl
<=> ( X0 = e
| X0 = op_a
| X0 = c3 ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f7988,plain,
! [X0] :
( ~ sQ167_spl
| X0 = e
| X0 = op_a
| X0 = c3 ),
inference(component_clause,[status(thm)],[f7987]) ).
fof(f8160,plain,
( sQ89_spl
| ~ sQ104_spl
| c4 != e ),
inference(backward_demodulation,[status(thm)],[f2607,f2330]) ).
fof(f8171,plain,
( ~ sQ104_spl
| i(c4) = op_b ),
inference(paramodulation,[status(thm)],[f2607,f1087]) ).
fof(f8174,plain,
( ~ sQ104_spl
| ~ sQ113_spl
| op_a = op_b ),
inference(forward_demodulation,[status(thm)],[f6871,f8171]) ).
fof(f8175,plain,
( ~ sQ104_spl
| ~ sQ113_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8174,f2157]) ).
fof(f8176,plain,
( ~ sQ104_spl
| ~ sQ113_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f8175]) ).
fof(f8185,plain,
( ~ sQ163_spl
| ~ sQ113_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f6871,f6894]) ).
fof(f8186,plain,
( ~ sQ163_spl
| ~ sQ113_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8185,f2017]) ).
fof(f8187,plain,
( ~ sQ163_spl
| ~ sQ113_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f8186]) ).
fof(f8217,plain,
( ~ sQ80_spl
| c4 != mult(op_b,op_a) ),
inference(backward_demodulation,[status(thm)],[f2100,f15]) ).
fof(f8258,plain,
( ~ sQ159_spl
| ~ sQ118_spl
| mult(op_b,op_a) = op_b ),
inference(forward_demodulation,[status(thm)],[f3309,f5141]) ).
fof(f8259,plain,
( ~ sQ159_spl
| ~ sQ118_spl
| sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8258,f2453]) ).
fof(f8260,plain,
( ~ sQ159_spl
| ~ sQ118_spl
| sQ94_spl ),
inference(contradiction_clause,[status(thm)],[f8259]) ).
fof(f8266,plain,
( ~ sQ13_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f3262,f448,f184]) ).
fof(f8276,plain,
( sQ89_spl
| ~ sQ104_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f8160,f481,f2606,f2328]) ).
fof(f8305,plain,
( sQ98_spl
| ~ sQ145_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f4411,f454,f4390,f2502]) ).
fof(f8361,plain,
! [X0] :
( ~ sQ70_spl
| X0 = c4
| X0 = c3
| X0 = c2
| X0 = op_a ),
inference(backward_demodulation,[status(thm)],[f1981,f16]) ).
fof(f8365,plain,
( ~ sQ70_spl
| op_a != c2 ),
inference(backward_demodulation,[status(thm)],[f1981,f17]) ).
fof(f8366,plain,
( ~ sQ70_spl
| op_a != c4 ),
inference(backward_demodulation,[status(thm)],[f1981,f19]) ).
fof(f8374,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ70_spl
| X0 = c4
| X0 = e
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f1373]) ).
fof(f8375,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ118_spl
| X0 = c4
| X0 = e
| X0 = op_b
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f3309,f8374]) ).
fof(f8376,plain,
( sQ94_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ118_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f8375,f2453]) ).
fof(f8382,plain,
( ~ sQ80_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ118_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f8375,f8217]) ).
fof(f8396,plain,
( sQ94_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ118_spl
| sQ121_spl
| sQ95_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f8376,f2457,f2454,f3502,f3308,f1980,f454,f2451]) ).
fof(f8402,plain,
( ~ sQ80_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ118_spl
| sQ95_spl
| sQ94_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f8382,f2457,f2451,f2454,f3308,f1980,f454,f2099]) ).
fof(f8431,plain,
! [X0,X1] :
( ~ sQ70_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f133]) ).
fof(f8432,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f455,f8431]) ).
fof(f8433,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| X1 = c4
| X1 = c3
| X1 = op_a
| X0 = c4
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f8432]) ).
fof(f8434,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| X1 = c4
| X1 = e
| X1 = op_a
| X0 = c4
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f455,f8433]) ).
fof(f8435,plain,
( sQ83_spl
| ~ sQ70_spl
| ~ sQ33_spl
| op_b = e
| op_b = op_a
| op_b = e
| op_b = op_b
| op_b = op_a ),
inference(resolution,[status(thm)],[f8434,f2125]) ).
fof(f8436,plain,
! [X0] :
( sQ83_spl
| ~ sQ70_spl
| ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = op_a
| op_b = e
| op_b = X0
| op_b = op_a ),
inference(resolution,[status(thm)],[f8434,f2125]) ).
fof(f8441,plain,
! [X0] :
( sQ99_spl
| ~ sQ70_spl
| ~ sQ33_spl
| i(op_a) = c4
| i(op_a) = e
| X0 = c4
| X0 = e
| X0 = i(op_a)
| X0 = op_a ),
inference(resolution,[status(thm)],[f8434,f2507]) ).
fof(f8458,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| X0 = e
| c4 != e
| X1 = c4
| X1 = e
| X1 = op_a
| X0 = X1
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f8434]) ).
fof(f8460,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ33_spl
| X0 = e
| c4 != e
| X0 = c4
| X0 = op_a
| X0 = e
| X0 = X0
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f8434]) ).
fof(f8461,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ33_spl
| X0 = c4
| c4 != c4
| X0 = e
| X0 = op_a
| X0 = e
| X0 = X0
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f8434]) ).
fof(f8467,plain,
( sQ83_spl
| ~ sQ70_spl
| ~ sQ33_spl
| sQ82_spl
| sQ86_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f8435,f2155,f2184,f2120,f454,f1980,f2123]) ).
fof(f8468,plain,
( sQ83_spl
| ~ sQ70_spl
| ~ sQ33_spl
| sQ82_spl
| sQ102_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f8436,f2155,f2599,f2120,f454,f1980,f2123]) ).
fof(f8479,definition,
! [X0] :
( sQ173_spl
<=> ( X0 = c4
| X0 = e
| X0 = i(op_a)
| X0 = op_a ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f8482,plain,
( sQ99_spl
| ~ sQ70_spl
| ~ sQ33_spl
| sQ113_spl
| sQ98_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f8441,f8479,f2502,f2661,f454,f1980,f2505]) ).
fof(f8505,definition,
! [X0,X1] :
( sQ178_spl
<=> ( X0 = op_a
| X1 = c4
| X1 = e
| X1 = op_a
| X0 = e
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f8509,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ35_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f8458,f8505,f481,f454,f1980]) ).
fof(f8510,definition,
! [X0] :
( sQ179_spl
<=> ( X0 = op_a
| X0 = c4
| X0 = e
| X0 = e
| X0 = X0
| X0 = op_a ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f8514,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ35_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f8460,f8510,f481,f454,f1980]) ).
fof(f8515,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ4_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f8461,f8510,f52,f454,f1980]) ).
fof(f8532,plain,
! [X0] :
( ~ sQ167_spl
| ~ sQ33_spl
| X0 = e
| X0 = op_a
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f455,f7988]) ).
fof(f8533,plain,
! [X0] :
( ~ sQ167_spl
| ~ sQ33_spl
| X0 = op_a
| X0 = e ),
inference(duplicate_literals_removal,[status(thm)],[f8532]) ).
fof(f8547,plain,
! [X0] :
( ~ sQ81_spl
| ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = c2
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f455,f7035]) ).
fof(f8554,plain,
( sQ99_spl
| ~ sQ154_spl
| ~ sQ117_spl ),
inference(split_clause,[status(thm)],[f5039,f3284,f4962,f2505]) ).
fof(f8555,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ33_spl
| X0 = c4
| X0 = e
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f455,f8361]) ).
fof(f8557,plain,
( sQ94_spl
| ~ sQ121_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f4119,f2123,f3502,f2451]) ).
fof(f8559,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ33_spl
| X0 = op_b
| X0 = e
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f455,f4868]) ).
fof(f8597,plain,
( ~ sQ33_spl
| sQ118_spl
| op_b = c4
| op_b = e
| op_b = c1 ),
inference(resolution,[status(thm)],[f3310,f1373]) ).
fof(f8599,plain,
( ~ sQ33_spl
| sQ118_spl
| sQ83_spl
| sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f8597,f2117,f2120,f2123,f3308,f454]) ).
fof(f8612,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| op_a = c4
| op_a = e
| op_a = op_a ),
inference(resolution,[status(thm)],[f8555,f8365]) ).
fof(f8616,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| op_a = e
| op_a = c2
| op_a = op_a ),
inference(resolution,[status(thm)],[f8555,f8366]) ).
fof(f8627,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| sQ72_spl
| sQ73_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f8612,f2020,f2015,f1986,f454,f1980]) ).
fof(f8631,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| sQ73_spl
| sQ117_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f8616,f2020,f3284,f2015,f454,f1980]) ).
fof(f8645,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = e
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2124,f8374]) ).
fof(f8646,plain,
( sQ118_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| op_b = op_b
| op_b = e
| op_b = op_a ),
inference(resolution,[status(thm)],[f8645,f3310]) ).
fof(f8649,plain,
( sQ94_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f8645,f2453]) ).
fof(f8660,plain,
( sQ118_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ86_spl
| sQ82_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f8646,f2155,f2120,f2184,f2123,f1980,f454,f3308]) ).
fof(f8663,plain,
( sQ94_spl
| ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ95_spl
| sQ159_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f8649,f2457,f5140,f2454,f2123,f1980,f454,f2451]) ).
fof(f8671,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ98_spl
| i(op_a) = op_b
| i(op_a) = e
| i(op_a) = op_a
| c2 != e ),
inference(paramodulation,[status(thm)],[f8645,f2504]) ).
fof(f8672,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ97_spl
| sQ98_spl
| sQ99_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f8671,f486,f2505,f2502,f2499,f2123,f1980,f454]) ).
fof(f8681,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| ~ sQ154_spl
| i(c2) = op_b
| i(c2) = e
| i(c2) = op_a
| c2 = op_a ),
inference(paramodulation,[status(thm)],[f8645,f5020]) ).
fof(f8692,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| ~ sQ154_spl
| sQ158_spl
| sQ156_spl
| sQ157_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f8681,f3284,f5055,f5052,f5058,f4962,f2123,f1980,f454]) ).
fof(f8695,plain,
( sQ99_spl
| ~ sQ154_spl
| c2 != op_a ),
inference(backward_demodulation,[status(thm)],[f4963,f2507]) ).
fof(f8731,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| mult(op_a,op_b) = e
| mult(op_a,op_b) = c2
| mult(op_a,op_b) = op_a ),
inference(resolution,[status(thm)],[f1979,f8645]) ).
fof(f8732,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| mult(op_a,op_b) = op_b
| mult(op_a,op_b) = e
| mult(op_a,op_b) = op_a
| c2 != op_b ),
inference(paramodulation,[status(thm)],[f8645,f1979]) ).
fof(f8733,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| sQ79_spl
| sQ119_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f8731,f2305,f3387,f2096,f1977,f2123,f1980,f454]) ).
fof(f8734,plain,
( ~ sQ33_spl
| ~ sQ70_spl
| ~ sQ83_spl
| sQ69_spl
| sQ79_spl
| sQ87_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f8732,f3308,f2305,f2096,f1977,f2123,f1980,f454]) ).
fof(f8735,plain,
! [X0,X1] :
( ~ sQ70_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = c3
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f218]) ).
fof(f8736,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = c4
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f455,f8735]) ).
fof(f8737,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| X1 = c4
| X1 = c3
| X1 = c1
| X0 = op_b
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2124,f8736]) ).
fof(f8738,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| X1 = c4
| X1 = c3
| X1 = op_a
| X0 = op_b
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f8737]) ).
fof(f8739,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| X1 = c4
| X1 = e
| X1 = op_a
| X0 = op_b
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f455,f8738]) ).
fof(f8740,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| X1 = op_b
| X1 = e
| X1 = op_a
| X0 = op_b
| X0 = e
| X0 = X1
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2124,f8739]) ).
fof(f8754,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| c2 = op_b
| c2 = e
| X0 = op_b
| X0 = e
| X0 = c2
| X0 = op_a ),
inference(resolution,[status(thm)],[f8740,f8365]) ).
fof(f8778,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| X0 = op_b
| op_b != op_b
| X0 = e
| X0 = op_a
| X0 = e
| X0 = X0
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f8740]) ).
fof(f8809,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| sQ118_spl
| sQ36_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f8754,f7647,f486,f3308,f2123,f454,f1980]) ).
fof(f8824,definition,
! [X0] :
( sQ190_spl
<=> ( X0 = op_a
| X0 = op_b
| X0 = e
| X0 = e
| X0 = X0
| X0 = op_a ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f8829,plain,
( ~ sQ70_spl
| ~ sQ33_spl
| ~ sQ83_spl
| ~ sQ86_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f8778,f8824,f2184,f2123,f454,f1980]) ).
fof(f8847,plain,
( sQ69_spl
| ~ sQ119_spl
| c2 != op_b ),
inference(backward_demodulation,[status(thm)],[f3388,f1979]) ).
fof(f8848,plain,
( sQ87_spl
| ~ sQ119_spl
| c2 != op_a ),
inference(backward_demodulation,[status(thm)],[f3388,f2307]) ).
fof(f8850,plain,
( ~ sQ119_spl
| c2 != mult(op_b,op_a) ),
inference(backward_demodulation,[status(thm)],[f3388,f15]) ).
fof(f8854,plain,
( ~ sQ119_spl
| i(op_b) = mult(i(c2),op_a) ),
inference(paramodulation,[status(thm)],[f3388,f1469]) ).
fof(f8855,plain,
( ~ sQ119_spl
| i(op_a) = mult(op_b,i(c2)) ),
inference(paramodulation,[status(thm)],[f3388,f1272]) ).
fof(f8858,plain,
( ~ sQ119_spl
| ~ sQ159_spl ),
inference(split_clause,[status(thm)],[f8850,f5140,f3387]) ).
fof(f8863,plain,
( ~ sQ119_spl
| ~ sQ154_spl
| c2 = mult(op_b,i(c2)) ),
inference(forward_demodulation,[status(thm)],[f4963,f8855]) ).
fof(f8864,plain,
( ~ sQ119_spl
| ~ sQ154_spl
| c2 = mult(op_b,op_a) ),
inference(forward_demodulation,[status(thm)],[f5020,f8863]) ).
fof(f8873,plain,
( ~ sQ78_spl
| ~ sQ70_spl
| mult(i(op_a),op_a) = op_b ),
inference(forward_demodulation,[status(thm)],[f1981,f3865]) ).
fof(f8874,plain,
( ~ sQ78_spl
| ~ sQ70_spl
| e = op_b ),
inference(forward_demodulation,[status(thm)],[f1049,f8873]) ).
fof(f8875,plain,
( ~ sQ78_spl
| ~ sQ70_spl
| sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8874,f2122]) ).
fof(f8876,plain,
( ~ sQ78_spl
| ~ sQ70_spl
| sQ82_spl ),
inference(contradiction_clause,[status(thm)],[f8875]) ).
fof(f8877,plain,
( ~ sQ160_spl
| ~ sQ70_spl
| i(op_a) = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f5830]) ).
fof(f8891,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| ~ sQ33_spl
| op_b = mult(i(e),op_a) ),
inference(forward_demodulation,[status(thm)],[f455,f4850]) ).
fof(f8892,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| ~ sQ33_spl
| op_b = mult(e,op_a) ),
inference(forward_demodulation,[status(thm)],[f1106,f8891]) ).
fof(f8893,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| ~ sQ33_spl
| op_b = op_a ),
inference(forward_demodulation,[status(thm)],[f1046,f8892]) ).
fof(f8894,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| ~ sQ33_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8893,f2157]) ).
fof(f8895,plain,
( ~ sQ151_spl
| ~ sQ88_spl
| ~ sQ33_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f8894]) ).
fof(f8896,plain,
( sQ79_spl
| ~ sQ151_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f4842,f454,f4792,f2096]) ).
fof(f8899,plain,
( sQ69_spl
| ~ sQ119_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f8847,f3308,f3387,f1977]) ).
fof(f8905,plain,
( ~ sQ78_spl
| ~ sQ81_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f2335,f1977,f2117,f2093]) ).
fof(f8922,plain,
( ~ sQ119_spl
| ~ sQ154_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f8864,f5140,f4962,f3387]) ).
fof(f8924,plain,
( sQ99_spl
| ~ sQ154_spl
| ~ sQ33_spl
| op_a = c4
| op_a = e
| op_a = c1 ),
inference(resolution,[status(thm)],[f1373,f8695]) ).
fof(f8939,plain,
( sQ99_spl
| ~ sQ154_spl
| ~ sQ33_spl
| sQ72_spl
| sQ73_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f8924,f1980,f2015,f1986,f454,f4962,f2505]) ).
fof(f8956,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ72_spl
| X0 = op_a
| X0 = e
| X0 = c2
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f1987,f1373]) ).
fof(f8959,plain,
( ~ sQ72_spl
| c2 != op_a ),
inference(backward_demodulation,[status(thm)],[f1987,f21]) ).
fof(f8960,plain,
( ~ sQ83_spl
| ~ sQ72_spl
| op_b = op_a ),
inference(forward_demodulation,[status(thm)],[f1987,f2124]) ).
fof(f8961,plain,
( ~ sQ83_spl
| ~ sQ72_spl
| sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8960,f2157]) ).
fof(f8962,plain,
( ~ sQ83_spl
| ~ sQ72_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f8961]) ).
fof(f9011,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ72_spl
| ~ sQ81_spl
| X0 = op_a
| X0 = e
| X0 = c2
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f8956]) ).
fof(f9012,plain,
( sQ118_spl
| ~ sQ33_spl
| ~ sQ72_spl
| ~ sQ81_spl
| op_b = op_a
| op_b = e
| op_b = op_b ),
inference(resolution,[status(thm)],[f9011,f3310]) ).
fof(f9013,plain,
( ~ sQ72_spl
| ~ sQ33_spl
| ~ sQ81_spl
| op_a = op_a
| op_a = e
| op_a = op_b ),
inference(resolution,[status(thm)],[f9011,f8959]) ).
fof(f9022,plain,
( sQ118_spl
| ~ sQ33_spl
| ~ sQ72_spl
| ~ sQ81_spl
| sQ84_spl
| sQ82_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f9012,f2184,f2120,f2155,f2117,f1986,f454,f3308]) ).
fof(f9023,plain,
( ~ sQ72_spl
| ~ sQ33_spl
| ~ sQ81_spl
| sQ74_spl
| sQ73_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f9013,f2155,f2015,f2020,f2117,f454,f1986]) ).
fof(f9040,plain,
! [X0] :
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| X0 = c4
| X0 = e
| X0 = op_a
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f3285,f8547]) ).
fof(f9041,plain,
( ~ sQ117_spl
| ~ sQ81_spl
| ~ sQ33_spl
| op_a = e
| op_a = op_a
| op_a = op_b ),
inference(resolution,[status(thm)],[f9040,f7870]) ).
fof(f9050,plain,
! [X0] :
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| X0 = e
| c4 != e
| X0 = op_a
| X0 = op_b ),
inference(equality_factoring,[status(thm)],[f9040]) ).
fof(f9051,plain,
( ~ sQ117_spl
| ~ sQ81_spl
| ~ sQ33_spl
| sQ73_spl
| sQ74_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f9041,f2155,f2020,f2015,f454,f2117,f3284]) ).
fof(f9056,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ35_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f9050,f2159,f481,f3284,f454,f2117]) ).
fof(f9057,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ89_spl
| i(op_b) = e
| i(op_b) = op_a
| i(op_b) = op_b
| c4 != e ),
inference(paramodulation,[status(thm)],[f9040,f2330]) ).
fof(f9058,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ89_spl
| sQ90_spl
| sQ88_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f9057,f481,f2325,f2331,f2328,f3284,f454,f2117]) ).
fof(f9059,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ90_spl
| i(op_b) = e
| i(op_b) = op_a
| i(op_b) = op_b
| c4 != op_a ),
inference(paramodulation,[status(thm)],[f9040,f2333]) ).
fof(f9060,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ89_spl
| sQ90_spl
| sQ88_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f9059,f1986,f2325,f2331,f2328,f3284,f454,f2117]) ).
fof(f9064,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ98_spl
| i(op_a) = e
| i(op_a) = op_a
| i(op_a) = op_b
| c4 != e ),
inference(paramodulation,[status(thm)],[f9040,f2504]) ).
fof(f9065,plain,
( ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ98_spl
| sQ99_spl
| sQ97_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f9064,f481,f2499,f2505,f2502,f3284,f454,f2117]) ).
fof(f9068,plain,
( sQ99_spl
| ~ sQ167_spl
| ~ sQ33_spl
| i(op_a) = e ),
inference(resolution,[status(thm)],[f8533,f2507]) ).
fof(f9069,plain,
( sQ90_spl
| ~ sQ167_spl
| ~ sQ33_spl
| i(op_b) = e ),
inference(resolution,[status(thm)],[f8533,f2333]) ).
fof(f9073,plain,
( sQ84_spl
| ~ sQ167_spl
| ~ sQ33_spl
| op_b = e ),
inference(resolution,[status(thm)],[f8533,f2157]) ).
fof(f9084,plain,
( sQ99_spl
| ~ sQ167_spl
| ~ sQ33_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f9068,f2502,f454,f7987,f2505]) ).
fof(f9085,plain,
( sQ90_spl
| ~ sQ167_spl
| ~ sQ33_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f9069,f2328,f454,f7987,f2331]) ).
fof(f9088,plain,
( sQ84_spl
| ~ sQ167_spl
| ~ sQ33_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f9073,f2120,f454,f7987,f2155]) ).
fof(f9090,plain,
( ~ sQ157_spl
| ~ sQ117_spl
| i(op_a) = op_a ),
inference(forward_demodulation,[status(thm)],[f3285,f5056]) ).
fof(f9091,plain,
( ~ sQ157_spl
| ~ sQ117_spl
| sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9090,f2507]) ).
fof(f9092,plain,
( ~ sQ157_spl
| ~ sQ117_spl
| sQ99_spl ),
inference(contradiction_clause,[status(thm)],[f9091]) ).
fof(f9096,plain,
( sQ98_spl
| ~ sQ113_spl
| c4 != e ),
inference(backward_demodulation,[status(thm)],[f2662,f2504]) ).
fof(f9117,plain,
( sQ104_spl
| ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| i(op_b) = e
| i(op_b) = op_a
| i(op_b) = op_b ),
inference(resolution,[status(thm)],[f9040,f2608]) ).
fof(f9119,plain,
( ~ sQ80_spl
| ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = op_b ),
inference(resolution,[status(thm)],[f9040,f8217]) ).
fof(f9130,plain,
( sQ104_spl
| ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ89_spl
| sQ90_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f9117,f2325,f2331,f2328,f3284,f454,f2117,f2606]) ).
fof(f9132,plain,
( ~ sQ80_spl
| ~ sQ81_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ95_spl
| sQ96_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f9119,f2451,f2457,f2454,f3284,f454,f2117,f2099]) ).
fof(f9145,plain,
( ~ sQ119_spl
| ~ sQ117_spl
| i(op_b) = mult(i(op_a),op_a) ),
inference(forward_demodulation,[status(thm)],[f3285,f8854]) ).
fof(f9146,plain,
( ~ sQ119_spl
| ~ sQ117_spl
| i(op_b) = e ),
inference(forward_demodulation,[status(thm)],[f1049,f9145]) ).
fof(f9147,plain,
( ~ sQ119_spl
| ~ sQ117_spl
| sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9146,f2330]) ).
fof(f9148,plain,
( ~ sQ119_spl
| ~ sQ117_spl
| sQ89_spl ),
inference(contradiction_clause,[status(thm)],[f9147]) ).
fof(f9149,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ117_spl
| X0 = c4
| X0 = e
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3285,f1373]) ).
fof(f9151,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ33_spl
| ~ sQ117_spl
| X0 = op_b
| X0 = e
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3285,f8559]) ).
fof(f9156,plain,
( ~ sQ117_spl
| ~ sQ33_spl
| op_a = e
| op_a = op_a
| op_a = c1 ),
inference(resolution,[status(thm)],[f9149,f7870]) ).
fof(f9164,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ117_spl
| X0 = e
| c4 != e
| X0 = op_a
| X0 = c1 ),
inference(equality_factoring,[status(thm)],[f9149]) ).
fof(f9166,plain,
( ~ sQ117_spl
| ~ sQ33_spl
| sQ73_spl
| sQ74_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f9156,f1980,f2020,f2015,f454,f3284]) ).
fof(f9170,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ35_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f9164,f2024,f481,f3284,f454]) ).
fof(f9171,plain,
! [X0] :
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = e
| X0 = op_a
| X0 = c1 ),
inference(backward_demodulation,[status(thm)],[f2124,f9149]) ).
fof(f9175,plain,
( sQ81_spl
| ~ sQ83_spl
| ~ sQ33_spl
| ~ sQ117_spl
| op_b = op_b
| op_b = e
| op_b = op_a ),
inference(resolution,[status(thm)],[f9151,f2119]) ).
fof(f9185,plain,
( sQ81_spl
| ~ sQ83_spl
| ~ sQ33_spl
| ~ sQ117_spl
| sQ86_spl
| sQ82_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f9175,f2155,f2120,f2184,f3284,f454,f2123,f2117]) ).
fof(f9204,plain,
( sQ94_spl
| ~ sQ101_spl
| ~ sQ83_spl
| op_a = mult(op_b,op_a) ),
inference(resolution,[status(thm)],[f5106,f2453]) ).
fof(f9206,plain,
( sQ81_spl
| ~ sQ101_spl
| ~ sQ83_spl
| op_a = c1 ),
inference(resolution,[status(thm)],[f5106,f2119]) ).
fof(f9217,plain,
( sQ94_spl
| ~ sQ101_spl
| ~ sQ83_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f9204,f2457,f2123,f2594,f2451]) ).
fof(f9218,plain,
( sQ81_spl
| ~ sQ101_spl
| ~ sQ83_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f9206,f1980,f2123,f2594,f2117]) ).
fof(f9228,plain,
( ~ sQ80_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f8217,f3502,f2099]) ).
fof(f9230,plain,
( sQ98_spl
| ~ sQ113_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f9096,f481,f2661,f2502]) ).
fof(f9234,plain,
( sQ95_spl
| ~ sQ121_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f4117,f481,f3502,f2454]) ).
fof(f9235,plain,
( sQ87_spl
| ~ sQ151_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f4841,f1983,f4792,f2305]) ).
fof(f9236,plain,
( sQ79_spl
| ~ sQ78_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3858,f448,f2093,f2096]) ).
fof(f9308,plain,
( ~ sQ151_spl
| ~ sQ31_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f5183,f4843]) ).
fof(f9330,plain,
( ~ sQ151_spl
| ~ sQ31_spl
| sQ121_spl
| sQ159_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f9308,f2454,f5140,f3502,f448,f4792]) ).
fof(f9352,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| X0 = op_b
| X0 = c3
| X0 = op_a
| X0 = e ),
inference(forward_demodulation,[status(thm)],[f2124,f7868]) ).
fof(f9353,plain,
( sQ96_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = c3
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f9352,f2459]) ).
fof(f9356,plain,
( sQ84_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| op_b = op_b
| op_b = c3
| op_b = e ),
inference(resolution,[status(thm)],[f9352,f2157]) ).
fof(f9358,plain,
( sQ71_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| op_a = op_b
| op_a = op_a
| op_a = e ),
inference(resolution,[status(thm)],[f9352,f1985]) ).
fof(f9379,plain,
( sQ96_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| sQ94_spl
| sQ152_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f9353,f2454,f4803,f2451,f2123,f3284,f448,f2457]) ).
fof(f9382,plain,
( sQ84_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| sQ86_spl
| sQ77_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f9356,f2120,f2090,f2184,f2123,f3284,f448,f2155]) ).
fof(f9384,plain,
( sQ71_spl
| ~ sQ31_spl
| ~ sQ117_spl
| ~ sQ83_spl
| sQ84_spl
| sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f9358,f2015,f2020,f2155,f2123,f3284,f448,f1983]) ).
fof(f9406,plain,
( sQ79_spl
| ~ sQ80_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f4159,f481,f2099,f2096]) ).
fof(f9412,plain,
! [X0] :
( ~ sQ117_spl
| X0 = c4
| X0 = c3
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3285,f16]) ).
fof(f9414,plain,
( sQ33_spl
| ~ sQ117_spl
| e = c4
| e = op_a
| e = c1 ),
inference(resolution,[status(thm)],[f9412,f456]) ).
fof(f9415,plain,
( ~ sQ117_spl
| op_a = c3
| op_a = op_a
| op_a = c1 ),
inference(resolution,[status(thm)],[f9412,f7870]) ).
fof(f9424,plain,
( sQ33_spl
| ~ sQ117_spl
| sQ35_spl
| sQ73_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f9414,f448,f2015,f481,f3284,f454]) ).
fof(f9425,plain,
( ~ sQ117_spl
| sQ71_spl
| sQ74_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f9415,f1980,f2020,f1983,f3284]) ).
fof(f9445,plain,
! [X0] :
( ~ sQ77_spl
| ~ sQ117_spl
| X0 = c4
| X0 = op_b
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3285,f3698]) ).
fof(f9447,plain,
( ~ sQ77_spl
| ~ sQ117_spl
| op_b = op_b
| op_b = op_a
| op_b = c1 ),
inference(resolution,[status(thm)],[f9445,f3367]) ).
fof(f9457,plain,
( ~ sQ77_spl
| ~ sQ117_spl
| sQ86_spl
| sQ84_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f9447,f2117,f2155,f2184,f3284,f2090]) ).
fof(f9467,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ117_spl
| X0 = e
| X0 = c3
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3285,f502]) ).
fof(f9468,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ117_spl
| ~ sQ77_spl
| X0 = e
| X0 = op_b
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f2091,f9467]) ).
fof(f9494,plain,
( ~ sQ35_spl
| ~ sQ117_spl
| ~ sQ77_spl
| ~ sQ78_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = op_a
| c1 != c1 ),
inference(paramodulation,[status(thm)],[f9468,f4027]) ).
fof(f9496,plain,
( ~ sQ35_spl
| ~ sQ117_spl
| ~ sQ77_spl
| ~ sQ78_spl
| sQ95_spl
| sQ94_spl
| sQ96_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f9494,f39,f2457,f2451,f2454,f2093,f2090,f3284,f481]) ).
fof(f9498,plain,
! [X0] :
( ~ sQ117_spl
| ~ sQ35_spl
| X0 = e
| X0 = c3
| X0 = op_a
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f9412]) ).
fof(f9503,plain,
( ~ sQ83_spl
| ~ sQ35_spl
| op_b = e ),
inference(forward_demodulation,[status(thm)],[f482,f2124]) ).
fof(f9504,plain,
( ~ sQ83_spl
| ~ sQ35_spl
| sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9503,f2122]) ).
fof(f9505,plain,
( ~ sQ83_spl
| ~ sQ35_spl
| sQ82_spl ),
inference(contradiction_clause,[status(thm)],[f9504]) ).
fof(f9510,plain,
( sQ69_spl
| ~ sQ151_spl
| ~ sQ77_spl ),
inference(split_clause,[status(thm)],[f4840,f2090,f4792,f1977]) ).
fof(f9558,plain,
! [X0] :
( ~ sQ117_spl
| ~ sQ35_spl
| ~ sQ81_spl
| X0 = e
| X0 = c3
| X0 = op_a
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f9498]) ).
fof(f9560,plain,
( sQ77_spl
| ~ sQ117_spl
| ~ sQ35_spl
| ~ sQ81_spl
| op_b = e
| op_b = op_a
| op_b = op_b ),
inference(resolution,[status(thm)],[f9558,f2092]) ).
fof(f9570,plain,
( sQ77_spl
| ~ sQ117_spl
| ~ sQ35_spl
| ~ sQ81_spl
| sQ82_spl
| sQ84_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f9560,f2184,f2155,f2120,f2117,f481,f3284,f2090]) ).
fof(f9576,plain,
( ~ sQ117_spl
| ~ sQ35_spl
| ~ sQ81_spl
| ~ sQ151_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = op_b
| c3 != c3 ),
inference(paramodulation,[status(thm)],[f9558,f4843]) ).
fof(f9578,plain,
( ~ sQ117_spl
| ~ sQ35_spl
| ~ sQ81_spl
| ~ sQ151_spl
| sQ95_spl
| sQ96_spl
| sQ94_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f9576,f56,f2451,f2457,f2454,f4792,f2117,f481,f3284]) ).
fof(f9582,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ35_spl
| X0 = e
| X0 = c3
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f482,f8361]) ).
fof(f9588,plain,
! [X0] :
( ~ sQ35_spl
| X0 = e
| X0 = c3
| X0 = c2
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f16]) ).
fof(f9597,plain,
( ~ sQ70_spl
| ~ sQ35_spl
| op_a = e
| op_a = c3
| op_a = op_a ),
inference(resolution,[status(thm)],[f9582,f8365]) ).
fof(f9599,plain,
( ~ sQ151_spl
| ~ sQ70_spl
| ~ sQ35_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f9582,f4843]) ).
fof(f9607,plain,
! [X0] :
( ~ sQ70_spl
| ~ sQ35_spl
| X0 = e
| c2 != e
| X0 = c3
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f9582]) ).
fof(f9608,plain,
( ~ sQ70_spl
| ~ sQ35_spl
| sQ73_spl
| sQ71_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f9597,f2020,f1983,f2015,f481,f1980]) ).
fof(f9610,plain,
( ~ sQ151_spl
| ~ sQ70_spl
| ~ sQ35_spl
| sQ95_spl
| sQ159_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f9599,f2457,f5140,f2454,f481,f1980,f4792]) ).
fof(f9616,plain,
( ~ sQ70_spl
| ~ sQ35_spl
| ~ sQ36_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f9607,f7987,f486,f481,f1980]) ).
fof(f9625,plain,
( ~ sQ160_spl
| ~ sQ70_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f8877,f2505,f1980,f5829]) ).
fof(f9642,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ70_spl
| X0 = e
| X0 = c3
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f1981,f9588]) ).
fof(f9643,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ70_spl
| ~ sQ77_spl
| X0 = e
| X0 = op_b
| X0 = c2
| X0 = op_a ),
inference(forward_demodulation,[status(thm)],[f2091,f9642]) ).
fof(f9649,plain,
( sQ94_spl
| ~ sQ35_spl
| ~ sQ70_spl
| ~ sQ77_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f9643,f2453]) ).
fof(f9658,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ70_spl
| ~ sQ77_spl
| X0 = e
| c2 != e
| X0 = op_b
| X0 = op_a ),
inference(equality_factoring,[status(thm)],[f9643]) ).
fof(f9664,plain,
( sQ94_spl
| ~ sQ35_spl
| ~ sQ70_spl
| ~ sQ77_spl
| sQ95_spl
| sQ159_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f9649,f2457,f5140,f2454,f2090,f1980,f481,f2451]) ).
fof(f9669,plain,
( ~ sQ35_spl
| ~ sQ70_spl
| ~ sQ77_spl
| ~ sQ36_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f9658,f2159,f486,f2090,f1980,f481]) ).
fof(f9752,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ83_spl
| ~ sQ78_spl
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a ),
inference(resolution,[status(thm)],[f3860,f9171]) ).
fof(f9753,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ83_spl
| ~ sQ78_spl
| mult(op_b,op_a) = op_b
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a
| c1 != c1 ),
inference(paramodulation,[status(thm)],[f9171,f3860]) ).
fof(f9754,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ83_spl
| ~ sQ78_spl
| sQ94_spl
| sQ95_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f9752,f2457,f2454,f2451,f2093,f2123,f3284,f454]) ).
fof(f9755,plain,
( ~ sQ33_spl
| ~ sQ117_spl
| ~ sQ83_spl
| ~ sQ78_spl
| sQ94_spl
| sQ95_spl
| sQ96_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f9753,f39,f2457,f2454,f2451,f2093,f2123,f3284,f454]) ).
fof(f9806,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ118_spl
| X0 = c4
| X0 = op_a
| X0 = op_b
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3309,f6044]) ).
fof(f9808,plain,
( sQ83_spl
| ~ sQ71_spl
| ~ sQ118_spl
| op_b = op_a
| op_b = op_b
| op_b = c1 ),
inference(resolution,[status(thm)],[f9806,f2125]) ).
fof(f9818,plain,
( sQ83_spl
| ~ sQ71_spl
| ~ sQ118_spl
| sQ84_spl
| sQ86_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f9808,f2117,f2184,f2155,f3308,f1983,f2123]) ).
fof(f9832,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ118_spl
| X0 = c4
| X0 = op_a
| X0 = op_b
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f3309,f6732]) ).
fof(f9833,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ118_spl
| ~ sQ35_spl
| X0 = e
| X0 = op_a
| X0 = op_b
| X0 = c1 ),
inference(forward_demodulation,[status(thm)],[f482,f9832]) ).
fof(f9837,plain,
( ~ sQ78_spl
| ~ sQ71_spl
| ~ sQ118_spl
| ~ sQ35_spl
| mult(op_b,op_a) = e
| mult(op_b,op_a) = op_a
| mult(op_b,op_a) = op_b ),
inference(resolution,[status(thm)],[f9833,f3860]) ).
fof(f9848,plain,
( ~ sQ78_spl
| ~ sQ71_spl
| ~ sQ118_spl
| ~ sQ35_spl
| sQ95_spl
| sQ96_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f9837,f2451,f2457,f2454,f481,f3308,f1983,f2093]) ).
fof(f9914,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ81_spl
| X0 = c4
| X0 = op_a
| X0 = c2
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f5537]) ).
fof(f9915,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ81_spl
| ~ sQ35_spl
| X0 = e
| X0 = op_a
| X0 = c2
| X0 = op_b ),
inference(forward_demodulation,[status(thm)],[f482,f9914]) ).
fof(f9973,plain,
( ~ sQ71_spl
| ~ sQ81_spl
| ~ sQ35_spl
| sQ154_spl
| i(op_a) = e
| i(op_a) = op_a
| i(op_a) = op_b ),
inference(resolution,[status(thm)],[f4964,f9915]) ).
fof(f9975,plain,
( ~ sQ71_spl
| ~ sQ81_spl
| ~ sQ35_spl
| sQ154_spl
| sQ98_spl
| sQ99_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f9973,f2499,f2505,f2502,f4962,f481,f2117,f1983]) ).
fof(f10006,plain,
( ~ sQ162_spl
| ~ sQ81_spl
| mult(op_b,op_a) = op_b ),
inference(forward_demodulation,[status(thm)],[f2118,f6701]) ).
fof(f10007,plain,
( ~ sQ162_spl
| ~ sQ81_spl
| sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10006,f2453]) ).
fof(f10008,plain,
( ~ sQ162_spl
| ~ sQ81_spl
| sQ94_spl ),
inference(contradiction_clause,[status(thm)],[f10007]) ).
fof(f10016,plain,
( ~ sQ152_spl
| ~ sQ71_spl
| mult(op_b,op_a) = op_a ),
inference(forward_demodulation,[status(thm)],[f1984,f4804]) ).
fof(f10017,plain,
( ~ sQ152_spl
| ~ sQ71_spl
| sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10016,f2459]) ).
fof(f10018,plain,
( ~ sQ152_spl
| ~ sQ71_spl
| sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f10017]) ).
fof(f10021,plain,
( sQ96_spl
| ~ sQ121_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f4118,f1986,f3502,f2457]) ).
fof(f10022,plain,
( sQ87_spl
| ~ sQ119_spl
| op_a = c4
| op_a = c3
| op_a = c1 ),
inference(resolution,[status(thm)],[f16,f8848]) ).
fof(f10030,plain,
( sQ87_spl
| ~ sQ119_spl
| sQ72_spl
| sQ71_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f10022,f1980,f1983,f1986,f3387,f2305]) ).
fof(f10103,plain,
( sQ94_spl
| ~ sQ31_spl
| ~ sQ77_spl
| mult(op_b,op_a) = c4
| mult(op_b,op_a) = c2
| mult(op_b,op_a) = e ),
inference(resolution,[status(thm)],[f3363,f2453]) ).
fof(f10118,plain,
( sQ94_spl
| ~ sQ31_spl
| ~ sQ77_spl
| sQ121_spl
| sQ159_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f10103,f2454,f5140,f3502,f2090,f448,f2451]) ).
fof(f10148,plain,
( ~ sQ77_spl
| op_b = c4
| op_b = op_b
| op_b = c1 ),
inference(resolution,[status(thm)],[f3698,f3364]) ).
fof(f10158,plain,
( ~ sQ77_spl
| sQ83_spl
| sQ86_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f10148,f2117,f2184,f2123,f2090]) ).
fof(f10183,plain,
( ~ sQ35_spl
| ~ sQ72_spl
| op_a = e ),
inference(forward_demodulation,[status(thm)],[f1987,f482]) ).
fof(f10184,plain,
( ~ sQ35_spl
| ~ sQ72_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10183,f2017]) ).
fof(f10185,plain,
( ~ sQ35_spl
| ~ sQ72_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f10184]) ).
fof(f10245,plain,
( sQ95_spl
| ~ sQ152_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f7728,f454,f4803,f2454]) ).
fof(f10248,plain,
( ~ sQ78_spl
| ~ sQ162_spl ),
inference(split_clause,[status(thm)],[f3860,f6700,f2093]) ).
fof(f10249,plain,
$false,
inference(sat_refutation,[status(thm)],[f48,f59,f76,f84,f87,f89,f91,f102,f112,f114,f193,f206,f367,f373,f411,f457,f461,f494,f523,f572,f588,f607,f632,f680,f719,f759,f776,f813,f822,f863,f903,f913,f974,f986,f992,f1112,f1171,f1208,f1317,f1318,f1341,f1346,f1364,f1365,f1511,f1535,f1540,f1541,f1558,f1576,f1660,f1974,f2023,f2047,f2065,f2102,f2126,f2130,f2145,f2169,f2252,f2255,f2268,f2269,f2391,f2435,f2460,f2511,f2537,f2549,f2550,f2598,f2630,f2667,f2668,f2959,f2994,f3001,f3051,f3052,f3058,f3130,f3136,f3141,f3200,f3203,f3206,f3210,f3219,f3240,f3287,f3298,f3311,f3348,f3353,f3390,f3434,f3505,f3600,f3647,f3751,f3785,f3817,f3856,f3928,f3943,f3957,f3960,f3961,f3975,f4038,f4039,f4209,f4212,f4381,f4394,f4407,f4650,f4651,f4652,f4691,f4786,f4795,f4806,f4867,f4915,f4916,f4975,f4987,f5132,f5135,f5154,f5200,f5202,f5832,f5877,f5891,f6203,f6374,f6551,f6561,f6681,f6703,f7072,f7245,f7247,f7271,f7296,f7514,f7610,f7754,f7756,f7762,f7776,f7783,f7785,f7809,f7874,f7875,f7885,f7920,f7928,f7935,f7937,f7975,f7976,f8176,f8187,f8260,f8266,f8276,f8305,f8396,f8402,f8467,f8468,f8482,f8509,f8514,f8515,f8554,f8557,f8599,f8627,f8631,f8660,f8663,f8672,f8692,f8733,f8734,f8809,f8829,f8858,f8876,f8895,f8896,f8899,f8905,f8922,f8939,f8962,f9022,f9023,f9051,f9056,f9058,f9060,f9065,f9084,f9085,f9088,f9092,f9130,f9132,f9148,f9166,f9170,f9185,f9217,f9218,f9228,f9230,f9234,f9235,f9236,f9330,f9379,f9382,f9384,f9406,f9424,f9425,f9457,f9496,f9505,f9510,f9570,f9578,f9608,f9610,f9616,f9625,f9664,f9669,f9754,f9755,f9818,f9848,f9975,f10008,f10018,f10021,f10030,f10118,f10158,f10185,f10245,f10248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP759+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.59 % Computer : n006.cluster.edu
% 0.10/10.59 % Model : x86_64 x86_64
% 0.10/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.59 % Memory : 8046.5625MB
% 0.10/10.59 % OS : Linux 6.8.0-71-generic
% 0.10/10.59 % CPULimit : 300
% 0.10/10.59 % WCLimit : 300
% 0.10/10.59 % DateTime : Sun Sep 20 20:38:11 UTC 2026
% 0.10/10.60 % CPUTime :
% 0.15/10.60 % Drodi V4.1.1
% 15.65/12.65 % Refutation found
% 15.65/12.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 15.65/12.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.65/12.68 % Elapsed time: 2.079394 seconds
% 15.65/12.68 % CPU time: 16.296627 seconds
% 15.65/12.68 % Total memory used: 146.292 MB
% 15.65/12.68 % Net memory used: 132.106 MB
%------------------------------------------------------------------------------