%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : LAT378+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 07:48:33 AM UTC 2026
% Result : Theorem 27.29s 4.38s
% Output : CNFRefutation 27.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 13
% Syntax : Number of formulae : 166 ( 26 unt; 0 def)
% Number of atoms : 991 ( 18 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 1480 ( 655 ~; 737 |; 54 &)
% ( 2 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-5 aty)
% Number of variables : 184 ( 11 sgn 51 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [X0,X1,X2] :
( 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('k2$uzfmisc$u1'(X0,X1)))
=> 'v1$urelat$u1'(X2) ) ).
fof(d15_waybel34,axiom,
! [X0] :
( ( 'l1$uorders$u2'(X0)
& ~ 'v3$ustruct$u0'(X0) )
=> ! [X1] :
( ( 'l1$uorders$u2'(X1)
& ~ 'v3$ustruct$u0'(X1) )
=> ! [X2] :
( ( 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X2) )
=> ( 'v4$uwaybel34'(X2,X0,X1)
<=> ! [X3] :
( ( 'm1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))
& 'v1$ufinset$u1'(X3) )
=> 'r4$uwaybel$u0'(X0,X1,X2,X3) ) ) ) ) ) ).
fof(dt_k4_pre_topc,axiom,
! [X0,X1,X2,X3] :
( ( 'm1$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X2)
& 'l1$ustruct$u0'(X1)
& 'l1$ustruct$u0'(X0) )
=> 'm1$usubset$u1'('k4$upre$utopc'(X0,X1,X2,X3),'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) ) ).
fof(dt_k7_funct_2,axiom,
! [X0,X1,X2,X3,X4] :
( ( 'm1$urelset$u1'(X4,X1,X2)
& 'v1$ufunct$u2'(X4,X1,X2)
& 'v1$ufunct$u1'(X4)
& 'm1$urelset$u1'(X3,X0,X1)
& 'v1$ufunct$u2'(X3,X0,X1)
& 'v1$ufunct$u1'(X3)
& ~ 'v1$uxboole$u0'(X1) )
=> ( 'm2$urelset$u1'('k7$ufunct$u2'(X0,X1,X2,X3,X4),X0,X2)
& 'v1$ufunct$u2'('k7$ufunct$u2'(X0,X1,X2,X3,X4),X0,X2)
& 'v1$ufunct$u1'('k7$ufunct$u2'(X0,X1,X2,X3,X4)) ) ) ).
fof(dt_l1_orders_2,axiom,
! [X0] :
( 'l1$uorders$u2'(X0)
=> 'l1$ustruct$u0'(X0) ) ).
fof(dt_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'm2$urelset$u1'(X2,X0,X1)
=> 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('k2$uzfmisc$u1'(X0,X1))) ) ).
fof(fc13_finset_1,axiom,
! [X0,X1] :
( ( 'v1$ufinset$u1'(X1)
& 'v1$ufunct$u1'(X0)
& 'v1$urelat$u1'(X0) )
=> 'v1$ufinset$u1'('k9$urelat$u1'(X0,X1)) ) ).
fof(fc1_struct_0,axiom,
! [X0] :
( ( 'l1$ustruct$u0'(X0)
& ~ 'v3$ustruct$u0'(X0) )
=> ~ 'v1$uxboole$u0'('u1$ustruct$u0'(X0)) ) ).
fof(redefinition_k4_pre_topc,axiom,
! [X0,X1,X2,X3] :
( ( 'm1$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X2)
& 'l1$ustruct$u0'(X1)
& 'l1$ustruct$u0'(X0) )
=> 'k4$upre$utopc'(X0,X1,X2,X3) = 'k9$urelat$u1'(X2,X3) ) ).
fof(redefinition_k7_funct_2,axiom,
! [X0,X1,X2,X3,X4] :
( ( 'm1$urelset$u1'(X4,X1,X2)
& 'v1$ufunct$u2'(X4,X1,X2)
& 'v1$ufunct$u1'(X4)
& 'm1$urelset$u1'(X3,X0,X1)
& 'v1$ufunct$u2'(X3,X0,X1)
& 'v1$ufunct$u1'(X3)
& ~ 'v1$uxboole$u0'(X1) )
=> 'k7$ufunct$u2'(X0,X1,X2,X3,X4) = 'k5$urelat$u1'(X3,X4) ) ).
fof(redefinition_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'm2$urelset$u1'(X2,X0,X1)
<=> 'm1$urelset$u1'(X2,X0,X1) ) ).
fof(t62_waybel34,axiom,
! [X0] :
( ( 'l1$uorders$u2'(X0)
& ~ 'v3$ustruct$u0'(X0) )
=> ! [X1] :
( ( 'l1$uorders$u2'(X1)
& ~ 'v3$ustruct$u0'(X1) )
=> ! [X2] :
( ( 'l1$uorders$u2'(X2)
& ~ 'v3$ustruct$u0'(X2) )
=> ! [X3] :
( 'm1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))
=> ! [X4] :
( ( 'm2$urelset$u1'(X4,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X4,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X4) )
=> ! [X5] :
( ( 'm2$urelset$u1'(X5,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u2'(X5,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u1'(X5) )
=> ( ( 'r4$uwaybel$u0'(X1,X2,X5,'k4$upre$utopc'(X0,X1,X4,X3))
& 'r4$uwaybel$u0'(X0,X1,X4,X3) )
=> 'r4$uwaybel$u0'(X0,X2,'k7$ufunct$u2'('u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2),X4,X5),X3) ) ) ) ) ) ) ) ).
fof(t63_waybel34,conjecture,
! [X0] :
( ( 'l1$uorders$u2'(X0)
& ~ 'v3$ustruct$u0'(X0) )
=> ! [X1] :
( ( 'l1$uorders$u2'(X1)
& ~ 'v3$ustruct$u0'(X1) )
=> ! [X2] :
( ( 'l1$uorders$u2'(X2)
& ~ 'v3$ustruct$u0'(X2) )
=> ! [X3] :
( ( 'm2$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X3) )
=> ! [X4] :
( ( 'm2$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u1'(X4) )
=> ( ( 'v4$uwaybel34'(X4,X1,X2)
& 'v4$uwaybel34'(X3,X0,X1) )
=> 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2),X3,X4),X0,X2) ) ) ) ) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( 'l1$uorders$u2'(X0)
& ~ 'v3$ustruct$u0'(X0) )
=> ! [X1] :
( ( 'l1$uorders$u2'(X1)
& ~ 'v3$ustruct$u0'(X1) )
=> ! [X2] :
( ( 'l1$uorders$u2'(X2)
& ~ 'v3$ustruct$u0'(X2) )
=> ! [X3] :
( ( 'm2$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))
& 'v1$ufunct$u1'(X3) )
=> ! [X4] :
( ( 'm2$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
& 'v1$ufunct$u1'(X4) )
=> ( ( 'v4$uwaybel34'(X4,X1,X2)
& 'v4$uwaybel34'(X3,X0,X1) )
=> 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2),X3,X4),X0,X2) ) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t63_waybel34]) ).
cnf(c36,plain,
( 'v1$urelat$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('k2$uzfmisc$u1'(X1,X2))) ),
inference(clausification,[status(esa)],[cc1_relset_1]) ).
cnf(c50,plain,
( ~ 'm2$urelset$u1'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
| ~ 'v1$ufinset$u1'(X0)
| ~ 'v1$ufunct$u1'(X3)
| ~ 'l1$uorders$u2'(X1)
| ~ 'v4$uwaybel34'(X3,X1,X2)
| 'r4$uwaybel$u0'(X1,X2,X3,X0)
| 'v3$ustruct$u0'(X1)
| ~ 'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(X2)
| 'v3$ustruct$u0'(X2)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) ),
inference(clausification,[status(esa)],[d15_waybel34]) ).
cnf(c51,plain,
( ~ 'v1$ufunct$u1'(X2)
| 'v4$uwaybel34'(X2,X1,X0)
| ~ 'l1$uorders$u2'(X1)
| ~ 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0))
| 'v3$ustruct$u0'(X1)
| ~ 'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0))
| ~ 'l1$uorders$u2'(X0)
| 'v1$ufinset$u1'(sK42(X1,X0,X2))
| 'v3$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[d15_waybel34]) ).
cnf(c52,plain,
( ~ 'v1$ufunct$u1'(X1)
| 'v4$uwaybel34'(X1,X2,X0)
| ~ 'l1$uorders$u2'(X2)
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| 'm1$usubset$u1'(sK42(X2,X0,X1),'k1$uzfmisc$u1'('u1$ustruct$u0'(X2)))
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| ~ 'l1$uorders$u2'(X0)
| 'v3$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[d15_waybel34]) ).
cnf(c53,plain,
( ~ 'v1$ufunct$u1'(X1)
| 'v4$uwaybel34'(X1,X2,X0)
| ~ 'l1$uorders$u2'(X2)
| ~ 'r4$uwaybel$u0'(X2,X0,X1,sK42(X2,X0,X1))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| ~ 'l1$uorders$u2'(X0)
| 'v3$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[d15_waybel34]) ).
cnf(c54,plain,
( ~ 'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))
| ~ 'l1$ustruct$u0'(X2)
| ~ 'l1$ustruct$u0'(X1)
| ~ 'v1$ufunct$u1'(X0)
| 'm1$usubset$u1'('k4$upre$utopc'(X1,X2,X0,X3),'k1$uzfmisc$u1'('u1$ustruct$u0'(X2)))
| ~ 'm1$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) ),
inference(clausification,[status(esa)],[dt_k4_pre_topc]) ).
cnf(c56,plain,
( ~ 'v1$ufunct$u2'(X4,X3,X0)
| ~ 'm1$urelset$u1'(X4,X3,X0)
| ~ 'm1$urelset$u1'(X1,X0,X2)
| ~ 'v1$ufunct$u1'(X4)
| ~ 'v1$ufunct$u1'(X1)
| 'v1$ufunct$u1'('k7$ufunct$u2'(X3,X0,X2,X4,X1))
| ~ 'v1$ufunct$u2'(X1,X0,X2)
| 'v1$uxboole$u0'(X0) ),
inference(clausification,[status(esa)],[dt_k7_funct_2]) ).
cnf(c57,plain,
( ~ 'v1$ufunct$u2'(X3,X4,X0)
| ~ 'm1$urelset$u1'(X3,X4,X0)
| 'v1$ufunct$u2'('k7$ufunct$u2'(X4,X0,X2,X3,X1),X4,X2)
| ~ 'm1$urelset$u1'(X1,X0,X2)
| ~ 'v1$ufunct$u1'(X3)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'v1$ufunct$u2'(X1,X0,X2)
| 'v1$uxboole$u0'(X0) ),
inference(clausification,[status(esa)],[dt_k7_funct_2]) ).
cnf(c58,plain,
( ~ 'v1$ufunct$u2'(X4,X3,X0)
| ~ 'm1$urelset$u1'(X4,X3,X0)
| ~ 'm1$urelset$u1'(X1,X0,X2)
| ~ 'v1$ufunct$u1'(X4)
| 'm2$urelset$u1'('k7$ufunct$u2'(X3,X0,X2,X4,X1),X3,X2)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'v1$ufunct$u2'(X1,X0,X2)
| 'v1$uxboole$u0'(X0) ),
inference(clausification,[status(esa)],[dt_k7_funct_2]) ).
cnf(c59,plain,
( 'l1$ustruct$u0'(X0)
| ~ 'l1$uorders$u2'(X0) ),
inference(clausification,[status(esa)],[dt_l1_orders_2]) ).
cnf(c60,plain,
( 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('k2$uzfmisc$u1'(X1,X2)))
| ~ 'm2$urelset$u1'(X0,X1,X2) ),
inference(clausification,[status(esa)],[dt_m2_relset_1]) ).
cnf(c66,plain,
( 'v1$ufinset$u1'('k9$urelat$u1'(X0,X1))
| ~ 'v1$ufinset$u1'(X1)
| ~ 'v1$ufunct$u1'(X0)
| ~ 'v1$urelat$u1'(X0) ),
inference(clausification,[status(esa)],[fc13_finset_1]) ).
cnf(c70,plain,
( ~ 'v1$uxboole$u0'('u1$ustruct$u0'(X0))
| ~ 'l1$ustruct$u0'(X0)
| 'v3$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[fc1_struct_0]) ).
cnf(c104,plain,
( ~ 'l1$ustruct$u0'(X2)
| ~ 'm1$urelset$u1'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| 'k4$upre$utopc'(X2,X0,X1,X3) = 'k9$urelat$u1'(X1,X3)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X2),'u1$ustruct$u0'(X0))
| ~ 'l1$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[redefinition_k4_pre_topc]) ).
cnf(c105,plain,
( ~ 'm1$urelset$u1'(X3,X4,X1)
| ~ 'v1$ufunct$u1'(X0)
| 'k7$ufunct$u2'(X4,X1,X2,X3,X0) = 'k5$urelat$u1'(X3,X0)
| 'v1$uxboole$u0'(X1)
| ~ 'm1$urelset$u1'(X0,X1,X2)
| ~ 'v1$ufunct$u1'(X3)
| ~ 'v1$ufunct$u2'(X3,X4,X1)
| ~ 'v1$ufunct$u2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_k7_funct_2]) ).
cnf(c106,plain,
( 'm1$urelset$u1'(X0,X1,X2)
| ~ 'm2$urelset$u1'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c115,plain,
( 'v3$ustruct$u0'(X2)
| ~ 'r4$uwaybel$u0'(X0,X2,X4,'k4$upre$utopc'(X1,X0,X3,X5))
| ~ 'v1$ufunct$u2'(X4,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2))
| ~ 'v1$ufunct$u1'(X4)
| ~ 'l1$uorders$u2'(X1)
| ~ 'm1$usubset$u1'(X5,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1)))
| ~ 'l1$uorders$u2'(X2)
| ~ 'l1$uorders$u2'(X0)
| ~ 'm2$urelset$u1'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0))
| ~ 'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0))
| ~ 'r4$uwaybel$u0'(X1,X0,X3,X5)
| ~ 'v1$ufunct$u1'(X3)
| ~ 'm2$urelset$u1'(X4,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2))
| 'v3$ustruct$u0'(X1)
| 'r4$uwaybel$u0'(X1,X2,'k7$ufunct$u2'('u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2),X3,X4),X5)
| 'v3$ustruct$u0'(X0) ),
inference(clausification,[status(esa)],[t62_waybel34]) ).
cnf(c119,plain,
~ 'v3$ustruct$u0'(sK128),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c120,plain,
'l1$uorders$u2'(sK128),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c121,plain,
~ 'v3$ustruct$u0'(sK129),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c122,plain,
'l1$uorders$u2'(sK129),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c123,plain,
~ 'v3$ustruct$u0'(sK130),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c124,plain,
'l1$uorders$u2'(sK130),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c125,plain,
'v1$ufunct$u1'(sK131),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c126,plain,
'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c127,plain,
'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c128,plain,
'v1$ufunct$u1'(sK132),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c129,plain,
'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c130,plain,
'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c131,plain,
'v4$uwaybel34'(sK131,sK128,sK129),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c132,plain,
'v4$uwaybel34'(sK132,sK129,sK130),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c133,plain,
~ 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),sK128,sK130),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129)),
inference(resolution,[status(thm)],[c106,c127]) ).
cnf(d1,plain,
'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130)),
inference(resolution,[status(thm)],[c106,c130]) ).
cnf(d2,plain,
( ~ 'm1$urelset$u1'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'(X1)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'(X0,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),X1,sK132) = 'k5$urelat$u1'(X1,sK132) ),
inference(resolution,[status(thm)],[d1,c105]) ).
cnf(d3,plain,
( ~ 'm1$urelset$u1'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(X1)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'(X0,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),X1,sK132) = 'k5$urelat$u1'(X1,sK132) ),
inference(resolution,[status(thm)],[c128,d2]) ).
cnf(d4,plain,
( ~ 'm1$urelset$u1'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,X0,'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(X1)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'(X0,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),X1,sK132) = 'k5$urelat$u1'(X1,sK132) ),
inference(resolution,[status(thm)],[c129,d3]) ).
cnf(d5,plain,
( ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK131)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132) ),
inference(resolution,[status(thm)],[d4,d0]) ).
cnf(d6,plain,
( ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132) ),
inference(resolution,[status(thm)],[c125,d5]) ).
cnf(d7,plain,
( 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132) ),
inference(resolution,[status(thm)],[c126,d6]) ).
cnf(d8,plain,
( ~ 'l1$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(sK129)
| 'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132) ),
inference(resolution,[status(thm)],[d7,c70]) ).
cnf(d9,plain,
( ~ 'l1$ustruct$u0'(sK129)
| 'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132) ),
inference(resolution,[status(thm)],[c121,d8]) ).
cnf(d10,plain,
'l1$ustruct$u0'(sK129),
inference(resolution,[status(thm)],[c59,c122]) ).
cnf(d11,plain,
'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132) = 'k5$urelat$u1'(sK131,sK132),
inference(resolution,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'(sK131)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132)) ),
inference(superposition,[status(thm)],[d11,c56]) ).
cnf(d13,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK132)
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c125,d12]) ).
cnf(d14,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c128,d13]) ).
cnf(d15,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c126,d14]) ).
cnf(d16,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c129,d15]) ).
cnf(d17,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d0,d16]) ).
cnf(d18,plain,
( 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d1,d17]) ).
cnf(d19,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'(sK131)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130)) ),
inference(superposition,[status(thm)],[d11,c57]) ).
cnf(d20,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'(sK132)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c125,d19]) ).
cnf(d21,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c128,d20]) ).
cnf(d22,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c126,d21]) ).
cnf(d23,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c129,d22]) ).
cnf(d24,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d0,d23]) ).
cnf(d25,plain,
( 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d1,d24]) ).
cnf(d26,plain,
( 'v3$ustruct$u0'(sK128)
| 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d25,c51]) ).
cnf(d27,plain,
( 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c119,d26]) ).
cnf(d28,plain,
( 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c120,d27]) ).
cnf(d29,plain,
( ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c123,d28]) ).
cnf(d30,plain,
( ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c124,d29]) ).
cnf(d31,plain,
~ 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130),
inference(demodulation,[status(thm)],[c133,d11]) ).
cnf(d32,plain,
( ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'(sK131)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130)) ),
inference(superposition,[status(thm)],[d11,c58]) ).
cnf(d34,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'(sK132)
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c125,d33]) ).
cnf(d35,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c128,d34]) ).
cnf(d36,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c126,d35]) ).
cnf(d37,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[c129,d36]) ).
cnf(d38,plain,
( ~ 'm1$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d0,d37]) ).
cnf(d39,plain,
( 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d1,d38]) ).
cnf(d40,plain,
( ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d39,d32]) ).
cnf(d41,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'v3$ustruct$u0'(sK128)
| 'v3$ustruct$u0'(sK129)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c50,c126]) ).
cnf(d42,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'v3$ustruct$u0'(sK129)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c119,d41]) ).
cnf(d43,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'v3$ustruct$u0'(sK129)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c120,d42]) ).
cnf(d44,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c121,d43]) ).
cnf(d45,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c122,d44]) ).
cnf(d46,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v4$uwaybel34'(sK131,sK128,sK129)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c125,d45]) ).
cnf(d47,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c131,d46]) ).
cnf(d48,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c127,d47]) ).
cnf(d49,plain,
( 'v3$ustruct$u0'(sK128)
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'(X1,sK128,X0)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'(X1)
| 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,X1))
| ~ 'v1$ufinset$u1'(sK42(sK128,X0,X1)) ),
inference(resolution,[status(thm)],[d48,c52]) ).
cnf(d50,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,X1))
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'(X1,sK128,X0)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'v1$ufinset$u1'(sK42(sK128,X0,X1)) ),
inference(resolution,[status(thm)],[c119,d49]) ).
cnf(d51,plain,
( 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,X1))
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'(X1,sK128,X0)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'v1$ufinset$u1'(sK42(sK128,X0,X1)) ),
inference(resolution,[status(thm)],[c120,d50]) ).
cnf(d52,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| 'v3$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c50,c129]) ).
cnf(d53,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'l1$uorders$u2'(sK129)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c121,d52]) ).
cnf(d54,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| 'v3$ustruct$u0'(sK130)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c122,d53]) ).
cnf(d55,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c123,d54]) ).
cnf(d56,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c124,d55]) ).
cnf(d57,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v4$uwaybel34'(sK132,sK129,sK130)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c128,d56]) ).
cnf(d58,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c132,d57]) ).
cnf(d59,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,X0)
| ~ 'v1$ufinset$u1'(X0)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c130,d58]) ).
cnf(d60,plain,
( ~ 'l1$ustruct$u0'(sK128)
| ~ 'l1$ustruct$u0'(sK129)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK131)
| 'k4$upre$utopc'(sK128,sK129,sK131,X0) = 'k9$urelat$u1'(sK131,X0) ),
inference(resolution,[status(thm)],[d0,c104]) ).
cnf(d61,plain,
( ~ 'l1$ustruct$u0'(sK129)
| ~ 'l1$ustruct$u0'(sK128)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'k4$upre$utopc'(sK128,sK129,sK131,X0) = 'k9$urelat$u1'(sK131,X0) ),
inference(resolution,[status(thm)],[c125,d60]) ).
cnf(d62,plain,
( ~ 'l1$ustruct$u0'(sK129)
| ~ 'l1$ustruct$u0'(sK128)
| 'k4$upre$utopc'(sK128,sK129,sK131,X0) = 'k9$urelat$u1'(sK131,X0) ),
inference(resolution,[status(thm)],[c126,d61]) ).
cnf(d63,plain,
( ~ 'l1$ustruct$u0'(sK128)
| 'k4$upre$utopc'(sK128,sK129,sK131,X0) = 'k9$urelat$u1'(sK131,X0) ),
inference(resolution,[status(thm)],[d10,d62]) ).
cnf(d64,plain,
'l1$ustruct$u0'(sK128),
inference(resolution,[status(thm)],[c59,c120]) ).
cnf(d65,plain,
'k4$upre$utopc'(sK128,sK129,sK131,X0) = 'k9$urelat$u1'(sK131,X0),
inference(resolution,[status(thm)],[d64,d63]) ).
cnf(d66,plain,
( ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'l1$ustruct$u0'(sK129)
| ~ 'l1$ustruct$u0'(sK128)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'(sK131)
| 'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(superposition,[status(thm)],[d65,c54]) ).
cnf(d67,plain,
( ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'l1$ustruct$u0'(sK129)
| ~ 'l1$ustruct$u0'(sK128)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c125,d66]) ).
cnf(d68,plain,
( ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'l1$ustruct$u0'(sK129)
| ~ 'l1$ustruct$u0'(sK128)
| 'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[c126,d67]) ).
cnf(d69,plain,
( ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'l1$ustruct$u0'(sK128)
| 'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[d10,d68]) ).
cnf(d70,plain,
( ~ 'm1$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| 'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))) ),
inference(resolution,[status(thm)],[d64,d69]) ).
cnf(d71,plain,
'm1$usubset$u1'('k9$urelat$u1'(sK131,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK129))),
inference(resolution,[status(thm)],[d0,d70]) ).
cnf(d72,plain,
( 'r4$uwaybel$u0'(sK129,sK130,sK132,'k9$urelat$u1'(sK131,X0))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,X0)) ),
inference(resolution,[status(thm)],[d71,d59]) ).
cnf(d73,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X1,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X1),sK131,X2),X0)
| 'v3$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(X1)
| 'v3$ustruct$u0'(sK128)
| ~ 'v1$ufunct$u2'(X2,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X1))
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X2,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X1))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(X1)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'v1$ufunct$u1'(X2)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128)))
| ~ 'r4$uwaybel$u0'(sK129,X1,X2,'k9$urelat$u1'(sK131,X0)) ),
inference(superposition,[status(thm)],[d65,c115]) ).
cnf(d74,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c119,d73]) ).
cnf(d75,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c120,d74]) ).
cnf(d76,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(sK129)
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c121,d75]) ).
cnf(d77,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c122,d76]) ).
cnf(d78,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c125,d77]) ).
cnf(d79,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(sK131,'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c126,d78]) ).
cnf(d80,plain,
( ~ 'r4$uwaybel$u0'(sK129,X2,X1,'k9$urelat$u1'(sK131,X0))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,X0)
| 'r4$uwaybel$u0'(sK128,X2,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2),sK131,X1),X0)
| 'v3$ustruct$u0'(X2)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X2))
| ~ 'l1$uorders$u2'(X2)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c127,d79]) ).
cnf(d81,plain,
( 'v3$ustruct$u0'(sK128)
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),sK128,X0)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))
| ~ 'r4$uwaybel$u0'(sK129,X0,X1,'k9$urelat$u1'(sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)))
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[d80,c53]) ).
cnf(d82,plain,
( ~ 'r4$uwaybel$u0'(sK129,X0,X1,'k9$urelat$u1'(sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)))
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),sK128,X0)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c119,d81]) ).
cnf(d83,plain,
( ~ 'r4$uwaybel$u0'(sK129,X0,X1,'k9$urelat$u1'(sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)))
| 'v3$ustruct$u0'(X0)
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(X0))
| ~ 'm2$urelset$u1'(X1,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1),sK128,X0)
| ~ 'l1$uorders$u2'(X0)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1))
| ~ 'v1$ufunct$u1'(X1)
| ~ 'm1$usubset$u1'(sK42(sK128,X0,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(X0),sK131,X1)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c120,d82]) ).
cnf(d84,plain,
( ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132))))
| ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132))
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[d83,d72]) ).
cnf(d85,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d84,d11]) ).
cnf(d86,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d85,d11]) ).
cnf(d87,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d86,d11]) ).
cnf(d88,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d87,d11]) ).
cnf(d89,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d88,d11]) ).
cnf(d90,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k7$ufunct$u2'('u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130),sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d89,d11]) ).
cnf(d91,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(demodulation,[status(thm)],[d90,d11]) ).
cnf(d92,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c123,d91]) ).
cnf(d93,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'(sK132)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c124,d92]) ).
cnf(d94,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c128,d93]) ).
cnf(d95,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'(sK132,'u1$ustruct$u0'(sK129),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c129,d94]) ).
cnf(d96,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c130,d95]) ).
cnf(d97,plain,
( ~ 'r4$uwaybel$u0'(sK128,sK129,sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[d31,d96]) ).
cnf(d98,plain,
( 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[d97,d51]) ).
cnf(d99,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c123,d98]) ).
cnf(d100,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[c124,d99]) ).
cnf(d101,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'm1$usubset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK128))) ),
inference(resolution,[status(thm)],[d31,d100]) ).
cnf(d102,plain,
( 'v3$ustruct$u0'(sK128)
| 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[d101,c52]) ).
cnf(d103,plain,
( 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'l1$uorders$u2'(sK128)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[c119,d102]) ).
cnf(d104,plain,
( 'v3$ustruct$u0'(sK130)
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[c120,d103]) ).
cnf(d105,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'l1$uorders$u2'(sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[c123,d104]) ).
cnf(d106,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| 'v4$uwaybel34'('k5$urelat$u1'(sK131,sK132),sK128,sK130)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[c124,d105]) ).
cnf(d107,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'('k9$urelat$u1'(sK131,sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[d31,d106]) ).
cnf(d108,plain,
( ~ 'v1$urelat$u1'(sK131)
| ~ 'v1$ufunct$u1'(sK131)
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[d107,c66]) ).
cnf(d109,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$urelat$u1'(sK131)
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[c125,d108]) ).
cnf(d110,plain,
( 'v1$urelat$u1'(X0)
| ~ 'm2$urelset$u1'(X0,X1,X2) ),
inference(resolution,[status(thm)],[c60,c36]) ).
cnf(d111,plain,
'v1$urelat$u1'(sK131),
inference(resolution,[status(thm)],[d110,c127]) ).
cnf(d112,plain,
( ~ 'v1$ufunct$u2'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[d111,d109]) ).
cnf(d113,plain,
( 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| ~ 'm2$urelset$u1'('k5$urelat$u1'(sK131,sK132),'u1$ustruct$u0'(sK128),'u1$ustruct$u0'(sK130))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132))) ),
inference(resolution,[status(thm)],[d112,d25]) ).
cnf(d114,plain,
( 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| ~ 'v1$ufinset$u1'(sK42(sK128,sK130,'k5$urelat$u1'(sK131,sK132)))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d113,d39]) ).
cnf(d115,plain,
( ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| ~ 'v1$ufunct$u1'('k5$urelat$u1'(sK131,sK132))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d114,d40]) ).
cnf(d116,plain,
( 'v1$uxboole$u0'('u1$ustruct$u0'(sK129))
| 'v1$uxboole$u0'('u1$ustruct$u0'(sK129)) ),
inference(resolution,[status(thm)],[d115,d18]) ).
cnf(d117,plain,
( ~ 'l1$ustruct$u0'(sK129)
| 'v3$ustruct$u0'(sK129) ),
inference(resolution,[status(thm)],[d116,c70]) ).
cnf(d118,plain,
~ 'l1$ustruct$u0'(sK129),
inference(resolution,[status(thm)],[c121,d117]) ).
cnf(d119,plain,
$false,
inference(resolution,[status(thm)],[d10,d118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT378+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.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 : Fri Sep 25 21:34:32 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.29/4.38 % SZS status Theorem for theBenchmark.p
% 27.29/4.38 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------