%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP645+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:34:57 PM UTC 2026
% Result : Theorem 166.53s 23.00s
% Output : CNFRefutation 156.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 81
% Syntax : Number of formulae : 336 ( 110 unt; 55 def)
% Number of atoms : 1011 ( 56 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1002 ( 327 ~; 308 |; 296 &)
% ( 57 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 119 ( 117 usr; 56 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 17 con; 0-3 aty)
% Number of variables : 120 ( 107 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f58,axiom,
! [A,B] : k3_xboole_0(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B] : r1_tarski(k3_xboole_0(A,B),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [A,B] : k3_xboole_0(A,k2_xboole_0(A,B)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [A,B,C] : k3_xboole_0(A,k4_xboole_0(B,C)) = k4_xboole_0(k3_xboole_0(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1179,axiom,
( v3_ordinal1(k1_xboole_0)
& v2_ordinal1(k1_xboole_0)
& v1_ordinal1(k1_xboole_0)
& v1_xboole_0(k1_xboole_0)
& v2_funct_1(k1_xboole_0)
& v1_funct_1(k1_xboole_0)
& v3_relat_1(k1_xboole_0)
& v1_relat_1(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3065,axiom,
? [A] :
( v3_xreal_0(A)
& ~ v2_xreal_0(A)
& v1_xreal_0(A)
& v1_xcmplx_0(A)
& ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8911,axiom,
! [A,B,C] :
( ( m1_group_2(C,A)
& m1_group_2(B,A)
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m1_group_2(k9_group_2(A,B,C),A)
& v1_group_1(k9_group_2(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11093,axiom,
? [A] :
( v3_realset2(A)
& v4_group_1(A)
& v3_group_1(A)
& v2_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11282,axiom,
? [A] :
( v1_gr_cy_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v2_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11341,axiom,
( l1_group_1(k3_gr_cy_1)
& v7_group_1(k3_gr_cy_1)
& v4_group_1(k3_gr_cy_1)
& v3_group_1(k3_gr_cy_1)
& ~ v3_struct_0(k3_gr_cy_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11345,axiom,
( l1_group_1(k3_gr_cy_1)
& v4_group_1(k3_gr_cy_1)
& v3_group_1(k3_gr_cy_1)
& v1_group_1(k3_gr_cy_1)
& ~ v3_struct_0(k3_gr_cy_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11937,axiom,
? [A] :
( v17_monoid_0(A)
& v16_monoid_0(A)
& v13_monoid_0(A)
& v10_monoid_0(A)
& v2_monoid_0(A)
& v1_monoid_0(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11947,axiom,
? [A] :
( v17_monoid_0(A)
& v16_monoid_0(A)
& v15_monoid_0(A)
& v14_monoid_0(A)
& v13_monoid_0(A)
& v12_monoid_0(A)
& v11_monoid_0(A)
& v10_monoid_0(A)
& v2_monoid_0(A)
& v1_monoid_0(A)
& v1_vectsp_2(A)
& v8_vectsp_1(A)
& v6_vectsp_1(A)
& v1_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v2_group_1(A)
& ~ v3_struct_0(A)
& l1_vectsp_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12141,axiom,
( l1_group_1(k5_monoid_0)
& v16_monoid_0(k5_monoid_0)
& v13_monoid_0(k5_monoid_0)
& v7_group_1(k5_monoid_0)
& v4_group_1(k5_monoid_0)
& v2_group_1(k5_monoid_0)
& v1_group_1(k5_monoid_0)
& ~ v3_struct_0(k5_monoid_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12142,axiom,
( m2_monoid_0(k6_monoid_0,k5_monoid_0)
& v13_monoid_0(k6_monoid_0)
& v2_group_1(k6_monoid_0)
& v1_group_1(k6_monoid_0)
& ~ v3_struct_0(k6_monoid_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12143,axiom,
k6_monoid_0 = k3_gr_cy_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12146,axiom,
( l1_group_1(k9_monoid_0)
& v7_group_1(k9_monoid_0)
& v4_group_1(k9_monoid_0)
& v2_group_1(k9_monoid_0)
& v1_group_1(k9_monoid_0)
& ~ v3_struct_0(k9_monoid_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13120,axiom,
? [A] :
( v6_quantal1(A)
& v5_quantal1(A)
& v4_quantal1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13122,axiom,
? [A] :
( v8_quantal1(A)
& v7_quantal1(A)
& v6_quantal1(A)
& v5_quantal1(A)
& v4_quantal1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v4_lattice3(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l1_quantal1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13126,axiom,
? [A] :
( v10_quantal1(A)
& v9_quantal1(A)
& v8_quantal1(A)
& v7_quantal1(A)
& v6_quantal1(A)
& v5_quantal1(A)
& v4_quantal1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v4_lattice3(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l2_quantal1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13131,axiom,
? [A] :
( v21_quantal1(A)
& v20_quantal1(A)
& v19_quantal1(A)
& v10_quantal1(A)
& v9_quantal1(A)
& v8_quantal1(A)
& v7_quantal1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v4_lattice3(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_quantal1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13961,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(k1_latsubgr(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13978,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(B) )
=> ( B = k1_latsubgr(A)
<=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(B,C) = u1_struct_0(C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13987,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13988,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13989,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
inference(negated_conjecture,[status(cth)],[f13988]) ).
fof(f14199,plain,
! [A] : k3_xboole_0(A,A) = A,
inference(miniscoping,[status(thm)],[f58]) ).
fof(f14200,plain,
! [X0] : X0 = k3_xboole_0(X0,X0),
inference(cnf_transformation,[status(thm)],[f14199]) ).
fof(f14203,plain,
! [X0] : k3_xboole_0(X0,k1_xboole_0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f14249,plain,
! [X0,X1] : r1_tarski(k3_xboole_0(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f14260,plain,
! [X0,X1] : k3_xboole_0(X0,k2_xboole_0(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f14308,plain,
! [X0,X1,X2] : k3_xboole_0(X0,k4_xboole_0(X1,X2)) = k4_xboole_0(k3_xboole_0(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f16829,plain,
v1_funct_1(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f22902,plain,
( v3_xreal_0(sK960_skl)
& ~ v2_xreal_0(sK960_skl)
& v1_xreal_0(sK960_skl)
& v1_xcmplx_0(sK960_skl)
& ~ v1_xboole_0(sK960_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK960_skl]),skolemize(A,sK960_skl)],[f3065]) ).
fof(f22905,plain,
v1_xreal_0(sK960_skl),
inference(cnf_transformation,[status(thm)],[f22902]) ).
fof(f40770,plain,
! [A,B,C] :
( ( m1_group_2(k9_group_2(A,B,C),A)
& v1_group_1(k9_group_2(A,B,C)) )
| ~ m1_group_2(C,A)
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8911]) ).
fof(f40771,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X0)
| v1_group_1(k9_group_2(X0,X2,X1))
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[status(thm)],[f40770]) ).
fof(f40772,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X2,X0)
| m1_group_2(k9_group_2(X0,X1,X2),X0)
| ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[status(thm)],[f40770]) ).
fof(f47654,plain,
( v3_realset2(sK3076_skl)
& v4_group_1(sK3076_skl)
& v3_group_1(sK3076_skl)
& v2_group_1(sK3076_skl)
& ~ v3_struct_0(sK3076_skl)
& l1_group_1(sK3076_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3076_skl]),skolemize(A,sK3076_skl)],[f11093]) ).
fof(f47655,plain,
l1_group_1(sK3076_skl),
inference(cnf_transformation,[status(thm)],[f47654]) ).
fof(f47656,plain,
~ v3_struct_0(sK3076_skl),
inference(cnf_transformation,[status(thm)],[f47654]) ).
fof(f47658,plain,
v3_group_1(sK3076_skl),
inference(cnf_transformation,[status(thm)],[f47654]) ).
fof(f47659,plain,
v4_group_1(sK3076_skl),
inference(cnf_transformation,[status(thm)],[f47654]) ).
fof(f48275,plain,
( v1_gr_cy_1(sK3116_skl)
& v4_group_1(sK3116_skl)
& v3_group_1(sK3116_skl)
& v2_group_1(sK3116_skl)
& v1_group_1(sK3116_skl)
& ~ v3_struct_0(sK3116_skl)
& l1_group_1(sK3116_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3116_skl]),skolemize(A,sK3116_skl)],[f11282]) ).
fof(f48276,plain,
l1_group_1(sK3116_skl),
inference(cnf_transformation,[status(thm)],[f48275]) ).
fof(f48277,plain,
~ v3_struct_0(sK3116_skl),
inference(cnf_transformation,[status(thm)],[f48275]) ).
fof(f48278,plain,
v1_group_1(sK3116_skl),
inference(cnf_transformation,[status(thm)],[f48275]) ).
fof(f48280,plain,
v3_group_1(sK3116_skl),
inference(cnf_transformation,[status(thm)],[f48275]) ).
fof(f48281,plain,
v4_group_1(sK3116_skl),
inference(cnf_transformation,[status(thm)],[f48275]) ).
fof(f48434,plain,
v4_group_1(k3_gr_cy_1),
inference(cnf_transformation,[status(thm)],[f11341]) ).
fof(f48436,plain,
l1_group_1(k3_gr_cy_1),
inference(cnf_transformation,[status(thm)],[f11341]) ).
fof(f48446,plain,
v3_group_1(k3_gr_cy_1),
inference(cnf_transformation,[status(thm)],[f11345]) ).
fof(f50989,plain,
( v17_monoid_0(sK3372_skl)
& v16_monoid_0(sK3372_skl)
& v13_monoid_0(sK3372_skl)
& v10_monoid_0(sK3372_skl)
& v2_monoid_0(sK3372_skl)
& v1_monoid_0(sK3372_skl)
& v7_group_1(sK3372_skl)
& v4_group_1(sK3372_skl)
& v2_group_1(sK3372_skl)
& v1_group_1(sK3372_skl)
& ~ v3_struct_0(sK3372_skl)
& l1_group_1(sK3372_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3372_skl]),skolemize(A,sK3372_skl)],[f11937]) ).
fof(f50990,plain,
l1_group_1(sK3372_skl),
inference(cnf_transformation,[status(thm)],[f50989]) ).
fof(f50991,plain,
~ v3_struct_0(sK3372_skl),
inference(cnf_transformation,[status(thm)],[f50989]) ).
fof(f50992,plain,
v1_group_1(sK3372_skl),
inference(cnf_transformation,[status(thm)],[f50989]) ).
fof(f50994,plain,
v4_group_1(sK3372_skl),
inference(cnf_transformation,[status(thm)],[f50989]) ).
fof(f51035,plain,
( v17_monoid_0(sK3373_skl)
& v16_monoid_0(sK3373_skl)
& v15_monoid_0(sK3373_skl)
& v14_monoid_0(sK3373_skl)
& v13_monoid_0(sK3373_skl)
& v12_monoid_0(sK3373_skl)
& v11_monoid_0(sK3373_skl)
& v10_monoid_0(sK3373_skl)
& v2_monoid_0(sK3373_skl)
& v1_monoid_0(sK3373_skl)
& v1_vectsp_2(sK3373_skl)
& v8_vectsp_1(sK3373_skl)
& v6_vectsp_1(sK3373_skl)
& v1_vectsp_1(sK3373_skl)
& v7_group_1(sK3373_skl)
& v4_group_1(sK3373_skl)
& v3_group_1(sK3373_skl)
& v2_group_1(sK3373_skl)
& ~ v3_struct_0(sK3373_skl)
& l1_vectsp_1(sK3373_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3373_skl]),skolemize(A,sK3373_skl)],[f11947]) ).
fof(f51037,plain,
~ v3_struct_0(sK3373_skl),
inference(cnf_transformation,[status(thm)],[f51035]) ).
fof(f51039,plain,
v3_group_1(sK3373_skl),
inference(cnf_transformation,[status(thm)],[f51035]) ).
fof(f51822,plain,
~ v3_struct_0(k5_monoid_0),
inference(cnf_transformation,[status(thm)],[f12141]) ).
fof(f51823,plain,
v1_group_1(k5_monoid_0),
inference(cnf_transformation,[status(thm)],[f12141]) ).
fof(f51825,plain,
v4_group_1(k5_monoid_0),
inference(cnf_transformation,[status(thm)],[f12141]) ).
fof(f51829,plain,
l1_group_1(k5_monoid_0),
inference(cnf_transformation,[status(thm)],[f12141]) ).
fof(f51830,plain,
~ v3_struct_0(k6_monoid_0),
inference(cnf_transformation,[status(thm)],[f12142]) ).
fof(f51831,plain,
v1_group_1(k6_monoid_0),
inference(cnf_transformation,[status(thm)],[f12142]) ).
fof(f51835,plain,
k6_monoid_0 = k3_gr_cy_1,
inference(cnf_transformation,[status(thm)],[f12143]) ).
fof(f51845,plain,
~ v3_struct_0(k9_monoid_0),
inference(cnf_transformation,[status(thm)],[f12146]) ).
fof(f51846,plain,
v1_group_1(k9_monoid_0),
inference(cnf_transformation,[status(thm)],[f12146]) ).
fof(f51848,plain,
v4_group_1(k9_monoid_0),
inference(cnf_transformation,[status(thm)],[f12146]) ).
fof(f51850,plain,
l1_group_1(k9_monoid_0),
inference(cnf_transformation,[status(thm)],[f12146]) ).
fof(f55884,plain,
( v6_quantal1(sK3781_skl)
& v5_quantal1(sK3781_skl)
& v4_quantal1(sK3781_skl)
& ~ v3_struct_0(sK3781_skl)
& l1_group_1(sK3781_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3781_skl]),skolemize(A,sK3781_skl)],[f13120]) ).
fof(f55886,plain,
~ v3_struct_0(sK3781_skl),
inference(cnf_transformation,[status(thm)],[f55884]) ).
fof(f55893,plain,
( v8_quantal1(sK3782_skl)
& v7_quantal1(sK3782_skl)
& v6_quantal1(sK3782_skl)
& v5_quantal1(sK3782_skl)
& v4_quantal1(sK3782_skl)
& v7_group_1(sK3782_skl)
& v4_group_1(sK3782_skl)
& v2_group_1(sK3782_skl)
& v4_lattice3(sK3782_skl)
& v10_lattices(sK3782_skl)
& v9_lattices(sK3782_skl)
& v8_lattices(sK3782_skl)
& v7_lattices(sK3782_skl)
& v6_lattices(sK3782_skl)
& v5_lattices(sK3782_skl)
& v4_lattices(sK3782_skl)
& ~ v3_struct_0(sK3782_skl)
& l1_quantal1(sK3782_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3782_skl]),skolemize(A,sK3782_skl)],[f13122]) ).
fof(f55895,plain,
~ v3_struct_0(sK3782_skl),
inference(cnf_transformation,[status(thm)],[f55893]) ).
fof(f55938,plain,
( v10_quantal1(sK3784_skl)
& v9_quantal1(sK3784_skl)
& v8_quantal1(sK3784_skl)
& v7_quantal1(sK3784_skl)
& v6_quantal1(sK3784_skl)
& v5_quantal1(sK3784_skl)
& v4_quantal1(sK3784_skl)
& v7_group_1(sK3784_skl)
& v4_group_1(sK3784_skl)
& v2_group_1(sK3784_skl)
& v4_lattice3(sK3784_skl)
& v10_lattices(sK3784_skl)
& v9_lattices(sK3784_skl)
& v8_lattices(sK3784_skl)
& v7_lattices(sK3784_skl)
& v6_lattices(sK3784_skl)
& v5_lattices(sK3784_skl)
& v4_lattices(sK3784_skl)
& ~ v3_struct_0(sK3784_skl)
& l2_quantal1(sK3784_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3784_skl]),skolemize(A,sK3784_skl)],[f13126]) ).
fof(f55940,plain,
~ v3_struct_0(sK3784_skl),
inference(cnf_transformation,[status(thm)],[f55938]) ).
fof(f55979,plain,
( v21_quantal1(sK3788_skl)
& v20_quantal1(sK3788_skl)
& v19_quantal1(sK3788_skl)
& v10_quantal1(sK3788_skl)
& v9_quantal1(sK3788_skl)
& v8_quantal1(sK3788_skl)
& v7_quantal1(sK3788_skl)
& v7_group_1(sK3788_skl)
& v4_group_1(sK3788_skl)
& v2_group_1(sK3788_skl)
& v4_lattice3(sK3788_skl)
& v10_lattices(sK3788_skl)
& v9_lattices(sK3788_skl)
& v8_lattices(sK3788_skl)
& v7_lattices(sK3788_skl)
& v6_lattices(sK3788_skl)
& v5_lattices(sK3788_skl)
& v4_lattices(sK3788_skl)
& ~ v3_struct_0(sK3788_skl)
& l3_quantal1(sK3788_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3788_skl]),skolemize(A,sK3788_skl)],[f13131]) ).
fof(f55981,plain,
~ v3_struct_0(sK3788_skl),
inference(cnf_transformation,[status(thm)],[f55979]) ).
fof(f59522,plain,
! [A] :
( ( m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(k1_latsubgr(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13961]) ).
fof(f59523,plain,
! [X0] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| v1_funct_1(k1_latsubgr(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[status(thm)],[f59522]) ).
fof(f59524,plain,
! [X0] :
( v3_struct_0(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[status(thm)],[f59522]) ).
fof(f59525,plain,
! [X0] :
( ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X0)
| m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[status(thm)],[f59522]) ).
fof(f59570,plain,
! [A] :
( ! [B] :
( ( B = k1_latsubgr(A)
<=> ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13978]) ).
fof(f59571,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( k1_funct_1(B,C) != u1_struct_0(C)
& m1_group_2(C,A)
& v1_group_1(C) )
| B = k1_latsubgr(A) )
& ( ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| B != k1_latsubgr(A) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f59570]) ).
fof(f59572,plain,
! [A] :
( ! [B] :
( ( ( ( k1_funct_1(B,sK4178_skl(B,A)) != u1_struct_0(sK4178_skl(B,A))
& m1_group_2(sK4178_skl(B,A),A)
& v1_group_1(sK4178_skl(B,A)) )
| B = k1_latsubgr(A) )
& ( ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| B != k1_latsubgr(A) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4178_skl]),skolemize(C,sK4178_skl(B,A))],[f59571]) ).
fof(f59573,plain,
! [X0,X1,X2] :
( k1_funct_1(X1,X2) = u1_struct_0(X2)
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| X1 != k1_latsubgr(X0)
| ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f59572]) ).
fof(f59589,plain,
! [A] :
( ! [B] :
( ! [C] :
( u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C))
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| ~ m1_group_2(B,A)
| ~ v1_group_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13987]) ).
fof(f59590,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X0,X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| v3_struct_0(X1)
| k3_xboole_0(k1_funct_1(k1_latsubgr(X1),X0),k1_funct_1(k1_latsubgr(X1),X2)) = u1_struct_0(k9_group_2(X1,X0,X2))
| ~ l1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v1_group_1(X0) ),
inference(cnf_transformation,[status(thm)],[f59589]) ).
fof(f59591,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) != k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C))
& m1_group_2(C,A)
& v1_group_1(C) )
& m1_group_2(B,A)
& v1_group_1(B) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13989]) ).
fof(f59592,plain,
( k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) != k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4181_skl))
& m1_group_2(sK4181_skl,sK4179_skl)
& v1_group_1(sK4181_skl)
& m1_group_2(sK4180_skl,sK4179_skl)
& v1_group_1(sK4180_skl)
& l1_group_1(sK4179_skl)
& v4_group_1(sK4179_skl)
& v3_group_1(sK4179_skl)
& ~ v3_struct_0(sK4179_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4179_skl,sK4180_skl,sK4181_skl]),skolemize(A,sK4179_skl),skolemize(B,sK4180_skl),skolemize(C,sK4181_skl)],[f59591]) ).
fof(f59593,plain,
~ v3_struct_0(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59594,plain,
v3_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59595,plain,
v4_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59596,plain,
l1_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59597,plain,
v1_group_1(sK4180_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59598,plain,
m1_group_2(sK4180_skl,sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59599,plain,
v1_group_1(sK4181_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59600,plain,
m1_group_2(sK4181_skl,sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f59601,plain,
k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) != k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4181_skl)),
inference(cnf_transformation,[status(thm)],[f59592]) ).
fof(f64586,definition,
! [X1] :
( sQ445_spl
<=> ~ v1_xreal_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f64587,plain,
! [X0] :
( ~ sQ445_spl
| ~ v1_xreal_0(X0) ),
inference(component_clause,[status(thm)],[f64586]) ).
fof(f68243,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_group_1(X0)
| ~ v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_group_1(X1)
| v3_struct_0(X0)
| k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v1_funct_1(k1_latsubgr(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f59573]) ).
fof(f70795,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(paramodulation,[status(thm)],[f14203,f14249]) ).
fof(f70796,plain,
! [X0] : r1_tarski(X0,X0),
inference(paramodulation,[status(thm)],[f14200,f14249]) ).
fof(f71238,plain,
! [X0,X1,X2] : r1_tarski(k4_xboole_0(k3_xboole_0(X0,X1),X2),X0),
inference(paramodulation,[status(thm)],[f14308,f14249]) ).
fof(f71487,plain,
! [X0,X1] : r1_tarski(k4_xboole_0(X0,X1),X0),
inference(paramodulation,[status(thm)],[f14260,f71238]) ).
fof(f72925,definition,
( sQ1256_spl
<=> v1_funct_1(k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1256_spl])],[split_symbol_definition]) ).
fof(f72927,plain,
( sQ1256_spl
| ~ v1_funct_1(k1_xboole_0) ),
inference(component_clause,[status(thm)],[f72925]) ).
fof(f72994,plain,
! [X0,X1] :
( ~ v1_group_1(X1)
| ~ v4_group_1(sK4179_skl)
| u1_struct_0(k9_group_2(sK4179_skl,X1,X0)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),X1),k1_funct_1(k1_latsubgr(sK4179_skl),X0))
| v3_struct_0(sK4179_skl)
| ~ m1_group_2(X1,sK4179_skl)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK4179_skl)
| ~ v3_group_1(sK4179_skl) ),
inference(resolution,[status(thm)],[f59590,f59596]) ).
fof(f72995,definition,
( sQ1257_spl
<=> v3_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1257_spl])],[split_symbol_definition]) ).
fof(f72997,plain,
( sQ1257_spl
| ~ v3_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f72995]) ).
fof(f72998,definition,
! [X0,X1] :
( sQ1258_spl
<=> ( ~ v1_group_1(X1)
| u1_struct_0(k9_group_2(sK4179_skl,X1,X0)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),X1),k1_funct_1(k1_latsubgr(sK4179_skl),X0))
| ~ m1_group_2(X1,sK4179_skl)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1258_spl])],[split_symbol_definition]) ).
fof(f72999,plain,
! [X0,X1] :
( ~ sQ1258_spl
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK4179_skl)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK4179_skl)
| k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),X0),k1_funct_1(k1_latsubgr(sK4179_skl),X1)) = u1_struct_0(k9_group_2(sK4179_skl,X0,X1)) ),
inference(component_clause,[status(thm)],[f72998]) ).
fof(f73001,definition,
( sQ1259_spl
<=> v3_struct_0(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1259_spl])],[split_symbol_definition]) ).
fof(f73002,plain,
( ~ sQ1259_spl
| v3_struct_0(sK4179_skl) ),
inference(component_clause,[status(thm)],[f73001]) ).
fof(f73004,definition,
( sQ1260_spl
<=> l1_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1260_spl])],[split_symbol_definition]) ).
fof(f73006,plain,
( sQ1260_spl
| ~ l1_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f73004]) ).
fof(f73008,definition,
( sQ1261_spl
<=> v4_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1261_spl])],[split_symbol_definition]) ).
fof(f73010,plain,
( sQ1261_spl
| ~ v4_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f73008]) ).
fof(f73011,plain,
( ~ sQ1261_spl
| sQ1259_spl
| sQ1258_spl
| ~ sQ1257_spl ),
inference(split_clause,[status(thm)],[f72994,f72995,f72998,f73001,f73008]) ).
fof(f73012,plain,
( sQ1261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73010,f59595]) ).
fof(f73013,plain,
sQ1261_spl,
inference(contradiction_clause,[status(thm)],[f73012]) ).
fof(f73014,plain,
( sQ1260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73006,f59596]) ).
fof(f73015,plain,
sQ1260_spl,
inference(contradiction_clause,[status(thm)],[f73014]) ).
fof(f73016,plain,
( ~ sQ1259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73002,f59593]) ).
fof(f73017,plain,
~ sQ1259_spl,
inference(contradiction_clause,[status(thm)],[f73016]) ).
fof(f73018,plain,
( sQ1257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f72997,f59594]) ).
fof(f73019,plain,
sQ1257_spl,
inference(contradiction_clause,[status(thm)],[f73018]) ).
fof(f73025,plain,
! [X0] :
( ~ sQ1258_spl
| ~ v1_group_1(sK4180_skl)
| ~ m1_group_2(X0,sK4179_skl)
| k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),X0)) = u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,X0))
| ~ v1_group_1(X0) ),
inference(resolution,[status(thm)],[f72999,f59598]) ).
fof(f73027,definition,
! [X0] :
( sQ1262_spl
<=> ( ~ m1_group_2(X0,sK4179_skl)
| k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),X0)) = u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,X0))
| ~ v1_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1262_spl])],[split_symbol_definition]) ).
fof(f73028,plain,
! [X0] :
( ~ sQ1262_spl
| u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,X0)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),X0))
| ~ m1_group_2(X0,sK4179_skl)
| ~ v1_group_1(X0) ),
inference(component_clause,[status(thm)],[f73027]) ).
fof(f73030,definition,
( sQ1263_spl
<=> v1_group_1(sK4180_skl) ),
introduced(definition,[new_symbols(definition,[sQ1263_spl])],[split_symbol_definition]) ).
fof(f73032,plain,
( sQ1263_spl
| ~ v1_group_1(sK4180_skl) ),
inference(component_clause,[status(thm)],[f73030]) ).
fof(f73033,plain,
( ~ sQ1258_spl
| ~ sQ1263_spl
| sQ1262_spl ),
inference(split_clause,[status(thm)],[f73025,f73027,f73030,f72998]) ).
fof(f73037,definition,
( sQ1265_spl
<=> v1_group_1(sK4181_skl) ),
introduced(definition,[new_symbols(definition,[sQ1265_spl])],[split_symbol_definition]) ).
fof(f73039,plain,
( sQ1265_spl
| ~ v1_group_1(sK4181_skl) ),
inference(component_clause,[status(thm)],[f73037]) ).
fof(f73041,plain,
( sQ1263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73032,f59597]) ).
fof(f73042,plain,
sQ1263_spl,
inference(contradiction_clause,[status(thm)],[f73041]) ).
fof(f73043,plain,
( sQ1265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73039,f59599]) ).
fof(f73044,plain,
sQ1265_spl,
inference(contradiction_clause,[status(thm)],[f73043]) ).
fof(f73046,plain,
( ~ sQ1262_spl
| ~ v1_group_1(sK4181_skl)
| u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4181_skl)) ),
inference(resolution,[status(thm)],[f73028,f59600]) ).
fof(f73051,definition,
( sQ1267_spl
<=> u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4181_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition]) ).
fof(f73052,plain,
( ~ sQ1267_spl
| u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4181_skl)) ),
inference(component_clause,[status(thm)],[f73051]) ).
fof(f73054,plain,
( ~ sQ1262_spl
| ~ sQ1265_spl
| sQ1267_spl ),
inference(split_clause,[status(thm)],[f73046,f73051,f73037,f73027]) ).
fof(f73250,plain,
( ~ sQ1267_spl
| k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) != u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
inference(backward_demodulation,[status(thm)],[f73052,f59601]) ).
fof(f73585,plain,
! [X0,X1] :
( v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v1_group_1(X0)
| u1_struct_0(X0) = k1_funct_1(k1_latsubgr(X1),X0)
| ~ m2_relset_1(k1_latsubgr(X1),k1_group_3(X1),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(k1_latsubgr(X1))
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f68243,f59524]) ).
fof(f73594,plain,
( ~ v4_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| m2_relset_1(k1_latsubgr(sK4179_skl),k1_group_3(sK4179_skl),k1_zfmisc_1(u1_struct_0(sK4179_skl)))
| ~ v3_group_1(sK4179_skl) ),
inference(resolution,[status(thm)],[f59525,f59596]) ).
fof(f73596,definition,
( sQ1277_spl
<=> m2_relset_1(k1_latsubgr(sK4179_skl),k1_group_3(sK4179_skl),k1_zfmisc_1(u1_struct_0(sK4179_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1277_spl])],[split_symbol_definition]) ).
fof(f73597,plain,
( ~ sQ1277_spl
| m2_relset_1(k1_latsubgr(sK4179_skl),k1_group_3(sK4179_skl),k1_zfmisc_1(u1_struct_0(sK4179_skl))) ),
inference(component_clause,[status(thm)],[f73596]) ).
fof(f73599,plain,
( ~ sQ1261_spl
| sQ1259_spl
| sQ1277_spl
| ~ sQ1257_spl ),
inference(split_clause,[status(thm)],[f73594,f72995,f73596,f73001,f73008]) ).
fof(f73867,definition,
( sQ1284_spl
<=> m1_group_2(sK4181_skl,sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1284_spl])],[split_symbol_definition]) ).
fof(f73869,plain,
( sQ1284_spl
| ~ m1_group_2(sK4181_skl,sK4179_skl) ),
inference(component_clause,[status(thm)],[f73867]) ).
fof(f73882,plain,
( sQ1284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f73869,f59600]) ).
fof(f73883,plain,
sQ1284_spl,
inference(contradiction_clause,[status(thm)],[f73882]) ).
fof(f74161,definition,
( sQ1297_spl
<=> m1_group_2(sK4180_skl,sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1297_spl])],[split_symbol_definition]) ).
fof(f74163,plain,
( sQ1297_spl
| ~ m1_group_2(sK4180_skl,sK4179_skl) ),
inference(component_clause,[status(thm)],[f74161]) ).
fof(f74178,plain,
( sQ1297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f74163,f59598]) ).
fof(f74179,plain,
sQ1297_spl,
inference(contradiction_clause,[status(thm)],[f74178]) ).
fof(f74207,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK4179_skl)
| m1_group_2(k9_group_2(sK4179_skl,X0,X1),sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v3_group_1(sK4179_skl) ),
inference(resolution,[status(thm)],[f40772,f59596]) ).
fof(f74208,definition,
! [X0,X1] :
( sQ1306_spl
<=> ( ~ m1_group_2(X1,sK4179_skl)
| m1_group_2(k9_group_2(sK4179_skl,X0,X1),sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1306_spl])],[split_symbol_definition]) ).
fof(f74209,plain,
! [X0,X1] :
( ~ sQ1306_spl
| m1_group_2(k9_group_2(sK4179_skl,X1,X0),sK4179_skl)
| ~ m1_group_2(X1,sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f74208]) ).
fof(f74212,plain,
( ~ sQ1261_spl
| sQ1306_spl
| sQ1259_spl
| ~ sQ1257_spl ),
inference(split_clause,[status(thm)],[f74207,f72995,f73001,f74208,f73008]) ).
fof(f74220,plain,
( sQ1256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16829,f72927]) ).
fof(f74221,plain,
sQ1256_spl,
inference(contradiction_clause,[status(thm)],[f74220]) ).
fof(f74461,plain,
! [X0] :
( ~ sQ1306_spl
| m1_group_2(k9_group_2(sK4179_skl,X0,sK4181_skl),sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl) ),
inference(resolution,[status(thm)],[f74209,f59600]) ).
fof(f74570,definition,
! [X0] :
( sQ1343_spl
<=> X0 != k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ1343_spl])],[split_symbol_definition]) ).
fof(f74571,plain,
! [X0] :
( ~ sQ1343_spl
| X0 != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f74570]) ).
fof(f74574,plain,
( ~ sQ1343_spl
| $false ),
inference(destructive_equality_resolution,[status(thm)],[f74571]) ).
fof(f74575,plain,
~ sQ1343_spl,
inference(contradiction_clause,[status(thm)],[f74574]) ).
fof(f75404,definition,
( sQ1423_spl
<=> u1_struct_0(sK4179_skl) = u1_struct_0(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1423_spl])],[split_symbol_definition]) ).
fof(f75406,plain,
( sQ1423_spl
| u1_struct_0(sK4179_skl) != u1_struct_0(sK4179_skl) ),
inference(component_clause,[status(thm)],[f75404]) ).
fof(f75415,plain,
( sQ1423_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f75406]) ).
fof(f75416,plain,
sQ1423_spl,
inference(contradiction_clause,[status(thm)],[f75415]) ).
fof(f76057,plain,
( ~ sQ445_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22905,f64587]) ).
fof(f76058,plain,
~ sQ445_spl,
inference(contradiction_clause,[status(thm)],[f76057]) ).
fof(f77265,definition,
( sQ1440_spl
<=> v3_struct_0(sK3788_skl) ),
introduced(definition,[new_symbols(definition,[sQ1440_spl])],[split_symbol_definition]) ).
fof(f77266,plain,
( ~ sQ1440_spl
| v3_struct_0(sK3788_skl) ),
inference(component_clause,[status(thm)],[f77265]) ).
fof(f78201,definition,
! [X0] :
( sQ1459_spl
<=> ~ r1_tarski(X0,k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1459_spl])],[split_symbol_definition]) ).
fof(f78202,plain,
! [X0] :
( ~ sQ1459_spl
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(component_clause,[status(thm)],[f78201]) ).
fof(f78235,definition,
( sQ1464_spl
<=> v3_struct_0(sK3784_skl) ),
introduced(definition,[new_symbols(definition,[sQ1464_spl])],[split_symbol_definition]) ).
fof(f78236,plain,
( ~ sQ1464_spl
| v3_struct_0(sK3784_skl) ),
inference(component_clause,[status(thm)],[f78235]) ).
fof(f78725,plain,
( ~ sQ1459_spl
| $false ),
inference(resolution,[status(thm)],[f78202,f71487]) ).
fof(f78738,plain,
~ sQ1459_spl,
inference(contradiction_clause,[status(thm)],[f78725]) ).
fof(f78739,plain,
( ~ sQ1440_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55981,f77266]) ).
fof(f78740,plain,
~ sQ1440_spl,
inference(contradiction_clause,[status(thm)],[f78739]) ).
fof(f78835,plain,
( ~ sQ1464_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55940,f78236]) ).
fof(f78836,plain,
~ sQ1464_spl,
inference(contradiction_clause,[status(thm)],[f78835]) ).
fof(f79050,definition,
( sQ1487_spl
<=> v3_struct_0(sK3782_skl) ),
introduced(definition,[new_symbols(definition,[sQ1487_spl])],[split_symbol_definition]) ).
fof(f79051,plain,
( ~ sQ1487_spl
| v3_struct_0(sK3782_skl) ),
inference(component_clause,[status(thm)],[f79050]) ).
fof(f79703,plain,
! [X0,X1] :
( ~ m1_group_2(X0,X1)
| ~ v3_group_1(X1)
| k1_funct_1(k1_latsubgr(X1),X0) = u1_struct_0(X0)
| ~ l1_group_1(X1)
| v3_struct_0(X1)
| ~ v4_group_1(X1)
| ~ m2_relset_1(k1_latsubgr(X1),k1_group_3(X1),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_group_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f73585,f59523]) ).
fof(f79704,plain,
! [X0] :
( ~ sQ1277_spl
| ~ m1_group_2(X0,sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| k1_funct_1(k1_latsubgr(sK4179_skl),X0) = u1_struct_0(X0)
| ~ l1_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v1_group_1(X0) ),
inference(resolution,[status(thm)],[f79703,f73597]) ).
fof(f79705,definition,
! [X0] :
( sQ1511_spl
<=> ( ~ m1_group_2(X0,sK4179_skl)
| k1_funct_1(k1_latsubgr(sK4179_skl),X0) = u1_struct_0(X0)
| ~ v1_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1511_spl])],[split_symbol_definition]) ).
fof(f79706,plain,
! [X0] :
( ~ sQ1511_spl
| ~ m1_group_2(X0,sK4179_skl)
| u1_struct_0(X0) = k1_funct_1(k1_latsubgr(sK4179_skl),X0)
| ~ v1_group_1(X0) ),
inference(component_clause,[status(thm)],[f79705]) ).
fof(f79708,plain,
( ~ sQ1277_spl
| ~ sQ1257_spl
| ~ sQ1260_spl
| sQ1259_spl
| ~ sQ1261_spl
| sQ1511_spl ),
inference(split_clause,[status(thm)],[f79704,f79705,f73008,f73001,f73004,f72995,f73596]) ).
fof(f80672,definition,
( sQ1520_spl
<=> v3_struct_0(sK3781_skl) ),
introduced(definition,[new_symbols(definition,[sQ1520_spl])],[split_symbol_definition]) ).
fof(f80673,plain,
( ~ sQ1520_spl
| v3_struct_0(sK3781_skl) ),
inference(component_clause,[status(thm)],[f80672]) ).
fof(f80727,plain,
( ~ sQ1520_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f80673,f55886]) ).
fof(f80728,plain,
~ sQ1520_spl,
inference(contradiction_clause,[status(thm)],[f80727]) ).
fof(f80957,plain,
( ~ sQ1487_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55895,f79051]) ).
fof(f80958,plain,
~ sQ1487_spl,
inference(contradiction_clause,[status(thm)],[f80957]) ).
fof(f83110,definition,
! [X0] :
( sQ1569_spl
<=> ~ r1_tarski(k1_xboole_0,X0) ),
introduced(definition,[new_symbols(definition,[sQ1569_spl])],[split_symbol_definition]) ).
fof(f83111,plain,
! [X0] :
( ~ sQ1569_spl
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f83110]) ).
fof(f83117,plain,
( ~ sQ1569_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f83111,f70795]) ).
fof(f83118,plain,
~ sQ1569_spl,
inference(contradiction_clause,[status(thm)],[f83117]) ).
fof(f84555,plain,
v1_group_1(k3_gr_cy_1),
inference(forward_demodulation,[status(thm)],[f51835,f51831]) ).
fof(f84639,definition,
( sQ1575_spl
<=> v3_struct_0(k5_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1575_spl])],[split_symbol_definition]) ).
fof(f84640,plain,
( ~ sQ1575_spl
| v3_struct_0(k5_monoid_0) ),
inference(component_clause,[status(thm)],[f84639]) ).
fof(f84642,definition,
( sQ1576_spl
<=> l1_group_1(k5_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1576_spl])],[split_symbol_definition]) ).
fof(f84644,plain,
( sQ1576_spl
| ~ l1_group_1(k5_monoid_0) ),
inference(component_clause,[status(thm)],[f84642]) ).
fof(f84704,definition,
( sQ1592_spl
<=> v1_group_1(k5_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1592_spl])],[split_symbol_definition]) ).
fof(f84706,plain,
( sQ1592_spl
| ~ v1_group_1(k5_monoid_0) ),
inference(component_clause,[status(thm)],[f84704]) ).
fof(f84716,plain,
( ~ sQ1575_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f84640,f51822]) ).
fof(f84717,plain,
~ sQ1575_spl,
inference(contradiction_clause,[status(thm)],[f84716]) ).
fof(f84738,definition,
( sQ1597_spl
<=> v3_struct_0(k9_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1597_spl])],[split_symbol_definition]) ).
fof(f84739,plain,
( ~ sQ1597_spl
| v3_struct_0(k9_monoid_0) ),
inference(component_clause,[status(thm)],[f84738]) ).
fof(f84741,definition,
( sQ1598_spl
<=> v4_group_1(k9_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1598_spl])],[split_symbol_definition]) ).
fof(f84743,plain,
( sQ1598_spl
| ~ v4_group_1(k9_monoid_0) ),
inference(component_clause,[status(thm)],[f84741]) ).
fof(f84865,plain,
( ~ sQ1306_spl
| m1_group_2(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl),sK4179_skl) ),
inference(resolution,[status(thm)],[f74461,f59598]) ).
fof(f84888,plain,
( sQ1576_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51829,f84644]) ).
fof(f84889,plain,
sQ1576_spl,
inference(contradiction_clause,[status(thm)],[f84888]) ).
fof(f84907,definition,
( sQ1612_spl
<=> l1_group_1(k9_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1612_spl])],[split_symbol_definition]) ).
fof(f84909,plain,
( sQ1612_spl
| ~ l1_group_1(k9_monoid_0) ),
inference(component_clause,[status(thm)],[f84907]) ).
fof(f84917,definition,
( sQ1615_spl
<=> v1_group_1(k9_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1615_spl])],[split_symbol_definition]) ).
fof(f84919,plain,
( sQ1615_spl
| ~ v1_group_1(k9_monoid_0) ),
inference(component_clause,[status(thm)],[f84917]) ).
fof(f84960,plain,
( sQ1612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f84909,f51850]) ).
fof(f84961,plain,
sQ1612_spl,
inference(contradiction_clause,[status(thm)],[f84960]) ).
fof(f84962,plain,
( sQ1615_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f84919,f51846]) ).
fof(f84963,plain,
sQ1615_spl,
inference(contradiction_clause,[status(thm)],[f84962]) ).
fof(f84974,plain,
( sQ1598_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f84743,f51848]) ).
fof(f84975,plain,
sQ1598_spl,
inference(contradiction_clause,[status(thm)],[f84974]) ).
fof(f84976,plain,
~ v3_struct_0(k3_gr_cy_1),
inference(forward_demodulation,[status(thm)],[f51835,f51830]) ).
fof(f84978,plain,
( ~ sQ1597_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f84739,f51845]) ).
fof(f84979,plain,
~ sQ1597_spl,
inference(contradiction_clause,[status(thm)],[f84978]) ).
fof(f85016,definition,
( sQ1630_spl
<=> v4_group_1(k5_monoid_0) ),
introduced(definition,[new_symbols(definition,[sQ1630_spl])],[split_symbol_definition]) ).
fof(f85018,plain,
( sQ1630_spl
| ~ v4_group_1(k5_monoid_0) ),
inference(component_clause,[status(thm)],[f85016]) ).
fof(f85042,plain,
( sQ1630_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f85018,f51825]) ).
fof(f85043,plain,
sQ1630_spl,
inference(contradiction_clause,[status(thm)],[f85042]) ).
fof(f85084,plain,
( sQ1592_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51823,f84706]) ).
fof(f85085,plain,
sQ1592_spl,
inference(contradiction_clause,[status(thm)],[f85084]) ).
fof(f85963,definition,
( sQ1643_spl
<=> v3_struct_0(sK3373_skl) ),
introduced(definition,[new_symbols(definition,[sQ1643_spl])],[split_symbol_definition]) ).
fof(f85964,plain,
( ~ sQ1643_spl
| v3_struct_0(sK3373_skl) ),
inference(component_clause,[status(thm)],[f85963]) ).
fof(f85966,definition,
( sQ1644_spl
<=> v3_group_1(sK3373_skl) ),
introduced(definition,[new_symbols(definition,[sQ1644_spl])],[split_symbol_definition]) ).
fof(f85968,plain,
( sQ1644_spl
| ~ v3_group_1(sK3373_skl) ),
inference(component_clause,[status(thm)],[f85966]) ).
fof(f86034,plain,
( ~ sQ1643_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f85964,f51037]) ).
fof(f86035,plain,
~ sQ1643_spl,
inference(contradiction_clause,[status(thm)],[f86034]) ).
fof(f86676,plain,
( sQ1644_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51039,f85968]) ).
fof(f86677,plain,
sQ1644_spl,
inference(contradiction_clause,[status(thm)],[f86676]) ).
fof(f87537,definition,
( sQ1666_spl
<=> v3_struct_0(sK3372_skl) ),
introduced(definition,[new_symbols(definition,[sQ1666_spl])],[split_symbol_definition]) ).
fof(f87538,plain,
( ~ sQ1666_spl
| v3_struct_0(sK3372_skl) ),
inference(component_clause,[status(thm)],[f87537]) ).
fof(f87540,definition,
( sQ1667_spl
<=> l1_group_1(sK3372_skl) ),
introduced(definition,[new_symbols(definition,[sQ1667_spl])],[split_symbol_definition]) ).
fof(f87542,plain,
( sQ1667_spl
| ~ l1_group_1(sK3372_skl) ),
inference(component_clause,[status(thm)],[f87540]) ).
fof(f87583,definition,
( sQ1678_spl
<=> v1_group_1(sK3372_skl) ),
introduced(definition,[new_symbols(definition,[sQ1678_spl])],[split_symbol_definition]) ).
fof(f87585,plain,
( sQ1678_spl
| ~ v1_group_1(sK3372_skl) ),
inference(component_clause,[status(thm)],[f87583]) ).
fof(f87611,plain,
( ~ sQ1666_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f87538,f50991]) ).
fof(f87612,plain,
~ sQ1666_spl,
inference(contradiction_clause,[status(thm)],[f87611]) ).
fof(f87619,plain,
( sQ1667_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50990,f87542]) ).
fof(f87620,plain,
sQ1667_spl,
inference(contradiction_clause,[status(thm)],[f87619]) ).
fof(f87644,definition,
( sQ1686_spl
<=> v4_group_1(sK3372_skl) ),
introduced(definition,[new_symbols(definition,[sQ1686_spl])],[split_symbol_definition]) ).
fof(f87646,plain,
( sQ1686_spl
| ~ v4_group_1(sK3372_skl) ),
inference(component_clause,[status(thm)],[f87644]) ).
fof(f87678,plain,
( sQ1686_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f87646,f50994]) ).
fof(f87679,plain,
sQ1686_spl,
inference(contradiction_clause,[status(thm)],[f87678]) ).
fof(f87849,plain,
( sQ1678_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50992,f87585]) ).
fof(f87850,plain,
sQ1678_spl,
inference(contradiction_clause,[status(thm)],[f87849]) ).
fof(f89064,definition,
( sQ1727_spl
<=> v1_group_1(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1727_spl])],[split_symbol_definition]) ).
fof(f89066,plain,
( sQ1727_spl
| ~ v1_group_1(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
inference(component_clause,[status(thm)],[f89064]) ).
fof(f89232,plain,
( sQ1727_spl
| ~ m1_group_2(sK4180_skl,sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| ~ m1_group_2(sK4181_skl,sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(sK4179_skl) ),
inference(resolution,[status(thm)],[f89066,f40771]) ).
fof(f89233,plain,
( sQ1727_spl
| ~ sQ1297_spl
| ~ sQ1257_spl
| ~ sQ1284_spl
| ~ sQ1261_spl
| sQ1259_spl
| ~ sQ1260_spl ),
inference(split_clause,[status(thm)],[f89232,f73004,f73001,f73008,f73867,f72995,f74161,f89064]) ).
fof(f91930,definition,
( sQ1836_spl
<=> v3_struct_0(k3_gr_cy_1) ),
introduced(definition,[new_symbols(definition,[sQ1836_spl])],[split_symbol_definition]) ).
fof(f91931,plain,
( ~ sQ1836_spl
| v3_struct_0(k3_gr_cy_1) ),
inference(component_clause,[status(thm)],[f91930]) ).
fof(f91933,definition,
( sQ1837_spl
<=> l1_group_1(k3_gr_cy_1) ),
introduced(definition,[new_symbols(definition,[sQ1837_spl])],[split_symbol_definition]) ).
fof(f91935,plain,
( sQ1837_spl
| ~ l1_group_1(k3_gr_cy_1) ),
inference(component_clause,[status(thm)],[f91933]) ).
fof(f91936,definition,
( sQ1838_spl
<=> v3_group_1(k3_gr_cy_1) ),
introduced(definition,[new_symbols(definition,[sQ1838_spl])],[split_symbol_definition]) ).
fof(f91938,plain,
( sQ1838_spl
| ~ v3_group_1(k3_gr_cy_1) ),
inference(component_clause,[status(thm)],[f91936]) ).
fof(f91955,definition,
( sQ1843_spl
<=> v1_group_1(k3_gr_cy_1) ),
introduced(definition,[new_symbols(definition,[sQ1843_spl])],[split_symbol_definition]) ).
fof(f91957,plain,
( sQ1843_spl
| ~ v1_group_1(k3_gr_cy_1) ),
inference(component_clause,[status(thm)],[f91955]) ).
fof(f92007,plain,
( ~ sQ1836_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91931,f84976]) ).
fof(f92008,plain,
~ sQ1836_spl,
inference(contradiction_clause,[status(thm)],[f92007]) ).
fof(f92009,plain,
( sQ1843_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91957,f84555]) ).
fof(f92010,plain,
sQ1843_spl,
inference(contradiction_clause,[status(thm)],[f92009]) ).
fof(f92258,definition,
( sQ1858_spl
<=> v4_group_1(k3_gr_cy_1) ),
introduced(definition,[new_symbols(definition,[sQ1858_spl])],[split_symbol_definition]) ).
fof(f92260,plain,
( sQ1858_spl
| ~ v4_group_1(k3_gr_cy_1) ),
inference(component_clause,[status(thm)],[f92258]) ).
fof(f92293,plain,
( sQ1858_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f92260,f48434]) ).
fof(f92294,plain,
sQ1858_spl,
inference(contradiction_clause,[status(thm)],[f92293]) ).
fof(f92296,plain,
( sQ1838_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91938,f48446]) ).
fof(f92297,plain,
sQ1838_spl,
inference(contradiction_clause,[status(thm)],[f92296]) ).
fof(f92298,plain,
( sQ1837_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91935,f48436]) ).
fof(f92299,plain,
sQ1837_spl,
inference(contradiction_clause,[status(thm)],[f92298]) ).
fof(f92395,definition,
( sQ1868_spl
<=> v3_group_1(sK3116_skl) ),
introduced(definition,[new_symbols(definition,[sQ1868_spl])],[split_symbol_definition]) ).
fof(f92397,plain,
( sQ1868_spl
| ~ v3_group_1(sK3116_skl) ),
inference(component_clause,[status(thm)],[f92395]) ).
fof(f92398,definition,
( sQ1869_spl
<=> l1_group_1(sK3116_skl) ),
introduced(definition,[new_symbols(definition,[sQ1869_spl])],[split_symbol_definition]) ).
fof(f92400,plain,
( sQ1869_spl
| ~ l1_group_1(sK3116_skl) ),
inference(component_clause,[status(thm)],[f92398]) ).
fof(f92404,definition,
( sQ1871_spl
<=> v3_struct_0(sK3116_skl) ),
introduced(definition,[new_symbols(definition,[sQ1871_spl])],[split_symbol_definition]) ).
fof(f92405,plain,
( ~ sQ1871_spl
| v3_struct_0(sK3116_skl) ),
inference(component_clause,[status(thm)],[f92404]) ).
fof(f92415,definition,
( sQ1874_spl
<=> v1_group_1(sK3116_skl) ),
introduced(definition,[new_symbols(definition,[sQ1874_spl])],[split_symbol_definition]) ).
fof(f92417,plain,
( sQ1874_spl
| ~ v1_group_1(sK3116_skl) ),
inference(component_clause,[status(thm)],[f92415]) ).
fof(f92475,plain,
( sQ1874_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f92417,f48278]) ).
fof(f92476,plain,
sQ1874_spl,
inference(contradiction_clause,[status(thm)],[f92475]) ).
fof(f92521,plain,
( ~ sQ1871_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48277,f92405]) ).
fof(f92522,plain,
~ sQ1871_spl,
inference(contradiction_clause,[status(thm)],[f92521]) ).
fof(f92793,plain,
( sQ1868_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48280,f92397]) ).
fof(f92794,plain,
sQ1868_spl,
inference(contradiction_clause,[status(thm)],[f92793]) ).
fof(f93214,plain,
( sQ1869_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48276,f92400]) ).
fof(f93215,plain,
sQ1869_spl,
inference(contradiction_clause,[status(thm)],[f93214]) ).
fof(f93236,definition,
( sQ1926_spl
<=> v4_group_1(sK3116_skl) ),
introduced(definition,[new_symbols(definition,[sQ1926_spl])],[split_symbol_definition]) ).
fof(f93238,plain,
( sQ1926_spl
| ~ v4_group_1(sK3116_skl) ),
inference(component_clause,[status(thm)],[f93236]) ).
fof(f93271,plain,
( sQ1926_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f93238,f48281]) ).
fof(f93272,plain,
sQ1926_spl,
inference(contradiction_clause,[status(thm)],[f93271]) ).
fof(f93425,definition,
( sQ1933_spl
<=> v3_group_1(sK3076_skl) ),
introduced(definition,[new_symbols(definition,[sQ1933_spl])],[split_symbol_definition]) ).
fof(f93427,plain,
( sQ1933_spl
| ~ v3_group_1(sK3076_skl) ),
inference(component_clause,[status(thm)],[f93425]) ).
fof(f93428,definition,
( sQ1934_spl
<=> l1_group_1(sK3076_skl) ),
introduced(definition,[new_symbols(definition,[sQ1934_spl])],[split_symbol_definition]) ).
fof(f93430,plain,
( sQ1934_spl
| ~ l1_group_1(sK3076_skl) ),
inference(component_clause,[status(thm)],[f93428]) ).
fof(f93434,definition,
( sQ1936_spl
<=> v3_struct_0(sK3076_skl) ),
introduced(definition,[new_symbols(definition,[sQ1936_spl])],[split_symbol_definition]) ).
fof(f93435,plain,
( ~ sQ1936_spl
| v3_struct_0(sK3076_skl) ),
inference(component_clause,[status(thm)],[f93434]) ).
fof(f93505,plain,
( ~ sQ1936_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f93435,f47656]) ).
fof(f93506,plain,
~ sQ1936_spl,
inference(contradiction_clause,[status(thm)],[f93505]) ).
fof(f93631,plain,
( sQ1934_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f47655,f93430]) ).
fof(f93632,plain,
sQ1934_spl,
inference(contradiction_clause,[status(thm)],[f93631]) ).
fof(f93658,definition,
( sQ1962_spl
<=> v4_group_1(sK3076_skl) ),
introduced(definition,[new_symbols(definition,[sQ1962_spl])],[split_symbol_definition]) ).
fof(f93660,plain,
( sQ1962_spl
| ~ v4_group_1(sK3076_skl) ),
inference(component_clause,[status(thm)],[f93658]) ).
fof(f93689,plain,
( sQ1962_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f93660,f47659]) ).
fof(f93690,plain,
sQ1962_spl,
inference(contradiction_clause,[status(thm)],[f93689]) ).
fof(f93890,plain,
( sQ1933_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f47658,f93427]) ).
fof(f93891,plain,
sQ1933_spl,
inference(contradiction_clause,[status(thm)],[f93890]) ).
fof(f94807,definition,
( sQ2018_spl
<=> r1_tarski(u1_struct_0(sK4180_skl),u1_struct_0(sK4180_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2018_spl])],[split_symbol_definition]) ).
fof(f94809,plain,
( sQ2018_spl
| ~ r1_tarski(u1_struct_0(sK4180_skl),u1_struct_0(sK4180_skl)) ),
inference(component_clause,[status(thm)],[f94807]) ).
fof(f94815,plain,
( sQ2018_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f94809,f70796]) ).
fof(f94816,plain,
sQ2018_spl,
inference(contradiction_clause,[status(thm)],[f94815]) ).
fof(f102089,plain,
( ~ sQ1306_spl
| ~ sQ1511_spl
| u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl))
| ~ v1_group_1(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
inference(resolution,[status(thm)],[f79706,f84865]) ).
fof(f102101,definition,
( sQ2131_spl
<=> u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2131_spl])],[split_symbol_definition]) ).
fof(f102102,plain,
( ~ sQ2131_spl
| u1_struct_0(k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) = k1_funct_1(k1_latsubgr(sK4179_skl),k9_group_2(sK4179_skl,sK4180_skl,sK4181_skl)) ),
inference(component_clause,[status(thm)],[f102101]) ).
fof(f102104,plain,
( ~ sQ1306_spl
| ~ sQ1511_spl
| sQ2131_spl
| ~ sQ1727_spl ),
inference(split_clause,[status(thm)],[f102089,f89064,f102101,f79705,f74208]) ).
fof(f102137,plain,
( ~ sQ2131_spl
| ~ sQ1267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f102102,f73250]) ).
fof(f102138,plain,
( ~ sQ2131_spl
| ~ sQ1267_spl ),
inference(contradiction_clause,[status(thm)],[f102137]) ).
fof(f102139,plain,
$false,
inference(sat_refutation,[status(thm)],[f73011,f73013,f73015,f73017,f73019,f73033,f73042,f73044,f73054,f73599,f73883,f74179,f74212,f74221,f74575,f75416,f76058,f78738,f78740,f78836,f79708,f80728,f80958,f83118,f84717,f84889,f84961,f84963,f84975,f84979,f85043,f85085,f86035,f86677,f87612,f87620,f87679,f87850,f89233,f92008,f92010,f92294,f92297,f92299,f92476,f92522,f92794,f93215,f93272,f93506,f93632,f93690,f93891,f94816,f102104,f102138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP645+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 20:31:15 UTC 2026
% 0.10/0.35 % CPUTime :
% 1.89/2.13 % Drodi V4.1.1
% 166.53/23.00 % Refutation found
% 166.53/23.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 166.53/23.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.27/23.51 % Elapsed time: 23.112840 seconds
% 12.27/23.51 % CPU time: 167.951192 seconds
% 12.27/23.51 % Total memory used: 4.357 GB
% 12.27/23.51 % Net memory used: 4.286 GB
%------------------------------------------------------------------------------