%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 01:02:51 PM UTC 2026
% Result : Theorem 57.50s 7.91s
% Output : CNFRefutation 58.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 15
% Syntax : Number of formulae : 174 ( 47 unt; 0 def)
% Number of atoms : 559 ( 156 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 625 ( 240 ~; 301 |; 60 &)
% ( 3 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-3 aty)
% Number of variables : 181 ( 179 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [A] :
( l2_conlat_1(A)
=> ( v4_conlat_1(A)
=> A = g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k7_conlat_2(A) = g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( l3_conlat_1(B,A)
=> ! [C] :
( ( l3_conlat_1(C,k7_conlat_2(A))
& v6_conlat_1(C,k7_conlat_2(A)) )
=> ( C = k8_conlat_2(A,B)
<=> ( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
& u4_conlat_1(k7_conlat_2(A),C) = u5_conlat_1(A,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l2_conlat_1(k7_conlat_2(A))
& v4_conlat_1(k7_conlat_2(A))
& ~ v3_conlat_1(k7_conlat_2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& ~ v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( l2_conlat_1(A)
=> m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> ! [D,E,F] :
( g2_conlat_1(A,B,C) = g2_conlat_1(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( v1_relat_1(A)
=> k4_relat_1(k4_relat_1(A)) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k6_relset_1(A,B,C) = k4_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k9_conlat_2(A,B) = k8_conlat_2(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,plain,
? [A] :
( ? [B] :
( k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) != B
& l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
& l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f72,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) != sK1_skl
& l3_conlat_1(sK1_skl,sK0_skl)
& v9_conlat_1(sK1_skl,sK0_skl)
& ~ v7_conlat_1(sK1_skl,sK0_skl)
& v6_conlat_1(sK1_skl,sK0_skl)
& l2_conlat_1(sK0_skl)
& v4_conlat_1(sK0_skl)
& ~ v3_conlat_1(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f71]) ).
fof(f73,plain,
~ v3_conlat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
v4_conlat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f75,plain,
l2_conlat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f76,plain,
v6_conlat_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f77,plain,
~ v7_conlat_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f78,plain,
v9_conlat_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f79,plain,
l3_conlat_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f80,plain,
k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) != sK1_skl,
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f81,plain,
! [A] :
( A = g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))
| ~ v4_conlat_1(A)
| ~ l2_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f82,plain,
! [X0] :
( X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))
| ~ v4_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f88,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f87]) ).
fof(f89,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f92,plain,
! [A] :
( k7_conlat_2(A) = g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f93,plain,
! [X0] :
( k7_conlat_2(X0) = g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = k8_conlat_2(A,B)
<=> ( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
& u4_conlat_1(k7_conlat_2(A),C) = u5_conlat_1(A,B) ) )
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A)) )
| ~ l3_conlat_1(B,A) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f95,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( u5_conlat_1(k7_conlat_2(A),C) != u4_conlat_1(A,B)
| u4_conlat_1(k7_conlat_2(A),C) != u5_conlat_1(A,B)
| C = k8_conlat_2(A,B) )
& ( ( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
& u4_conlat_1(k7_conlat_2(A),C) = u5_conlat_1(A,B) )
| C != k8_conlat_2(A,B) ) )
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A)) )
| ~ l3_conlat_1(B,A) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(NNF_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
! [X0,X1,X2] :
( u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1)
| X2 != k8_conlat_2(X0,X1)
| ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1,X2] :
( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
| X2 != k8_conlat_2(X0,X1)
| ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
! [X0,X1,X2] :
( u5_conlat_1(k7_conlat_2(X0),X2) != u4_conlat_1(X0,X1)
| u4_conlat_1(k7_conlat_2(X0),X2) != u5_conlat_1(X0,X1)
| X2 = k8_conlat_2(X0,X1)
| ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f109,plain,
! [A] :
( ( l2_conlat_1(k7_conlat_2(A))
& v4_conlat_1(k7_conlat_2(A))
& ~ v3_conlat_1(k7_conlat_2(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f110,plain,
! [X0] :
( ~ v3_conlat_1(k7_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0] :
( v4_conlat_1(k7_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f112,plain,
! [X0] :
( l2_conlat_1(k7_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f113,plain,
! [A,B] :
( ( l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A)) )
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f114,plain,
! [X0,X1] :
( v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1] :
( l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f116,plain,
! [A,B] :
( ( l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& ~ v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)) )
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f118,plain,
! [X0,X1] :
( ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f119,plain,
! [X0,X1] :
( v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f120,plain,
! [X0,X1] :
( l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f123,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f124,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [A] :
( m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A))
| ~ l2_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f126,plain,
! [X0] :
( m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f152,plain,
! [A,B,C] :
( ! [D,E,F] :
( ( C = F
& B = E
& A = D )
| g2_conlat_1(A,B,C) != g2_conlat_1(D,E,F) )
| ~ m1_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 = X3
| g2_conlat_1(X1,X2,X0) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X4
| g2_conlat_1(X1,X2,X0) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( X0 = X5
| g2_conlat_1(X1,X2,X0) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f160,plain,
! [A] :
( k4_relat_1(k4_relat_1(A)) = A
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f161,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f215,plain,
! [A,B,C] :
( k6_relset_1(A,B,C) = k4_relat_1(C)
| ~ m1_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f216,plain,
! [X0,X1,X2] :
( k6_relset_1(X1,X2,X0) = k4_relat_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f217,plain,
! [A,B] :
( k9_conlat_2(A,B) = k8_conlat_2(A,B)
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f218,plain,
! [X0,X1] :
( k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1)
| ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f220,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f219]) ).
fof(f221,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f247,plain,
! [X0,X1] :
( u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u5_conlat_1(X0,X1)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f96]) ).
fof(f248,plain,
! [X0,X1] :
( u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u4_conlat_1(X0,X1)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f97]) ).
fof(f251,plain,
( sK0_skl = g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))
| ~ v4_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f82,f75]) ).
fof(f252,plain,
sK0_skl = g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f251,f74]) ).
fof(f257,plain,
( v4_conlat_1(k7_conlat_2(sK0_skl))
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f111,f75]) ).
fof(f258,plain,
v4_conlat_1(k7_conlat_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f257,f73]) ).
fof(f261,plain,
( l2_conlat_1(k7_conlat_2(sK0_skl))
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f112,f75]) ).
fof(f262,plain,
l2_conlat_1(k7_conlat_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f261,f73]) ).
fof(f272,plain,
( k7_conlat_2(sK0_skl) = g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)))
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f93,f75]) ).
fof(f274,plain,
k7_conlat_2(sK0_skl) = g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f272,f73]) ).
fof(f275,plain,
( k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl))))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(resolution,[status(thm)],[f262,f93]) ).
fof(f278,plain,
( k7_conlat_2(sK0_skl) = g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))
| ~ v4_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(resolution,[status(thm)],[f262,f82]) ).
fof(f279,plain,
k7_conlat_2(sK0_skl) = g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f278,f258]) ).
fof(f303,plain,
( v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f119,f79]) ).
fof(f304,plain,
( v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f303,f73]) ).
fof(f315,plain,
( l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f120,f79]) ).
fof(f316,plain,
( l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f315,f73]) ).
fof(f317,plain,
( v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f304,f75]) ).
fof(f318,plain,
( v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f317,f78]) ).
fof(f319,plain,
v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f318,f77]) ).
fof(f338,plain,
( l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f316,f75]) ).
fof(f339,plain,
( l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f338,f78]) ).
fof(f340,plain,
l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f339,f77]) ).
fof(f341,plain,
( ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))) ),
inference(resolution,[status(thm)],[f275,f110]) ).
fof(f342,plain,
( ~ l2_conlat_1(sK0_skl)
| k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f73]) ).
fof(f352,plain,
! [X0,X1] :
( u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u4_conlat_1(X0,X1)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f248,f114]) ).
fof(f353,plain,
! [X0,X1] :
( u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u5_conlat_1(X0,X1)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f247,f114]) ).
fof(f356,plain,
( l3_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f115,f79]) ).
fof(f357,plain,
( l3_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f356,f73]) ).
fof(f373,plain,
l3_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f357,f75]) ).
fof(f444,plain,
m2_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl))),
inference(resolution,[status(thm)],[f126,f262]) ).
fof(f448,plain,
m2_relset_1(u3_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl)),
inference(resolution,[status(thm)],[f126,f75]) ).
fof(f475,plain,
m1_subset_1(u3_conlat_1(sK0_skl),k1_zfmisc_1(k2_zfmisc_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl)))),
inference(resolution,[status(thm)],[f448,f124]) ).
fof(f785,plain,
! [X0,X1,X2] :
( u1_conlat_1(k7_conlat_2(sK0_skl)) = X0
| k7_conlat_2(sK0_skl) != g2_conlat_1(X0,X1,X2)
| ~ m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f279,f153]) ).
fof(f792,plain,
! [X0,X1,X2] :
( u2_conlat_1(k7_conlat_2(sK0_skl)) = X1
| k7_conlat_2(sK0_skl) != g2_conlat_1(X0,X1,X2)
| ~ m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f279,f154]) ).
fof(f825,plain,
m1_relset_1(u3_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl)),
inference(resolution,[status(thm)],[f221,f448]) ).
fof(f834,plain,
! [X0,X1,X2] :
( X0 = k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))
| g2_conlat_1(X1,X2,X0) != k7_conlat_2(sK0_skl)
| ~ m1_relset_1(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f274,f155]) ).
fof(f1021,plain,
m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl))),
inference(resolution,[status(thm)],[f444,f221]) ).
fof(f1144,plain,
v1_relat_1(u3_conlat_1(sK0_skl)),
inference(resolution,[status(thm)],[f475,f89]) ).
fof(f1146,plain,
k4_relat_1(k4_relat_1(u3_conlat_1(sK0_skl))) = u3_conlat_1(sK0_skl),
inference(resolution,[status(thm)],[f1144,f161]) ).
fof(f1389,plain,
k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)) = k4_relat_1(u3_conlat_1(sK0_skl)),
inference(resolution,[status(thm)],[f216,f825]) ).
fof(f1454,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ l2_conlat_1(k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(resolution,[status(thm)],[f218,f373]) ).
fof(f1456,plain,
( k9_conlat_2(sK0_skl,sK1_skl) = k8_conlat_2(sK0_skl,sK1_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f218,f79]) ).
fof(f1482,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1454,f262]) ).
fof(f1484,plain,
( k9_conlat_2(sK0_skl,sK1_skl) = k8_conlat_2(sK0_skl,sK1_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1456,f73]) ).
fof(f1527,plain,
( k9_conlat_2(sK0_skl,sK1_skl) = k8_conlat_2(sK0_skl,sK1_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1484,f75]) ).
fof(f1528,plain,
( k9_conlat_2(sK0_skl,sK1_skl) = k8_conlat_2(sK0_skl,sK1_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f1527,f78]) ).
fof(f1529,plain,
k9_conlat_2(sK0_skl,sK1_skl) = k8_conlat_2(sK0_skl,sK1_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1528,f77]) ).
fof(f1574,plain,
! [X0,X1] :
( u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u4_conlat_1(X0,X1)
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f352,f115]) ).
fof(f1602,plain,
( u5_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = u4_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1574,f79]) ).
fof(f1628,plain,
( u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u4_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f1529,f1602]) ).
fof(f1629,plain,
( u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u4_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1628,f73]) ).
fof(f1630,plain,
! [X0,X1] :
( u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u5_conlat_1(X0,X1)
| ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f115]) ).
fof(f1658,plain,
( u4_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = u5_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1630,f79]) ).
fof(f1684,plain,
( u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u5_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f1529,f1658]) ).
fof(f1685,plain,
( u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u5_conlat_1(sK0_skl,sK1_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1684,f73]) ).
fof(f1697,plain,
u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u4_conlat_1(sK0_skl,sK1_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1629,f75]) ).
fof(f1709,plain,
u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = u5_conlat_1(sK0_skl,sK1_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1685,f75]) ).
fof(f1710,plain,
! [X0] :
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ l2_conlat_1(k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1709,f98]) ).
fof(f1711,plain,
! [X0] :
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| ~ l2_conlat_1(k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1697,f1710]) ).
fof(f1712,plain,
! [X0] :
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1711,f262]) ).
fof(f3684,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k8_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1529,f1482]) ).
fof(f3685,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1529,f3684]) ).
fof(f3686,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1529,f3685]) ).
fof(f3687,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ v9_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v7_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1529,f3686]) ).
fof(f3688,plain,
( k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| v7_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3687,f319]) ).
fof(f3689,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(resolution,[status(thm)],[f3688,f118]) ).
fof(f3690,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3689,f110]) ).
fof(f4200,plain,
! [X0] :
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1712,f340]) ).
fof(f4953,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))),
inference(forward_subsumption_resolution,[status(thm)],[f342,f75]) ).
fof(f5920,plain,
! [X0,X1,X2] :
( X0 = k4_relat_1(u3_conlat_1(sK0_skl))
| g2_conlat_1(X1,X2,X0) != k7_conlat_2(sK0_skl)
| ~ m1_relset_1(X0,X1,X2) ),
inference(backward_demodulation,[status(thm)],[f1389,f834]) ).
fof(f5924,plain,
k7_conlat_2(sK0_skl) = g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k4_relat_1(u3_conlat_1(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f1389,f274]) ).
fof(f5954,plain,
( u3_conlat_1(k7_conlat_2(sK0_skl)) = k4_relat_1(u3_conlat_1(sK0_skl))
| ~ m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl))) ),
inference(resolution,[status(thm)],[f5920,f279]) ).
fof(f5963,plain,
u3_conlat_1(k7_conlat_2(sK0_skl)) = k4_relat_1(u3_conlat_1(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f5954,f1021]) ).
fof(f6004,plain,
k7_conlat_2(sK0_skl) = g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f5963,f5924]) ).
fof(f6006,plain,
k4_relat_1(u3_conlat_1(k7_conlat_2(sK0_skl))) = u3_conlat_1(sK0_skl),
inference(backward_demodulation,[status(thm)],[f5963,f1146]) ).
fof(f7483,plain,
! [X0,X1,X2] :
( u1_conlat_1(k7_conlat_2(sK0_skl)) = X0
| k7_conlat_2(sK0_skl) != g2_conlat_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f785,f1021]) ).
fof(f7484,plain,
u1_conlat_1(k7_conlat_2(sK0_skl)) = u2_conlat_1(sK0_skl),
inference(resolution,[status(thm)],[f7483,f6004]) ).
fof(f7499,plain,
m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(sK0_skl),u2_conlat_1(k7_conlat_2(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f7484,f1021]) ).
fof(f7504,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u2_conlat_1(sK0_skl),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))),
inference(backward_demodulation,[status(thm)],[f7484,f4953]) ).
fof(f7519,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(sK0_skl),k6_relset_1(u2_conlat_1(sK0_skl),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f7484,f7504]) ).
fof(f7729,plain,
! [X0,X1,X2] :
( u2_conlat_1(k7_conlat_2(sK0_skl)) = X1
| k7_conlat_2(sK0_skl) != g2_conlat_1(X0,X1,X2)
| ~ m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(sK0_skl),u2_conlat_1(k7_conlat_2(sK0_skl))) ),
inference(forward_demodulation,[status(thm)],[f7484,f792]) ).
fof(f7730,plain,
! [X0,X1,X2] :
( u2_conlat_1(k7_conlat_2(sK0_skl)) = X1
| k7_conlat_2(sK0_skl) != g2_conlat_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f7729,f7499]) ).
fof(f7732,plain,
u2_conlat_1(k7_conlat_2(sK0_skl)) = u1_conlat_1(sK0_skl),
inference(resolution,[status(thm)],[f7730,f6004]) ).
fof(f7742,plain,
m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f7732,f7499]) ).
fof(f7827,plain,
k6_relset_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl))) = k4_relat_1(u3_conlat_1(k7_conlat_2(sK0_skl))),
inference(resolution,[status(thm)],[f7742,f216]) ).
fof(f7833,plain,
k6_relset_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl))) = u3_conlat_1(sK0_skl),
inference(forward_demodulation,[status(thm)],[f6006,f7827]) ).
fof(f18708,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3690,f73]) ).
fof(f29310,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),k6_relset_1(u2_conlat_1(sK0_skl),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f7732,f7519]) ).
fof(f29311,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),k6_relset_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f7732,f29310]) ).
fof(f29312,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f7833,f29311]) ).
fof(f29379,plain,
! [X0] :
( u5_conlat_1(sK0_skl,X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f29388,f4200]) ).
fof(f29388,plain,
k7_conlat_2(k7_conlat_2(sK0_skl)) = sK0_skl,
inference(forward_demodulation,[status(thm)],[f252,f29312]) ).
fof(f29500,plain,
! [X0] :
( u5_conlat_1(sK0_skl,X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,k7_conlat_2(k7_conlat_2(sK0_skl)))
| ~ v6_conlat_1(X0,sK0_skl)
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f29388,f29379]) ).
fof(f29501,plain,
! [X0] :
( u5_conlat_1(sK0_skl,X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,sK0_skl)
| ~ v6_conlat_1(X0,sK0_skl)
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f29388,f29500]) ).
fof(f29502,plain,
! [X0] :
( u5_conlat_1(sK0_skl,X0) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(sK0_skl,X0) != u4_conlat_1(sK0_skl,sK1_skl)
| X0 = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ l3_conlat_1(X0,sK0_skl)
| ~ v6_conlat_1(X0,sK0_skl)
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f29388,f29501]) ).
fof(f29678,plain,
( u5_conlat_1(sK0_skl,sK1_skl) != u5_conlat_1(sK0_skl,sK1_skl)
| u4_conlat_1(sK0_skl,sK1_skl) != u4_conlat_1(sK0_skl,sK1_skl)
| sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ v6_conlat_1(sK1_skl,sK0_skl)
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(resolution,[status(thm)],[f29502,f79]) ).
fof(f29804,plain,
( sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| ~ v6_conlat_1(sK1_skl,sK0_skl)
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(trivial_equality_resolution,[status(thm)],[f29678]) ).
fof(f29805,plain,
( sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))
| v3_conlat_1(k7_conlat_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f29804,f76]) ).
fof(f29845,plain,
( ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f29805,f110]) ).
fof(f29846,plain,
( ~ l2_conlat_1(sK0_skl)
| sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f29845,f73]) ).
fof(f29850,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)) = sK1_skl ),
inference(backward_demodulation,[status(thm)],[f29852,f18708]) ).
fof(f29852,plain,
sK1_skl = k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f29846,f75]) ).
fof(f29853,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f29850,f80]) ).
fof(f29887,plain,
( ~ l3_conlat_1(sK1_skl,sK0_skl)
| ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f29853,f75]) ).
fof(f29888,plain,
( ~ v9_conlat_1(sK1_skl,sK0_skl)
| v7_conlat_1(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f29887,f79]) ).
fof(f29889,plain,
~ v9_conlat_1(sK1_skl,sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f29888,f77]) ).
fof(f29890,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f29889,f78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.47 % Computer : n020.cluster.edu
% 0.16/0.47 % Model : x86_64 x86_64
% 0.16/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.47 % Memory : 8046.5625MB
% 0.16/0.47 % OS : Linux 6.8.0-71-generic
% 0.16/0.47 % CPULimit : 300
% 0.16/0.47 % WCLimit : 300
% 0.16/0.47 % DateTime : Sun Sep 20 23:44:47 UTC 2026
% 0.16/0.48 % CPUTime :
% 0.16/0.50 % Drodi V4.1.1
% 57.50/7.91 % Refutation found
% 57.50/7.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.50/7.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 32.84/9.12 % Elapsed time: 8.423243 seconds
% 32.84/9.12 % CPU time: 56.306578 seconds
% 32.84/9.12 % Total memory used: 398.817 MB
% 32.84/9.12 % Net memory used: 385.337 MB
%------------------------------------------------------------------------------