LisaST---0.9.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : LisaST---0.9
% Problem  : GRP621+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 : n012.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:24:11 AM UTC 2026

% Result   : Theorem 163.07s 23.76s
% Output   : CNFRefutation 163.07s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : GRP621+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02  % Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30  % Computer : n012.cluster.edu
% 0.04/0.30  % Model    : x86_64 x86_64
% 0.04/0.30  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30  % Memory   : 8046.5625MB
% 0.04/0.30  % OS       : Linux 6.8.0-71-generic
% 0.04/0.30  % CPULimit : 300
% 0.04/0.30  % WCLimit  : 300
% 0.04/0.30  % DateTime : Fri Sep 25 15:02:50 UTC 2026
% 0.04/0.30  % CPUTime  : 
% 0.04/0.30  Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 163.07/23.76  % SZS status Theorem for theBenchmark.p
% 163.07/23.76  % SZS output start CNFRefutation for theBenchmark.p
% 163.07/23.76  fof(d1_autgroup, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v1$ugroup$u1'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0))))) => ! [X1] : (('m1$ufraenkel'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) => (X1 = 'k1$uautgroup'(X0) <=> (! [X2] : (('m2$ufraenkel'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),X1) => ('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) & ('v1$ugroup$u6'(X2,X0,X0) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0))))))) & ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) & ('v1$ugroup$u6'(X2,X0,X0) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0))))) => ('r2$uhidden'(X2,X1) <=> ('v2$ufunct$u1'(X2) & 'v3$ugroup$u6'(X2,X0,X0)))))))))))).
% 163.07/23.76  fof(dt_k1_autgroup, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v1$ugroup$u1'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0))))) => 'm1$ufraenkel'('k1$uautgroup'(X0),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0))))).
% 163.07/23.76  fof(dt_k7_funct_2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((~'v1$uxboole$u0'(X1) & ('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,X0,X1) & ('m1$urelset$u1'(X3,X0,X1) & ('v1$ufunct$u1'(X4) & ('v1$ufunct$u2'(X4,X1,X2) & 'm1$urelset$u1'(X4,X1,X2))))))) => ('v1$ufunct$u1'('k7$ufunct$u2'(X0,X1,X2,X3,X4)) & ('v1$ufunct$u2'('k7$ufunct$u2'(X0,X1,X2,X3,X4),X0,X2) & 'm2$urelset$u1'('k7$ufunct$u2'(X0,X1,X2,X3,X4),X0,X2)))))).
% 163.07/23.76  fof(dt_k8_group_6, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & ('l1$ugroup$u1'(X0) & (~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & ('l1$ugroup$u1'(X1) & (~'v3$ustruct$u0'(X2) & ('v3$ugroup$u1'(X2) & ('v4$ugroup$u1'(X2) & ('l1$ugroup$u1'(X2) & ('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X3,X0,X1) & ('m1$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ufunct$u1'(X4) & ('v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) & ('v1$ugroup$u6'(X4,X1,X2) & 'm1$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))))))))))))))))))))) => ('v1$ufunct$u1'('k8$ugroup$u6'(X0,X1,X2,X3,X4)) & ('v1$ufunct$u2'('k8$ugroup$u6'(X0,X1,X2,X3,X4),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) & ('v1$ugroup$u6'('k8$ugroup$u6'(X0,X1,X2,X3,X4),X0,X2) & 'm2$urelset$u1'('k8$ugroup$u6'(X0,X1,X2,X3,X4),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)))))))).
% 163.07/23.76  fof(dt_l1_group_1, axiom, ! [X0] : (('l1$ugroup$u1'(X0) => 'l1$ustruct$u0'(X0)))).
% 163.07/23.76  fof(dt_m1_fraenkel, axiom, ! [X0] : ! [X1] : ! [X2] : (('m1$ufraenkel'(X2,X0,X1) => (~'v1$uxboole$u0'(X2) & 'v1$ufraenkel'(X2))))).
% 163.07/23.76  fof(dt_m2_fraenkel, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'v1$uxboole$u0'(X1) & 'm1$ufraenkel'(X2,X0,X1)) => ! [X3] : (('m2$ufraenkel'(X3,X0,X1,X2) => ('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,X0,X1) & 'm2$urelset$u1'(X3,X0,X1)))))))).
% 163.07/23.76  fof(fc1_struct_0, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & 'l1$ustruct$u0'(X0)) => ~'v1$uxboole$u0'('u1$ustruct$u0'(X0))))).
% 163.07/23.76  fof(fc1_xboole_0, axiom, 'v1$uxboole$u0'('k1$uxboole$u0')).
% 163.07/23.76  fof(rc1_xboole_0, axiom, ? [X0] : 'v1$uxboole$u0'(X0)).
% 163.07/23.76  fof(redefinition_k7_funct_2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((~'v1$uxboole$u0'(X1) & ('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,X0,X1) & ('m1$urelset$u1'(X3,X0,X1) & ('v1$ufunct$u1'(X4) & ('v1$ufunct$u2'(X4,X1,X2) & 'm1$urelset$u1'(X4,X1,X2))))))) => 'k7$ufunct$u2'(X0,X1,X2,X3,X4) = 'k5$urelat$u1'(X3,X4)))).
% 163.07/23.76  fof(redefinition_k8_group_6, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & ('l1$ugroup$u1'(X0) & (~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & ('l1$ugroup$u1'(X1) & (~'v3$ustruct$u0'(X2) & ('v3$ugroup$u1'(X2) & ('v4$ugroup$u1'(X2) & ('l1$ugroup$u1'(X2) & ('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X3,X0,X1) & ('m1$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ufunct$u1'(X4) & ('v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) & ('v1$ugroup$u6'(X4,X1,X2) & 'm1$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))))))))))))))))))))) => 'k8$ugroup$u6'(X0,X1,X2,X3,X4) = 'k5$urelat$u1'(X3,X4)))).
% 163.07/23.76  fof(redefinition_m2_fraenkel, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'v1$uxboole$u0'(X1) & 'm1$ufraenkel'(X2,X0,X1)) => ! [X3] : (('m2$ufraenkel'(X3,X0,X1,X2) <=> 'm1$usubset$u1'(X3,X2)))))).
% 163.07/23.76  fof(redefinition_m2_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('m2$urelset$u1'(X2,X0,X1) <=> 'm1$urelset$u1'(X2,X0,X1)))).
% 163.07/23.76  fof(t1_subset, axiom, ! [X0] : ! [X1] : (('r2$uhidden'(X0,X1) => 'm1$usubset$u1'(X0,X1)))).
% 163.07/23.76  fof(t2_subset, axiom, ! [X0] : ! [X1] : (('m1$usubset$u1'(X0,X1) => ('v1$uxboole$u0'(X1) | 'r2$uhidden'(X0,X1))))).
% 163.07/23.76  fof(t5_autgroup, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v1$ugroup$u1'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0))))) => ! [X1] : ((('v1$ufunct$u1'(X1) & ('v1$ufunct$u2'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) & ('v1$ugroup$u6'(X1,X0,X0) & 'm2$urelset$u1'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0))))) => ('r2$uhidden'(X1,'k1$uautgroup'(X0)) <=> 'v4$ugroup$u6'(X1,X0,X0))))))).
% 163.07/23.76  fof(t6_boole, axiom, ! [X0] : (('v1$uxboole$u0'(X0) => X0 = 'k1$uxboole$u0'))).
% 163.07/23.76  fof(t74_group_6, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & 'l1$ugroup$u1'(X1)))) => ! [X2] : (((~'v3$ustruct$u0'(X2) & ('v3$ugroup$u1'(X2) & ('v4$ugroup$u1'(X2) & 'l1$ugroup$u1'(X2)))) => ! [X3] : ((('v1$ufunct$u1'(X3) & ('v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X3,X0,X1) & 'm2$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))) => ! [X4] : ((('v1$ufunct$u1'(X4) & ('v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) & ('v1$ugroup$u6'(X4,X1,X2) & 'm2$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2))))) => (('v4$ugroup$u6'(X3,X0,X1) & 'v4$ugroup$u6'(X4,X1,X2)) => 'v4$ugroup$u6'('k8$ugroup$u6'(X0,X1,X2,X3,X4),X0,X2))))))))))))).
% 163.07/23.76  fof(t8_boole, axiom, ! [X0] : ! [X1] : ~(('v1$uxboole$u0'(X0) & (X0 != X1 & 'v1$uxboole$u0'(X1))))).
% 163.07/23.76  fof(t8_autgroup, conjecture, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v1$ugroup$u1'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0))))) => ! [X1] : (('m2$ufraenkel'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0)) => ! [X2] : (('m2$ufraenkel'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0)) => 'm2$ufraenkel'('k7$ufunct$u2'('u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),X2,X1),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0))))))))).
% 163.07/23.76  fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'v3$ustruct$u0'(X0) & ('v1$ugroup$u1'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0))))) => ! [X1] : (('m2$ufraenkel'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0)) => ! [X2] : (('m2$ufraenkel'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0)) => 'm2$ufraenkel'('k7$ufunct$u2'('u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),X2,X1),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0),'k1$uautgroup'(X0)))))))), inference(negate_conjecture, [status(cth)], [t8_autgroup])).
% 163.07/23.76  cnf(c20, plain, 'k1$uautgroup'(X0) != X1 | ~'l1$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X0) | ~'m1$ufraenkel'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) | X2(X0,X1) | 'v3$ustruct$u0'(X0) | ~'v1$ugroup$u1'(X0), inference(clausification, [status(esa)], [d1_autgroup])).
% 163.07/23.76  cnf(c24, plain, ~X0(X1,X2) | ~'m2$ufraenkel'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X1),X2) | 'v1$ugroup$u6'(X3,X1,X1), inference(clausification, [status(esa)], [d1_autgroup])).
% 163.07/23.76  cnf(c41, plain, ~'l1$ugroup$u1'(X0) | 'm1$ufraenkel'('k1$uautgroup'(X0),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) | ~'v1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v4$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X0), inference(clausification, [status(esa)], [dt_k1_autgroup])).
% 163.07/23.76  cnf(c43, plain, ~'v1$ufunct$u1'(X0) | ~'m1$urelset$u1'(X0,X1,X2) | ~'v1$ufunct$u1'(X3) | ~'v1$ufunct$u2'(X3,X4,X1) | ~'m1$urelset$u1'(X3,X4,X1) | 'v1$ufunct$u1'('k7$ufunct$u2'(X4,X1,X2,X3,X0)) | ~'v1$ufunct$u2'(X0,X1,X2) | 'v1$uxboole$u0'(X1), inference(clausification, [status(esa)], [dt_k7_funct_2])).
% 163.07/23.76  cnf(c44, plain, ~'v1$ufunct$u1'(X0) | ~'m1$urelset$u1'(X0,X1,X2) | ~'v1$ufunct$u1'(X3) | ~'v1$ufunct$u2'(X3,X4,X1) | 'm2$urelset$u1'('k7$ufunct$u2'(X4,X1,X2,X3,X0),X4,X2) | ~'m1$urelset$u1'(X3,X4,X1) | ~'v1$ufunct$u2'(X0,X1,X2) | 'v1$uxboole$u0'(X1), inference(clausification, [status(esa)], [dt_k7_funct_2])).
% 163.07/23.76  cnf(c45, plain, ~'v1$ufunct$u1'(X0) | ~'m1$urelset$u1'(X0,X1,X2) | 'v1$ufunct$u2'('k7$ufunct$u2'(X3,X1,X2,X4,X0),X3,X2) | ~'v1$ufunct$u1'(X4) | ~'v1$ufunct$u2'(X4,X3,X1) | ~'m1$urelset$u1'(X4,X3,X1) | ~'v1$ufunct$u2'(X0,X1,X2) | 'v1$uxboole$u0'(X1), inference(clausification, [status(esa)], [dt_k7_funct_2])).
% 163.07/23.76  cnf(c47, plain, 'v1$ugroup$u6'('k8$ugroup$u6'(X0,X1,X2,X3,X4),X0,X2) | ~'v3$ugroup$u1'(X2) | ~'l1$ugroup$u1'(X0) | ~'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'v3$ugroup$u1'(X0) | ~'v1$ufunct$u2'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | ~'v1$ufunct$u1'(X3) | ~'v1$ugroup$u6'(X3,X0,X1) | ~'v4$ugroup$u1'(X2) | ~'m1$urelset$u1'(X3,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'l1$ugroup$u1'(X2) | ~'v3$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X4,X1,X2) | ~'v4$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X0) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(X0) | ~'m1$urelset$u1'(X4,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X4) | 'v3$ustruct$u0'(X2), inference(clausification, [status(esa)], [dt_k8_group_6])).
% 163.07/23.76  cnf(c50, plain, ~'l1$ugroup$u1'(X0) | 'l1$ustruct$u0'(X0), inference(clausification, [status(esa)], [dt_l1_group_1])).
% 163.07/23.76  cnf(c51, plain, ~'m1$ufraenkel'(X0,X1,X2) | ~'v1$uxboole$u0'(X0), inference(clausification, [status(esa)], [dt_m1_fraenkel])).
% 163.07/23.76  cnf(c53, plain, ~'m1$ufraenkel'(X0,X1,X2) | 'v1$uxboole$u0'(X2) | ~'m2$ufraenkel'(X3,X1,X2,X0) | 'v1$ufunct$u1'(X3), inference(clausification, [status(esa)], [dt_m2_fraenkel])).
% 163.07/23.76  cnf(c54, plain, ~'m1$ufraenkel'(X0,X1,X2) | 'v1$uxboole$u0'(X2) | ~'m2$ufraenkel'(X3,X1,X2,X0) | 'm2$urelset$u1'(X3,X1,X2), inference(clausification, [status(esa)], [dt_m2_fraenkel])).
% 163.07/23.76  cnf(c55, plain, ~'m1$ufraenkel'(X0,X1,X2) | 'v1$uxboole$u0'(X2) | ~'m2$ufraenkel'(X3,X1,X2,X0) | 'v1$ufunct$u2'(X3,X1,X2), inference(clausification, [status(esa)], [dt_m2_fraenkel])).
% 163.07/23.76  cnf(c71, plain, ~'l1$ustruct$u0'(X0) | 'v3$ustruct$u0'(X0) | ~'v1$uxboole$u0'('u1$ustruct$u0'(X0)), inference(clausification, [status(esa)], [fc1_struct_0])).
% 163.07/23.76  cnf(c72, plain, 'v1$uxboole$u0'('k1$uxboole$u0'), inference(clausification, [status(esa)], [fc1_xboole_0])).
% 163.07/23.76  cnf(c89, plain, 'v1$uxboole$u0'(sK89), inference(clausification, [status(esa)], [rc1_xboole_0])).
% 163.07/23.76  cnf(c121, plain, ~'m1$urelset$u1'(X0,X1,X2) | ~'v1$ufunct$u2'(X0,X1,X2) | ~'v1$ufunct$u2'(X3,X4,X1) | 'v1$uxboole$u0'(X1) | 'k5$urelat$u1'(X3,X0) = 'k7$ufunct$u2'(X4,X1,X2,X3,X0) | ~'v1$ufunct$u1'(X3) | ~'m1$urelset$u1'(X3,X4,X1) | ~'v1$ufunct$u1'(X0), inference(clausification, [status(esa)], [redefinition_k7_funct_2])).
% 163.07/23.76  cnf(c122, plain, ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | 'k5$urelat$u1'(X3,X0) = 'k8$ugroup$u6'(X4,X1,X2,X3,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X4),'u1$ustruct$u0'(X1)) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X2) | ~'l1$ugroup$u1'(X2) | 'v3$ustruct$u0'(X1) | ~'v1$ufunct$u1'(X0) | ~'l1$ugroup$u1'(X4) | ~'v3$ugroup$u1'(X4) | ~'v1$ugroup$u6'(X0,X1,X2) | ~'v4$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X4) | 'v3$ustruct$u0'(X4) | 'v3$ustruct$u0'(X2) | ~'v1$ugroup$u6'(X3,X4,X1) | ~'m1$urelset$u1'(X3,'u1$ustruct$u0'(X4),'u1$ustruct$u0'(X1)) | ~'v1$ufunct$u1'(X3) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | ~'v3$ugroup$u1'(X2), inference(clausification, [status(esa)], [redefinition_k8_group_6])).
% 163.07/23.76  cnf(c123, plain, ~'m1$ufraenkel'(X0,X1,X2) | 'v1$uxboole$u0'(X2) | ~'m2$ufraenkel'(X3,X1,X2,X0) | 'm1$usubset$u1'(X3,X0), inference(clausification, [status(esa)], [redefinition_m2_fraenkel])).
% 163.07/23.76  cnf(c124, plain, ~'m1$ufraenkel'(X0,X1,X2) | 'v1$uxboole$u0'(X2) | 'm2$ufraenkel'(X3,X1,X2,X0) | ~'m1$usubset$u1'(X3,X0), inference(clausification, [status(esa)], [redefinition_m2_fraenkel])).
% 163.07/23.76  cnf(c125, plain, ~'m2$urelset$u1'(X0,X1,X2) | 'm1$urelset$u1'(X0,X1,X2), inference(clausification, [status(esa)], [redefinition_m2_relset_1])).
% 163.07/23.76  cnf(c128, plain, ~'r2$uhidden'(X0,X1) | 'm1$usubset$u1'(X0,X1), inference(clausification, [status(esa)], [t1_subset])).
% 163.07/23.76  cnf(c129, plain, ~'m1$usubset$u1'(X0,X1) | 'r2$uhidden'(X0,X1) | 'v1$uxboole$u0'(X1), inference(clausification, [status(esa)], [t2_subset])).
% 163.07/23.76  cnf(c133, plain, ~'v1$ufunct$u1'(X0) | ~'v3$ugroup$u1'(X1) | ~'m2$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X1)) | ~'v1$ugroup$u1'(X1) | ~'r2$uhidden'(X0,'k1$uautgroup'(X1)) | ~'v1$ugroup$u6'(X0,X1,X1) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | 'v4$ugroup$u6'(X0,X1,X1) | ~'v4$ugroup$u1'(X1), inference(clausification, [status(esa)], [t5_autgroup])).
% 163.07/23.76  cnf(c134, plain, ~'v1$ufunct$u1'(X0) | ~'v4$ugroup$u6'(X0,X1,X1) | ~'v3$ugroup$u1'(X1) | ~'m2$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X1)) | ~'v1$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,X1,X1) | 'r2$uhidden'(X0,'k1$uautgroup'(X1)) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1), inference(clausification, [status(esa)], [t5_autgroup])).
% 163.07/23.76  cnf(c136, plain, ~'v1$uxboole$u0'(X0) | X0 = 'k1$uxboole$u0', inference(clausification, [status(esa)], [t6_boole])).
% 163.07/23.76  cnf(c137, plain, ~'l1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X1) | ~'v3$ugroup$u1'(X1) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'v1$ufunct$u1'(X2) | ~'v4$ugroup$u6'(X3,X1,X4) | ~'l1$ugroup$u1'(X4) | ~'v4$ugroup$u6'(X2,X0,X1) | 'v3$ustruct$u0'(X4) | ~'v4$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X0) | 'v4$ugroup$u6'('k8$ugroup$u6'(X0,X1,X4,X2,X3),X0,X4) | ~'m2$urelset$u1'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X4)) | ~'m2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'v1$ugroup$u6'(X2,X0,X1) | ~'v1$ufunct$u1'(X3) | ~'v3$ugroup$u1'(X4) | ~'l1$ugroup$u1'(X1) | 'v3$ustruct$u0'(X0) | ~'v4$ugroup$u1'(X4) | ~'v1$ufunct$u2'(X3,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X4)) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X3,X1,X4), inference(clausification, [status(esa)], [t74_group_6])).
% 163.07/23.76  cnf(c139, plain, ~'v1$uxboole$u0'(X0) | ~'v1$uxboole$u0'(X1) | X1 = X0, inference(clausification, [status(esa)], [t8_boole])).
% 163.07/23.76  cnf(c140, plain, 'v1$ugroup$u1'(sK148), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c141, plain, 'v4$ugroup$u1'(sK148), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c142, plain, 'l1$ugroup$u1'(sK148), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c143, plain, 'v3$ugroup$u1'(sK148), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c144, plain, ~'v3$ustruct$u0'(sK148), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c145, plain, 'm2$ufraenkel'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'k1$uautgroup'(sK148)), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c146, plain, 'm2$ufraenkel'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'k1$uautgroup'(sK148)), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(c147, plain, ~'m2$ufraenkel'('k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'k1$uautgroup'(sK148)), inference(clausification, [status(esa)], [negated_conjecture])).
% 163.07/23.76  cnf(d0, plain, ~'v1$uxboole$u0'('k1$uautgroup'(X0)) | ~'l1$ugroup$u1'(X0) | ~'v1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X0), inference(resolution, [status(thm)], [c51,c41])).
% 163.07/23.76  cnf(d1, plain, sK89 = 'k1$uxboole$u0', inference(resolution, [status(thm)], [c136,c89])).
% 163.07/23.76  cnf(d2, plain, sK89 = X0 | ~'v1$uxboole$u0'(X0), inference(resolution, [status(thm)], [c139,c89])).
% 163.07/23.76  cnf(d3, plain, 'k1$uxboole$u0' = X0 | ~'v1$uxboole$u0'(X0), inference(demodulation, [status(thm)], [d2,d1])).
% 163.07/23.76  cnf(d4, plain, 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c123,c146])).
% 163.07/23.76  cnf(d5, plain, 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d4,c41])).
% 163.07/23.76  cnf(d6, plain, ~'l1$ugroup$u1'(sK148) | 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d5])).
% 163.07/23.76  cnf(d7, plain, ~'l1$ugroup$u1'(sK148) | 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d6])).
% 163.07/23.76  cnf(d8, plain, 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d7])).
% 163.07/23.76  cnf(d9, plain, 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d8])).
% 163.07/23.76  cnf(d10, plain, 'm1$usubset$u1'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d9])).
% 163.07/23.76  cnf(d11, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d10,c129])).
% 163.07/23.76  cnf(d12, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c54,c146])).
% 163.07/23.76  cnf(d13, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d12,c41])).
% 163.07/23.76  cnf(d14, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c140,d13])).
% 163.07/23.76  cnf(d15, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c141,d14])).
% 163.07/23.76  cnf(d16, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c142,d15])).
% 163.07/23.76  cnf(d17, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c143,d16])).
% 163.07/23.76  cnf(d18, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d17])).
% 163.07/23.76  cnf(d19, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c133,d18])).
% 163.07/23.76  cnf(d20, plain, ~'l1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c140,d19])).
% 163.07/23.76  cnf(d21, plain, ~'l1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c141,d20])).
% 163.07/23.76  cnf(d22, plain, ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c142,d21])).
% 163.07/23.76  cnf(d23, plain, ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c143,d22])).
% 163.07/23.76  cnf(d24, plain, ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c144,d23])).
% 163.07/23.76  cnf(d25, plain, 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c53,c146])).
% 163.07/23.76  cnf(d26, plain, 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d25,c41])).
% 163.07/23.76  cnf(d27, plain, ~'l1$ugroup$u1'(sK148) | 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d26])).
% 163.07/23.76  cnf(d28, plain, ~'l1$ugroup$u1'(sK148) | 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d27])).
% 163.07/23.76  cnf(d29, plain, 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d28])).
% 163.07/23.76  cnf(d30, plain, 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d29])).
% 163.07/23.76  cnf(d31, plain, 'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d30])).
% 163.07/23.76  cnf(d32, plain, 'v3$ustruct$u0'(sK148) | ~'l1$ustruct$u0'(sK148) | 'v1$ufunct$u1'(sK150), inference(resolution, [status(thm)], [c71,d31])).
% 163.07/23.76  cnf(d33, plain, 'v1$ufunct$u1'(sK150) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c144,d32])).
% 163.07/23.76  cnf(d34, plain, 'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c50,c142])).
% 163.07/23.76  cnf(d35, plain, 'v1$ufunct$u1'(sK150), inference(resolution, [status(thm)], [d34,d33])).
% 163.07/23.76  cnf(d36, plain, ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d35,d24])).
% 163.07/23.76  cnf(d37, plain, ~'Ts20'(sK148,'k1$uautgroup'(sK148)) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c24,c146])).
% 163.07/23.76  cnf(d38, plain, ~'l1$ugroup$u1'(X0) | ~'v1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v3$ugroup$u1'(X0) | ~'m1$ufraenkel'('k1$uautgroup'(X0),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) | ~'v4$ugroup$u1'(X0) | 'Ts20'(X0,'k1$uautgroup'(X0)), inference(equality_resolution, [status(thm)], [c20])).
% 163.07/23.76  cnf(d39, plain, ~'l1$ugroup$u1'(X0) | ~'v1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X0) | ~'v1$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X0) | 'Ts20'(X0,'k1$uautgroup'(X0)), inference(resolution, [status(thm)], [c41,d38])).
% 163.07/23.76  cnf(d40, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d39,d37])).
% 163.07/23.76  cnf(d41, plain, ~'l1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c140,d40])).
% 163.07/23.76  cnf(d42, plain, ~'l1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c141,d41])).
% 163.07/23.76  cnf(d43, plain, 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c142,d42])).
% 163.07/23.76  cnf(d44, plain, 'v3$ustruct$u0'(sK148) | 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c143,d43])).
% 163.07/23.76  cnf(d45, plain, 'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c144,d44])).
% 163.07/23.76  cnf(d46, plain, ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d45,d36])).
% 163.07/23.76  cnf(d47, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c55,c146])).
% 163.07/23.76  cnf(d48, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d47,c41])).
% 163.07/23.76  cnf(d49, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d48])).
% 163.07/23.76  cnf(d50, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d49])).
% 163.07/23.76  cnf(d51, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d50])).
% 163.07/23.76  cnf(d52, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d51])).
% 163.07/23.76  cnf(d53, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d52])).
% 163.07/23.76  cnf(d54, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'r2$uhidden'(sK150,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d53,d46])).
% 163.07/23.76  cnf(d55, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK150,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d54,d11])).
% 163.07/23.76  cnf(d56, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c55,c145])).
% 163.07/23.76  cnf(d57, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d56,c41])).
% 163.07/23.76  cnf(d58, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d57])).
% 163.07/23.76  cnf(d59, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d58])).
% 163.07/23.76  cnf(d60, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d59])).
% 163.07/23.76  cnf(d61, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d60])).
% 163.07/23.76  cnf(d62, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d61])).
% 163.07/23.76  cnf(d63, plain, 'k5$urelat$u1'(sK150,X0) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),X1,sK150,X0) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),X1) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),X1) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c121,d53])).
% 163.07/23.76  cnf(d64, plain, 'k5$urelat$u1'(sK150,X0) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),X1,sK150,X0) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),X1) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),X1), inference(resolution, [status(thm)], [d35,d63])).
% 163.07/23.76  cnf(d65, plain, 'm1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c125,d18])).
% 163.07/23.76  cnf(d66, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'k5$urelat$u1'(sK150,X0) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),X1,sK150,X0) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),X1) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),X1), inference(resolution, [status(thm)], [d65,d64])).
% 163.07/23.76  cnf(d67, plain, 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d66,d62])).
% 163.07/23.76  cnf(d68, plain, 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c53,c145])).
% 163.07/23.76  cnf(d69, plain, 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d68,c41])).
% 163.07/23.76  cnf(d70, plain, ~'l1$ugroup$u1'(sK148) | 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d69])).
% 163.07/23.76  cnf(d71, plain, ~'l1$ugroup$u1'(sK148) | 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d70])).
% 163.07/23.76  cnf(d72, plain, 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d71])).
% 163.07/23.76  cnf(d73, plain, 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d72])).
% 163.07/23.76  cnf(d74, plain, 'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d73])).
% 163.07/23.76  cnf(d75, plain, 'v3$ustruct$u0'(sK148) | ~'l1$ustruct$u0'(sK148) | 'v1$ufunct$u1'(sK149), inference(resolution, [status(thm)], [c71,d74])).
% 163.07/23.76  cnf(d76, plain, 'v1$ufunct$u1'(sK149) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c144,d75])).
% 163.07/23.76  cnf(d77, plain, 'v1$ufunct$u1'(sK149), inference(resolution, [status(thm)], [d34,d76])).
% 163.07/23.76  cnf(d78, plain, 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d77,d67])).
% 163.07/23.76  cnf(d79, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c54,c145])).
% 163.07/23.76  cnf(d80, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d79,c41])).
% 163.07/23.76  cnf(d81, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c140,d80])).
% 163.07/23.76  cnf(d82, plain, ~'l1$ugroup$u1'(sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c141,d81])).
% 163.07/23.76  cnf(d83, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c142,d82])).
% 163.07/23.76  cnf(d84, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c143,d83])).
% 163.07/23.76  cnf(d85, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'm2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d84])).
% 163.07/23.76  cnf(d86, plain, 'm1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c125,d85])).
% 163.07/23.76  cnf(d87, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d86,d78])).
% 163.07/23.76  cnf(d88, plain, 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149) | 'v3$ustruct$u0'(sK148) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [d87,c71])).
% 163.07/23.76  cnf(d89, plain, 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c144,d88])).
% 163.07/23.76  cnf(d90, plain, 'k5$urelat$u1'(sK150,sK149) = 'k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149), inference(resolution, [status(thm)], [d34,d89])).
% 163.07/23.76  cnf(d91, plain, ~'l1$ugroup$u1'(X0) | ~'v1$ugroup$u1'(X0) | 'r2$uhidden'('k7$ufunct$u2'('u1$ustruct$u0'(X0),X1,'u1$ustruct$u0'(X0),X2,X3),'k1$uautgroup'(X0)) | ~'v1$ufunct$u1'('k7$ufunct$u2'('u1$ustruct$u0'(X0),X1,'u1$ustruct$u0'(X0),X2,X3)) | ~'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(X0),X1,'u1$ustruct$u0'(X0),X2,X3),'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X0)) | 'v3$ustruct$u0'(X0) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X0) | ~'v1$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X0),X1,'u1$ustruct$u0'(X0),X2,X3),X0,X0) | ~'v4$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X0),X1,'u1$ustruct$u0'(X0),X2,X3),X0,X0) | ~'v1$ufunct$u1'(X2) | ~'v1$ufunct$u1'(X3) | 'v1$uxboole$u0'(X1) | ~'m1$urelset$u1'(X2,'u1$ustruct$u0'(X0),X1) | ~'m1$urelset$u1'(X3,X1,'u1$ustruct$u0'(X0)) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),X1) | ~'v1$ufunct$u2'(X3,X1,'u1$ustruct$u0'(X0)), inference(resolution, [status(thm)], [c134,c44])).
% 163.07/23.76  cnf(d92, plain, ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(X1) | 'v1$uxboole$u0'(X2) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X3),X2) | ~'m1$urelset$u1'(X1,X2,'u1$ustruct$u0'(X3)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X3),X2) | ~'v1$ufunct$u2'(X1,X2,'u1$ustruct$u0'(X3)) | ~'l1$ugroup$u1'(X3) | ~'v1$ugroup$u1'(X3) | 'r2$uhidden'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),'k1$uautgroup'(X3)) | ~'v1$ufunct$u1'(X1) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'(X2) | ~'m1$urelset$u1'(X1,X2,'u1$ustruct$u0'(X3)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X3),X2) | ~'v1$ufunct$u2'(X1,X2,'u1$ustruct$u0'(X3)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X3),X2) | ~'v1$ufunct$u2'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),'u1$ustruct$u0'(X3),'u1$ustruct$u0'(X3)) | 'v3$ustruct$u0'(X3) | ~'v3$ugroup$u1'(X3) | ~'v4$ugroup$u1'(X3) | ~'v1$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),X3,X3) | ~'v4$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),X3,X3), inference(resolution, [status(thm)], [c43,d91])).
% 163.07/23.76  cnf(d93, plain, ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(X1) | 'v1$uxboole$u0'(X2) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X3),X2) | ~'m1$urelset$u1'(X1,X2,'u1$ustruct$u0'(X3)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X3),X2) | ~'v1$ufunct$u2'(X1,X2,'u1$ustruct$u0'(X3)) | ~'l1$ugroup$u1'(X3) | ~'v1$ugroup$u1'(X3) | 'r2$uhidden'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),'k1$uautgroup'(X3)) | ~'v1$ufunct$u1'(X1) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'(X2) | ~'m1$urelset$u1'(X1,X2,'u1$ustruct$u0'(X3)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X3),X2) | ~'v1$ufunct$u2'(X1,X2,'u1$ustruct$u0'(X3)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X3),X2) | 'v3$ustruct$u0'(X3) | ~'v3$ugroup$u1'(X3) | ~'v4$ugroup$u1'(X3) | ~'v1$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),X3,X3) | ~'v4$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(X3),X2,'u1$ustruct$u0'(X3),X0,X1),X3,X3), inference(resolution, [status(thm)], [c45,d92])).
% 163.07/23.76  cnf(d94, plain, ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'r2$uhidden'('k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149),sK148,sK148), inference(superposition, [status(thm)], [d90,d93])).
% 163.07/23.76  cnf(d95, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(demodulation, [status(thm)], [d94,d90])).
% 163.07/23.76  cnf(d96, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(demodulation, [status(thm)], [d95,d90])).
% 163.07/23.76  cnf(d97, plain, ~'l1$ugroup$u1'(sK148) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [c140,d96])).
% 163.07/23.76  cnf(d98, plain, ~'l1$ugroup$u1'(sK148) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [c141,d97])).
% 163.07/23.76  cnf(d99, plain, 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [c142,d98])).
% 163.07/23.76  cnf(d100, plain, 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [c143,d99])).
% 163.07/23.76  cnf(d101, plain, 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [c144,d100])).
% 163.07/23.76  cnf(d102, plain, 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d35,d101])).
% 163.07/23.76  cnf(d103, plain, 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d77,d102])).
% 163.07/23.76  cnf(d104, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d62,d103])).
% 163.07/23.76  cnf(d105, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d53,d104])).
% 163.07/23.76  cnf(d106, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d86,d105])).
% 163.07/23.76  cnf(d107, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d65,d106])).
% 163.07/23.76  cnf(d108, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(sK148) | ~'l1$ugroup$u1'(X1) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(sK148) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v3$ugroup$u1'(X1) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(X1) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c122,d53])).
% 163.07/23.76  cnf(d109, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(X1) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c141,d108])).
% 163.07/23.76  cnf(d110, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(X1) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c142,d109])).
% 163.07/23.76  cnf(d111, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c143,d110])).
% 163.07/23.76  cnf(d112, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | ~'v1$ufunct$u1'(sK150) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c144,d111])).
% 163.07/23.76  cnf(d113, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d35,d112])).
% 163.07/23.76  cnf(d114, plain, 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1), inference(resolution, [status(thm)], [d45,d113])).
% 163.07/23.76  cnf(d115, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'k5$urelat$u1'(sK150,X0) = 'k8$ugroup$u6'(sK148,sK148,X1,sK150,X0) | ~'l1$ugroup$u1'(X1) | ~'v1$ufunct$u1'(X0) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | ~'v1$ugroup$u6'(X0,sK148,X1), inference(resolution, [status(thm)], [d65,d114])).
% 163.07/23.76  cnf(d116, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d115,d62])).
% 163.07/23.76  cnf(d117, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c141,d116])).
% 163.07/23.76  cnf(d118, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c142,d117])).
% 163.07/23.76  cnf(d119, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c143,d118])).
% 163.07/23.76  cnf(d120, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c144,d119])).
% 163.07/23.76  cnf(d121, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d77,d120])).
% 163.07/23.76  cnf(d122, plain, ~'Ts20'(sK148,'k1$uautgroup'(sK148)) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c24,c145])).
% 163.07/23.76  cnf(d123, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d39,d122])).
% 163.07/23.76  cnf(d124, plain, ~'l1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c140,d123])).
% 163.07/23.76  cnf(d125, plain, ~'l1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c141,d124])).
% 163.07/23.76  cnf(d126, plain, 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c142,d125])).
% 163.07/23.76  cnf(d127, plain, 'v3$ustruct$u0'(sK148) | 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c143,d126])).
% 163.07/23.76  cnf(d128, plain, 'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c144,d127])).
% 163.07/23.76  cnf(d129, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d128,d121])).
% 163.07/23.76  cnf(d130, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d86,d129])).
% 163.07/23.76  cnf(d131, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | 'v3$ustruct$u0'(sK148) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [d130,c71])).
% 163.07/23.76  cnf(d132, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c144,d131])).
% 163.07/23.76  cnf(d133, plain, 'k5$urelat$u1'(sK150,sK149) = 'k8$ugroup$u6'(sK148,sK148,sK148,sK150,sK149), inference(resolution, [status(thm)], [d34,d132])).
% 163.07/23.76  cnf(d134, plain, 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'l1$ugroup$u1'(sK148) | ~'l1$ugroup$u1'(sK148) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | 'v3$ustruct$u0'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(superposition, [status(thm)], [d133,c47])).
% 163.07/23.76  cnf(d135, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c141,d134])).
% 163.07/23.76  cnf(d136, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c142,d135])).
% 163.07/23.76  cnf(d137, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c143,d136])).
% 163.07/23.76  cnf(d138, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c144,d137])).
% 163.07/23.76  cnf(d139, plain, ~'v1$ufunct$u1'(sK149) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d35,d138])).
% 163.07/23.76  cnf(d140, plain, ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d77,d139])).
% 163.07/23.76  cnf(d141, plain, ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d45,d140])).
% 163.07/23.76  cnf(d142, plain, ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d128,d141])).
% 163.07/23.76  cnf(d143, plain, ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d142,d53])).
% 163.07/23.76  cnf(d144, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d62,d143])).
% 163.07/23.76  cnf(d145, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d86,d144])).
% 163.07/23.76  cnf(d146, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d65,d145])).
% 163.07/23.76  cnf(d147, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148), inference(resolution, [status(thm)], [d146,d107])).
% 163.07/23.76  cnf(d148, plain, 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'l1$ugroup$u1'(sK148) | ~'l1$ugroup$u1'(sK148) | ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | 'v3$ustruct$u0'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'(sK150,sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148), inference(superposition, [status(thm)], [d133,c137])).
% 163.07/23.76  cnf(d149, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c141,d148])).
% 163.07/23.76  cnf(d150, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c142,d149])).
% 163.07/23.76  cnf(d151, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c143,d150])).
% 163.07/23.76  cnf(d152, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u1'(sK150) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [c144,d151])).
% 163.07/23.76  cnf(d153, plain, ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d35,d152])).
% 163.07/23.76  cnf(d154, plain, ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'v1$ugroup$u6'(sK150,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d77,d153])).
% 163.07/23.76  cnf(d155, plain, ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d45,d154])).
% 163.07/23.76  cnf(d156, plain, ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d128,d155])).
% 163.07/23.76  cnf(d157, plain, ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d156,d18])).
% 163.07/23.76  cnf(d158, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'m2$urelset$u1'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d62,d157])).
% 163.07/23.76  cnf(d159, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK150,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d85,d158])).
% 163.07/23.76  cnf(d160, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'('k5$urelat$u1'(sK150,sK149),sK148,sK148) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d53,d159])).
% 163.07/23.76  cnf(d161, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148) | 'r2$uhidden'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [d160,d147])).
% 163.07/23.76  cnf(d162, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148) | 'm1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d161,c128])).
% 163.07/23.76  cnf(d163, plain, ~'m1$usubset$u1'('k7$ufunct$u2'('u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148),sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c124,c147])).
% 163.07/23.76  cnf(d164, plain, ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(demodulation, [status(thm)], [d163,d90])).
% 163.07/23.76  cnf(d165, plain, ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d164,c41])).
% 163.07/23.76  cnf(d166, plain, ~'l1$ugroup$u1'(sK148) | ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d165])).
% 163.07/23.76  cnf(d167, plain, ~'l1$ugroup$u1'(sK148) | ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d166])).
% 163.07/23.76  cnf(d168, plain, ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d167])).
% 163.07/23.76  cnf(d169, plain, ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d168])).
% 163.07/23.76  cnf(d170, plain, ~'m1$usubset$u1'('k5$urelat$u1'(sK150,sK149),'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d169])).
% 163.07/23.76  cnf(d171, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | ~'v4$ugroup$u6'(sK150,sK148,sK148), inference(resolution, [status(thm)], [d170,d162])).
% 163.07/23.76  cnf(d172, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v4$ugroup$u6'(sK149,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d171,d55])).
% 163.07/23.76  cnf(d173, plain, 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'m1$ufraenkel'('k1$uautgroup'(sK148),'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c123,c145])).
% 163.07/23.76  cnf(d174, plain, 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [d173,c41])).
% 163.07/23.76  cnf(d175, plain, ~'l1$ugroup$u1'(sK148) | 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d174])).
% 163.07/23.76  cnf(d176, plain, ~'l1$ugroup$u1'(sK148) | 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d175])).
% 163.07/23.76  cnf(d177, plain, 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d176])).
% 163.07/23.76  cnf(d178, plain, 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d177])).
% 163.07/23.76  cnf(d179, plain, 'm1$usubset$u1'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c144,d178])).
% 163.07/23.76  cnf(d180, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d179,c129])).
% 163.07/23.76  cnf(d181, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)), inference(resolution, [status(thm)], [c133,d85])).
% 163.07/23.76  cnf(d182, plain, ~'l1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c140,d181])).
% 163.07/23.76  cnf(d183, plain, ~'l1$ugroup$u1'(sK148) | ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c141,d182])).
% 163.07/23.76  cnf(d184, plain, ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c142,d183])).
% 163.07/23.76  cnf(d185, plain, ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v3$ustruct$u0'(sK148) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c143,d184])).
% 163.07/23.76  cnf(d186, plain, ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | ~'v1$ufunct$u1'(sK149) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [c144,d185])).
% 163.07/23.76  cnf(d187, plain, ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | ~'v1$ugroup$u6'(sK149,sK148,sK148) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d77,d186])).
% 163.07/23.76  cnf(d188, plain, ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'v1$ufunct$u2'(sK149,'u1$ustruct$u0'(sK148),'u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d128,d187])).
% 163.07/23.76  cnf(d189, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | ~'r2$uhidden'(sK149,'k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK149,sK148,sK148), inference(resolution, [status(thm)], [d62,d188])).
% 163.07/23.76  cnf(d190, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v4$ugroup$u6'(sK149,sK148,sK148) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d189,d180])).
% 163.07/23.76  cnf(d191, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)) | 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'v1$uxboole$u0'('k1$uautgroup'(sK148)), inference(resolution, [status(thm)], [d190,d172])).
% 163.07/23.76  cnf(d192, plain, 'v1$uxboole$u0'('u1$ustruct$u0'(sK148)) | 'k1$uxboole$u0' = 'k1$uautgroup'(sK148), inference(resolution, [status(thm)], [d191,d3])).
% 163.07/23.76  cnf(d193, plain, 'k1$uxboole$u0' = 'k1$uautgroup'(sK148) | 'v3$ustruct$u0'(sK148) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [d192,c71])).
% 163.07/23.76  cnf(d194, plain, 'k1$uxboole$u0' = 'k1$uautgroup'(sK148) | ~'l1$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c144,d193])).
% 163.07/23.76  cnf(d195, plain, 'k1$uxboole$u0' = 'k1$uautgroup'(sK148), inference(resolution, [status(thm)], [d34,d194])).
% 163.07/23.76  cnf(d196, plain, ~'v1$uxboole$u0'('k1$uxboole$u0') | ~'l1$ugroup$u1'(sK148) | ~'v1$ugroup$u1'(sK148) | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(superposition, [status(thm)], [d195,d0])).
% 163.07/23.76  cnf(d197, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$uxboole$u0'('k1$uxboole$u0') | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148) | ~'v4$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c140,d196])).
% 163.07/23.76  cnf(d198, plain, ~'l1$ugroup$u1'(sK148) | ~'v1$uxboole$u0'('k1$uxboole$u0') | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c141,d197])).
% 163.07/23.76  cnf(d199, plain, ~'v1$uxboole$u0'('k1$uxboole$u0') | 'v3$ustruct$u0'(sK148) | ~'v3$ugroup$u1'(sK148), inference(resolution, [status(thm)], [c142,d198])).
% 163.07/23.76  cnf(d200, plain, ~'v1$uxboole$u0'('k1$uxboole$u0') | 'v3$ustruct$u0'(sK148), inference(resolution, [status(thm)], [c143,d199])).
% 163.07/23.76  cnf(d201, plain, ~'v1$uxboole$u0'('k1$uxboole$u0'), inference(resolution, [status(thm)], [c144,d200])).
% 163.07/23.76  cnf(d202, plain, $false, inference(resolution, [status(thm)], [c72,d201])).
% 163.07/23.76  % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------