LisaST---0.9.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : LisaST---0.9
% Problem  : SEU401+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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 08:41:53 AM UTC 2026

% Result   : Theorem 67.86s 16.85s
% Output   : CNFRefutation 67.86s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SEU401+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04  % Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n012.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Sat Sep 26 09:27:04 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.08/0.35  Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.86/16.85  % SZS status Theorem for theBenchmark.p
% 67.86/16.85  % SZS output start CNFRefutation for theBenchmark.p
% 67.86/16.85  fof(redefinition_m2_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('relation$uof2$uas$usubset'(X2,X0,X1) <=> 'relation$uof2'(X2,X0,X1)))).
% 67.86/16.85  fof(dt_k5_waybel_9, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('one$usorted$ustr'(X0) & (~'empty$ucarrier'(X1) & ('net$ustr'(X1,X0) & element(X2,'the$ucarrier'(X1)))))) => ('strict$unet$ustr'('netstr$urestr$uto$uelement'(X0,X1,X2),X0) & 'net$ustr'('netstr$urestr$uto$uelement'(X0,X1,X2),X0))))).
% 67.86/16.85  fof(redefinition_k5_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('relation$uof2'(X2,X0,X1) => 'relation$urng$uas$usubset'(X0,X1,X2) = 'relation$urng'(X2)))).
% 67.86/16.85  fof(redefinition_k6_waybel_9, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('one$usorted$ustr'(X0) & (~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & ('net$ustr'(X1,X0) & element(X2,'the$ucarrier'(X1)))))))) => 'subnetstr$uof$uelement'(X0,X1,X2) = 'netstr$urestr$uto$uelement'(X0,X1,X2)))).
% 67.86/16.85  fof(dt_l1_pre_topc, axiom, ! [X0] : (('top$ustr'(X0) => 'one$usorted$ustr'(X0)))).
% 67.86/16.85  fof(dt_u1_waybel_0, axiom, ! [X0] : ! [X1] : ((('one$usorted$ustr'(X0) & 'net$ustr'(X1,X0)) => (function('the$umapping'(X0,X1)) & ('quasi$utotal'('the$umapping'(X0,X1),'the$ucarrier'(X1),'the$ucarrier'(X0)) & 'relation$uof2$uas$usubset'('the$umapping'(X0,X1),'the$ucarrier'(X1),'the$ucarrier'(X0))))))).
% 67.86/16.85  fof(t2_tarski, axiom, ! [X0] : ! [X1] : ((! [X2] : ((in(X2,X0) <=> in(X2,X1))) => X0 = X1))).
% 67.86/16.85  fof(s2_xboole_0__e6_39_3__yellow19__1, conjecture, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & ('top$ustr'(X0) & (~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0))))))) => ! [X3] : ! [X4] : ! [X5] : (((! [X6] : ((in(X6,X4) <=> (in(X6,'the$ucarrier'(X1)) & ? [X7] : (('netstr$uinduced$usubset'(X7,X0,X1) & ? [X8] : ((element(X8,'the$ucarrier'(X1)) & (X3 = 'topstr$uclosure'(X0,X7) & (X6 = X8 & X7 = 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X0,X1,X8)),'the$ucarrier'(X0),'the$umapping'(X0,'subnetstr$uof$uelement'(X0,X1,X8)))))))))))) & ! [X6] : ((in(X6,X5) <=> (in(X6,'the$ucarrier'(X1)) & ? [X9] : (('netstr$uinduced$usubset'(X9,X0,X1) & ? [X10] : ((element(X10,'the$ucarrier'(X1)) & (X3 = 'topstr$uclosure'(X0,X9) & (X6 = X10 & X9 = 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X0,X1,X10)),'the$ucarrier'(X0),'the$umapping'(X0,'subnetstr$uof$uelement'(X0,X1,X10))))))))))))) => X4 = X5))))).
% 67.86/16.85  fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & ('top$ustr'(X0) & (~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0))))))) => ! [X3] : ! [X4] : ! [X5] : (((! [X6] : ((in(X6,X4) <=> (in(X6,'the$ucarrier'(X1)) & ? [X7] : (('netstr$uinduced$usubset'(X7,X0,X1) & ? [X8] : ((element(X8,'the$ucarrier'(X1)) & (X3 = 'topstr$uclosure'(X0,X7) & (X6 = X8 & X7 = 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X0,X1,X8)),'the$ucarrier'(X0),'the$umapping'(X0,'subnetstr$uof$uelement'(X0,X1,X8)))))))))))) & ! [X6] : ((in(X6,X5) <=> (in(X6,'the$ucarrier'(X1)) & ? [X9] : (('netstr$uinduced$usubset'(X9,X0,X1) & ? [X10] : ((element(X10,'the$ucarrier'(X1)) & (X3 = 'topstr$uclosure'(X0,X9) & (X6 = X10 & X9 = 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X0,X1,X10)),'the$ucarrier'(X0),'the$umapping'(X0,'subnetstr$uof$uelement'(X0,X1,X10))))))))))))) => X4 = X5)))), inference(negate_conjecture, [status(cth)], [s2_xboole_0__e6_39_3__yellow19__1])).
% 67.86/16.85  cnf(c96, plain, ~'relation$uof2$uas$usubset'(X0,X1,X2) | 'relation$uof2'(X0,X1,X2), inference(clausification, [status(esa)], [redefinition_m2_relset_1])).
% 67.86/16.85  cnf(c99, plain, 'net$ustr'('netstr$urestr$uto$uelement'(X0,X1,X2),X0) | ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X1) | 'empty$ucarrier'(X0) | ~element(X2,'the$ucarrier'(X1)) | ~'net$ustr'(X1,X0), inference(clausification, [status(esa)], [dt_k5_waybel_9])).
% 67.86/16.85  cnf(c130, plain, ~'relation$uof2'(X0,X1,X2) | 'relation$urng'(X0) = 'relation$urng$uas$usubset'(X1,X2,X0), inference(clausification, [status(esa)], [redefinition_k5_relset_1])).
% 67.86/16.85  cnf(c131, plain, ~'net$ustr'(X0,X1) | ~'directed$urelstr'(X0) | ~'one$usorted$ustr'(X1) | ~'transitive$urelstr'(X0) | 'empty$ucarrier'(X1) | 'netstr$urestr$uto$uelement'(X1,X0,X2) = 'subnetstr$uof$uelement'(X1,X0,X2) | ~element(X2,'the$ucarrier'(X0)) | 'empty$ucarrier'(X0), inference(clausification, [status(esa)], [redefinition_k6_waybel_9])).
% 67.86/16.85  cnf(c136, plain, ~'top$ustr'(X0) | 'one$usorted$ustr'(X0), inference(clausification, [status(esa)], [dt_l1_pre_topc])).
% 67.86/16.85  cnf(c140, plain, ~'net$ustr'(X0,X1) | ~'one$usorted$ustr'(X1) | 'relation$uof2$uas$usubset'('the$umapping'(X1,X0),'the$ucarrier'(X0),'the$ucarrier'(X1)), inference(clausification, [status(esa)], [dt_u1_waybel_0])).
% 67.86/16.85  cnf(c143, plain, in(sK136(X0,X1),X0) | in(sK136(X0,X1),X1) | X1 = X0, inference(clausification, [status(esa)], [t2_tarski])).
% 67.86/16.85  cnf(c144, plain, ~in(sK136(X0,X1),X1) | ~in(sK136(X0,X1),X0) | X1 = X0, inference(clausification, [status(esa)], [t2_tarski])).
% 67.86/16.85  cnf(c147, plain, ~'empty$ucarrier'(sK140), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c148, plain, 'directed$urelstr'(sK140), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c149, plain, 'net$ustr'(sK140,sK139), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c150, plain, 'transitive$urelstr'(sK140), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c151, plain, 'top$ustr'(sK139), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c152, plain, ~'empty$ucarrier'(sK139), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c153, plain, ~in(X0,sK144) | X1(sK139,sK140,sK142,X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c154, plain, ~element(X0,'the$ucarrier'(sK140)) | ~'netstr$uinduced$usubset'(X1,sK139,sK140) | X0 != X2 | in(X2,sK144) | ~in(X2,'the$ucarrier'(sK140)) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,X0)),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,X0))) != X1 | 'topstr$uclosure'(sK139,X1) != sK142, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c155, plain, ~in(X0,sK143) | X1(sK139,sK140,sK142,X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c156, plain, ~element(X0,'the$ucarrier'(sK140)) | X0 != X1 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,X0)),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,X0))) != X2 | ~'netstr$uinduced$usubset'(X2,sK139,sK140) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | 'topstr$uclosure'(sK139,X2) != sK142, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c157, plain, sK144 != sK143, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c158, plain, ~X0(X1,X2,X3,X4) | in(X4,'the$ucarrier'(X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c159, plain, ~X0(X1,X2,X3,X4) | 'netstr$uinduced$usubset'(sK151(X4,X3,X2,X1),X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c160, plain, ~X0(X1,X2,X3,X4) | element(sK152(X4,X3,X2,X1),'the$ucarrier'(X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c161, plain, ~X0(X1,X2,X3,X4) | sK152(X4,X3,X2,X1) = X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c162, plain, ~X0(X1,X2,X3,X4) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X1,X2,sK152(X4,X3,X2,X1))),'the$ucarrier'(X1),'the$umapping'(X1,'subnetstr$uof$uelement'(X1,X2,sK152(X4,X3,X2,X1)))) = sK151(X4,X3,X2,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c163, plain, ~X0(X1,X2,X3,X4) | 'topstr$uclosure'(X1,sK151(X4,X3,X2,X1)) = X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c164, plain, ~X0(X1,X2,X3,X4) | in(X4,'the$ucarrier'(X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c165, plain, ~X0(X1,X2,X3,X4) | 'netstr$uinduced$usubset'(sK153(X4,X3,X1,X2),X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c166, plain, ~X0(X1,X2,X3,X4) | element(sK154(X4,X3,X1,X2),'the$ucarrier'(X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c167, plain, ~X0(X1,X2,X3,X4) | sK154(X4,X3,X1,X2) = X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c168, plain, ~X0(X1,X2,X3,X4) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(X1,X2,sK154(X4,X3,X1,X2))),'the$ucarrier'(X1),'the$umapping'(X1,'subnetstr$uof$uelement'(X1,X2,sK154(X4,X3,X1,X2)))) = sK153(X4,X3,X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(c169, plain, ~X0(X1,X2,X3,X4) | 'topstr$uclosure'(X1,sK153(X4,X3,X1,X2)) = X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.86/16.85  cnf(d0, plain, in(X0,'the$ucarrier'(sK140)) | ~in(X0,sK143), inference(resolution, [status(thm)], [c164,c155])).
% 67.86/16.85  cnf(d1, plain, 'topstr$uclosure'(sK139,sK151(X0,sK142,sK140,sK139)) = sK142 | ~in(X0,sK144), inference(resolution, [status(thm)], [c163,c153])).
% 67.86/16.85  cnf(d2, plain, sK144 = X0 | in(sK136(X0,sK144),X0) | 'topstr$uclosure'(sK139,sK151(sK136(X0,sK144),sK142,sK140,sK139)) = sK142, inference(resolution, [status(thm)], [c143,d1])).
% 67.86/16.85  cnf(d3, plain, sK154(X0,sK142,sK139,sK140) = X0 | ~in(X0,sK143), inference(resolution, [status(thm)], [c167,c155])).
% 67.86/16.85  cnf(d4, plain, X0 = sK143 | in(sK136(sK143,X0),X0) | sK154(sK136(sK143,X0),sK142,sK139,sK140) = sK136(sK143,X0), inference(resolution, [status(thm)], [c143,d3])).
% 67.86/16.85  cnf(d5, plain, sK152(X0,sK142,sK140,sK139) = X0 | ~in(X0,sK144), inference(resolution, [status(thm)], [c161,c153])).
% 67.86/16.85  cnf(d6, plain, sK144 = X0 | in(sK136(X0,sK144),X0) | sK152(sK136(X0,sK144),sK142,sK140,sK139) = sK136(X0,sK144), inference(resolution, [status(thm)], [c143,d5])).
% 67.86/16.85  cnf(d7, plain, sK144 = sK143 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d6,d3])).
% 67.86/16.85  cnf(d8, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d7])).
% 67.86/16.85  cnf(d9, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d8,c166])).
% 67.86/16.85  cnf(d10, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d9,c155])).
% 67.86/16.85  cnf(d11, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(X0,sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(X0,sK142,sK139,sK140)))) = sK153(X0,sK142,sK139,sK140) | ~in(X0,sK143), inference(resolution, [status(thm)], [c168,c155])).
% 67.86/16.85  cnf(d12, plain, sK144 = sK143 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [d6,d11])).
% 67.86/16.85  cnf(d13, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d12])).
% 67.86/16.85  cnf(d14, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d8,d13])).
% 67.86/16.85  cnf(d15, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d8,d14])).
% 67.86/16.85  cnf(d16, plain, sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK136(sK143,sK144) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d15,c154])).
% 67.86/16.85  cnf(d17, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) != sK142 | sK136(sK143,sK144) != X0 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d16])).
% 67.86/16.85  cnf(d18, plain, 'topstr$uclosure'(sK139,sK153(X0,sK142,sK139,sK140)) = sK142 | ~in(X0,sK143), inference(resolution, [status(thm)], [c169,c155])).
% 67.86/16.85  cnf(d19, plain, sK144 = sK143 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [d6,d18])).
% 67.86/16.85  cnf(d20, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d19])).
% 67.86/16.85  cnf(d21, plain, sK142 != sK142 | sK136(sK143,sK144) != X0 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d20,d17])).
% 67.86/16.85  cnf(d22, plain, sK142 != sK142 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d21])).
% 67.86/16.85  cnf(d23, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d22])).
% 67.86/16.85  cnf(d24, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d23,c165])).
% 67.86/16.85  cnf(d25, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d24,c155])).
% 67.86/16.85  cnf(d26, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d25,d0])).
% 67.86/16.85  cnf(d27, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d26,d10])).
% 67.86/16.85  cnf(d28, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | in(sK136(sK143,sK144),sK144) | sK144 = sK143 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d27,d6])).
% 67.86/16.85  cnf(d29, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d28])).
% 67.86/16.85  cnf(d30, plain, sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d29,d5])).
% 67.86/16.85  cnf(d31, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~'Ts137'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d30,c160])).
% 67.86/16.85  cnf(d32, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d31,c153])).
% 67.86/16.85  cnf(d33, plain, in(X0,'the$ucarrier'(sK140)) | ~in(X0,sK144), inference(resolution, [status(thm)], [c158,c153])).
% 67.86/16.85  cnf(d34, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(X0,sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(X0,sK142,sK140,sK139)))) = sK151(X0,sK142,sK140,sK139) | ~in(X0,sK144), inference(resolution, [status(thm)], [c162,c153])).
% 67.86/16.85  cnf(d35, plain, sK144 = sK143 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(resolution, [status(thm)], [d4,d34])).
% 67.86/16.85  cnf(d36, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d35])).
% 67.86/16.85  cnf(d37, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK152(sK136(sK143,sK144),sK142,sK140,sK139),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d36,c156])).
% 67.86/16.85  cnf(d38, plain, 'topstr$uclosure'(sK139,X0) != sK142 | sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK136(sK143,sK144) != X1 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK152(sK136(sK143,sK144),sK142,sK140,sK139),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d37,d30])).
% 67.86/16.85  cnf(d39, plain, 'topstr$uclosure'(sK139,X0) != sK142 | sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK136(sK143,sK144) != X1 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d38,d30])).
% 67.86/16.85  cnf(d40, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) != sK142 | sK136(sK143,sK144) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d39])).
% 67.86/16.85  cnf(d41, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK144 = sK143 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d2,d3])).
% 67.86/16.85  cnf(d42, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d41])).
% 67.86/16.85  cnf(d43, plain, sK142 != sK142 | sK136(sK143,sK144) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d42,d40])).
% 67.86/16.85  cnf(d44, plain, sK142 != sK142 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d43])).
% 67.86/16.85  cnf(d45, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d44])).
% 67.86/16.85  cnf(d46, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'Ts137'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d45,c159])).
% 67.86/16.85  cnf(d47, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d46,c153])).
% 67.86/16.85  cnf(d48, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d47,d33])).
% 67.86/16.85  cnf(d49, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d48,d32])).
% 67.86/16.85  cnf(d50, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | in(sK136(sK143,sK144),sK143) | sK144 = sK143 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d49,d4])).
% 67.86/16.85  cnf(d51, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c157,d50])).
% 67.86/16.85  cnf(d52, plain, sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d51,d3])).
% 67.86/16.85  cnf(d53, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d52,c166])).
% 67.86/16.85  cnf(d54, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d53,c155])).
% 67.86/16.85  cnf(d55, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK144 = sK143 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [d2,d11])).
% 67.86/16.85  cnf(d56, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [c157,d55])).
% 67.86/16.85  cnf(d57, plain, sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140) | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142, inference(superposition, [status(thm)], [d56,c154])).
% 67.86/16.85  cnf(d58, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(equality_resolution, [status(thm)], [d57])).
% 67.86/16.85  cnf(d59, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d58,d52])).
% 67.86/16.85  cnf(d60, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d59,d52])).
% 67.86/16.85  cnf(d61, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d60,d52])).
% 67.86/16.85  cnf(d62, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d61])).
% 67.86/16.85  cnf(d63, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK144 = sK143 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [d2,d18])).
% 67.86/16.85  cnf(d64, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [c157,d63])).
% 67.86/16.85  cnf(d65, plain, sK142 != sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140) | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142, inference(superposition, [status(thm)], [d64,d62])).
% 67.86/16.85  cnf(d66, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d65])).
% 67.86/16.85  cnf(d67, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d66,c165])).
% 67.86/16.85  cnf(d68, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d67,c155])).
% 67.86/16.85  cnf(d69, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d68,d0])).
% 67.86/16.85  cnf(d70, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d69,d54])).
% 67.86/16.85  cnf(d71, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | in(sK136(sK143,sK144),sK144) | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | sK144 = sK143, inference(resolution, [status(thm)], [d70,d2])).
% 67.86/16.85  cnf(d72, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d71])).
% 67.86/16.85  cnf(d73, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142 | 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) = sK142, inference(resolution, [status(thm)], [d72,d1])).
% 67.86/16.85  cnf(d74, plain, ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0) | 'relation$uof2'('the$umapping'(X0,X1),'the$ucarrier'(X1),'the$ucarrier'(X0)), inference(resolution, [status(thm)], [c140,c96])).
% 67.86/16.85  cnf(d75, plain, ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0) | 'relation$urng'('the$umapping'(X0,X1)) = 'relation$urng$uas$usubset'('the$ucarrier'(X1),'the$ucarrier'(X0),'the$umapping'(X0,X1)), inference(resolution, [status(thm)], [d74,c130])).
% 67.86/16.85  cnf(d76, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,X1,X2))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,X1,X2)),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,X1,X2))) | ~'one$usorted$ustr'(X0) | ~element(X2,'the$ucarrier'(X1)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(X1) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0), inference(resolution, [status(thm)], [d75,c99])).
% 67.86/16.85  cnf(d77, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(sK140) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d76,d54])).
% 67.86/16.85  cnf(d78, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c147,d77])).
% 67.86/16.85  cnf(d79, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | sK144 = sK143 | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d78,c143])).
% 67.86/16.85  cnf(d80, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d79])).
% 67.86/16.85  cnf(d81, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(sK139) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d80,c149])).
% 67.86/16.85  cnf(d82, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c152,d81])).
% 67.86/16.85  cnf(d83, plain, 'one$usorted$ustr'(sK139), inference(resolution, [status(thm)], [c136,c151])).
% 67.86/16.85  cnf(d84, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d83,d82])).
% 67.86/16.85  cnf(d85, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(sK140) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d76,d32])).
% 67.86/16.85  cnf(d86, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c147,d85])).
% 67.86/16.85  cnf(d87, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | sK144 = sK143 | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d86,c143])).
% 67.86/16.85  cnf(d88, plain, 'relation$urng'('the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144))),'the$ucarrier'(X0),'the$umapping'(X0,'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c157,d87])).
% 67.86/16.85  cnf(d89, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | 'empty$ucarrier'(sK139) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d88,c149])).
% 67.86/16.85  cnf(d90, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c152,d89])).
% 67.86/16.85  cnf(d91, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d83,d90])).
% 67.86/16.85  cnf(d92, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | sK144 = sK143 | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d91,c144])).
% 67.86/16.85  cnf(d93, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d92])).
% 67.86/16.85  cnf(d94, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))), inference(resolution, [status(thm)], [d93,d84])).
% 67.86/16.85  cnf(d95, plain, 'netstr$urestr$uto$uelement'(X0,X1,sK154(X2,X3,X4,X1)) = 'subnetstr$uof$uelement'(X0,X1,sK154(X2,X3,X4,X1)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(X1) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0) | ~'directed$urelstr'(X1) | ~'transitive$urelstr'(X1) | ~'Ts138'(X4,X1,X3,X2), inference(resolution, [status(thm)], [c131,c166])).
% 67.86/16.85  cnf(d96, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) | 'empty$ucarrier'(sK140) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140) | ~in(X1,sK143), inference(resolution, [status(thm)], [d95,c155])).
% 67.86/16.85  cnf(d97, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140) | ~in(X1,sK143), inference(resolution, [status(thm)], [c147,d96])).
% 67.86/16.85  cnf(d98, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'transitive$urelstr'(sK140) | ~in(X1,sK143), inference(resolution, [status(thm)], [c148,d97])).
% 67.86/16.85  cnf(d99, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(X0,sK140,sK154(X1,sK142,sK139,sK140)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(X1,sK143), inference(resolution, [status(thm)], [c150,d98])).
% 67.86/16.85  cnf(d100, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK154(sK136(sK143,X1),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(X0,sK140,sK154(sK136(sK143,X1),sK142,sK139,sK140)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | X1 = sK143 | in(sK136(sK143,X1),X1), inference(resolution, [status(thm)], [d99,c143])).
% 67.86/16.85  cnf(d101, plain, X0 = sK143 | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) | 'empty$ucarrier'(sK139) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,X0),X0), inference(resolution, [status(thm)], [d100,c149])).
% 67.86/16.85  cnf(d102, plain, X0 = sK143 | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,X0),X0), inference(resolution, [status(thm)], [c152,d101])).
% 67.86/16.85  cnf(d103, plain, X0 = sK143 | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,X0),sK142,sK139,sK140)) | in(sK136(sK143,X0),X0), inference(resolution, [status(thm)], [d83,d102])).
% 67.86/16.85  cnf(d104, plain, sK144 = sK143 | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d103,d5])).
% 67.86/16.85  cnf(d105, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d104])).
% 67.86/16.85  cnf(d106, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d8,d105])).
% 67.86/16.85  cnf(d107, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144) | sK152(sK136(sK143,sK144),sK142,sK140,sK139) = sK136(sK143,sK144), inference(superposition, [status(thm)], [d8,d106])).
% 67.86/16.85  cnf(d108, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~'Ts137'(sK139,sK140,sK142,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d107,c160])).
% 67.86/16.85  cnf(d109, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d108,c153])).
% 67.86/16.85  cnf(d110, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | ~in(sK136(sK143,sK144),sK144) | 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(sK140) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140), inference(resolution, [status(thm)], [d109,c131])).
% 67.86/16.85  cnf(d111, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c147,d110])).
% 67.86/16.85  cnf(d112, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'transitive$urelstr'(sK140) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c148,d111])).
% 67.86/16.85  cnf(d113, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c150,d112])).
% 67.86/16.85  cnf(d114, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | sK144 = sK143 | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d113,c143])).
% 67.86/16.85  cnf(d115, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(X0,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c157,d114])).
% 67.86/16.85  cnf(d116, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'empty$ucarrier'(sK139) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d115,c149])).
% 67.86/16.85  cnf(d117, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | ~'one$usorted$ustr'(sK139) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c152,d116])).
% 67.86/16.85  cnf(d118, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d83,d117])).
% 67.86/16.85  cnf(d119, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK144 = sK143 | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d118,c144])).
% 67.86/16.85  cnf(d120, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d119])).
% 67.86/16.85  cnf(d121, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK144 = sK143 | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)), inference(resolution, [status(thm)], [d120,d103])).
% 67.86/16.85  cnf(d122, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)), inference(resolution, [status(thm)], [c157,d121])).
% 67.86/16.85  cnf(d123, plain, 'netstr$urestr$uto$uelement'(X0,X1,sK152(X2,X3,X1,X4)) = 'subnetstr$uof$uelement'(X0,X1,sK152(X2,X3,X1,X4)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(X1) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0) | ~'directed$urelstr'(X1) | ~'transitive$urelstr'(X1) | ~'Ts137'(X4,X1,X3,X2), inference(resolution, [status(thm)], [c131,c160])).
% 67.86/16.85  cnf(d124, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) | 'empty$ucarrier'(sK140) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140) | ~in(X1,sK144), inference(resolution, [status(thm)], [d123,c153])).
% 67.86/16.85  cnf(d125, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'directed$urelstr'(sK140) | ~'transitive$urelstr'(sK140) | ~in(X1,sK144), inference(resolution, [status(thm)], [c147,d124])).
% 67.86/16.85  cnf(d126, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~'transitive$urelstr'(sK140) | ~in(X1,sK144), inference(resolution, [status(thm)], [c148,d125])).
% 67.86/16.85  cnf(d127, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(X0,sK140,sK152(X1,sK142,sK140,sK139)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | ~in(X1,sK144), inference(resolution, [status(thm)], [c150,d126])).
% 67.86/16.85  cnf(d128, plain, 'netstr$urestr$uto$uelement'(X0,sK140,sK152(sK136(X1,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(X0,sK140,sK152(sK136(X1,sK144),sK142,sK140,sK139)) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~'net$ustr'(sK140,X0) | sK144 = X1 | in(sK136(X1,sK144),X1), inference(resolution, [status(thm)], [d127,c143])).
% 67.86/16.85  cnf(d129, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) | sK144 = X0 | 'empty$ucarrier'(sK139) | ~'one$usorted$ustr'(sK139) | in(sK136(X0,sK144),X0), inference(resolution, [status(thm)], [d128,c149])).
% 67.86/16.85  cnf(d130, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) | sK144 = X0 | ~'one$usorted$ustr'(sK139) | in(sK136(X0,sK144),X0), inference(resolution, [status(thm)], [c152,d129])).
% 67.86/16.85  cnf(d131, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)) | sK144 = X0 | in(sK136(X0,sK144),X0), inference(resolution, [status(thm)], [d83,d130])).
% 67.86/16.85  cnf(d132, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)) | sK144 = sK143 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [d131,d3])).
% 67.86/16.85  cnf(d133, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144), inference(resolution, [status(thm)], [c157,d132])).
% 67.86/16.85  cnf(d134, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d107,d133])).
% 67.86/16.85  cnf(d135, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | sK154(sK136(sK143,sK144),sK142,sK139,sK140) = sK136(sK143,sK144) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d107,d134])).
% 67.86/16.85  cnf(d136, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d135,d122])).
% 67.86/16.85  cnf(d137, plain, 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)) | 'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)) = 'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d135,d136])).
% 67.86/16.85  cnf(d138, plain, X0 = sK143 | in(sK136(sK143,X0),X0) | 'topstr$uclosure'(sK139,sK153(sK136(sK143,X0),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [c143,d18])).
% 67.86/16.85  cnf(d139, plain, sK144 = sK143 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(resolution, [status(thm)], [d138,d34])).
% 67.86/16.85  cnf(d140, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(resolution, [status(thm)], [c157,d139])).
% 67.86/16.85  cnf(d141, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK152(sK136(sK143,sK144),sK142,sK140,sK139) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK152(sK136(sK143,sK144),sK142,sK140,sK139),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140) | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(superposition, [status(thm)], [d140,c156])).
% 67.86/16.85  cnf(d142, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK136(sK143,sK144) != X1 | ~element(sK152(sK136(sK143,sK144),sK142,sK140,sK139),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d141,d30])).
% 67.86/16.85  cnf(d143, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d142,d30])).
% 67.86/16.85  cnf(d144, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) != sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d143])).
% 67.86/16.85  cnf(d145, plain, sK142 != sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(demodulation, [status(thm)], [d144,d73])).
% 67.86/16.85  cnf(d146, plain, sK142 != sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d145])).
% 67.86/16.85  cnf(d147, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d146])).
% 67.86/16.85  cnf(d148, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'Ts137'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d147,c159])).
% 67.86/16.85  cnf(d149, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d148,c153])).
% 67.86/16.85  cnf(d150, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d149,d33])).
% 67.86/16.85  cnf(d151, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d150,d32])).
% 67.86/16.85  cnf(d152, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | in(sK136(sK143,sK144),sK143) | sK144 = sK143 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [d151,d138])).
% 67.86/16.85  cnf(d153, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c157,d152])).
% 67.86/16.85  cnf(d154, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [d153,d18])).
% 67.86/16.85  cnf(d155, plain, sK144 = X0 | in(sK136(X0,sK144),X0) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(X0,sK144),sK142,sK140,sK139)))) = sK151(sK136(X0,sK144),sK142,sK140,sK139), inference(resolution, [status(thm)], [c143,d34])).
% 67.86/16.85  cnf(d156, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK144 = sK143 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [d155,d11])).
% 67.86/16.85  cnf(d157, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [c157,d156])).
% 67.86/16.85  cnf(d158, plain, sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(superposition, [status(thm)], [d157,c154])).
% 67.86/16.85  cnf(d159, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d158,d30])).
% 67.86/16.85  cnf(d160, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d159,d137])).
% 67.86/16.85  cnf(d161, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d160,d30])).
% 67.86/16.85  cnf(d162, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | sK154(sK136(sK143,sK144),sK142,sK139,sK140) != X1 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d161,d137])).
% 67.86/16.85  cnf(d163, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(equality_resolution, [status(thm)], [d162])).
% 67.86/16.85  cnf(d164, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | ~in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d163,d94])).
% 67.86/16.85  cnf(d165, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d164,d52])).
% 67.86/16.85  cnf(d166, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK154(sK136(sK143,sK144),sK142,sK139,sK140),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d165,d52])).
% 67.86/16.85  cnf(d167, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK153(sK136(sK143,sK144),sK142,sK139,sK140) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d166,d52])).
% 67.86/16.85  cnf(d168, plain, 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d167])).
% 67.86/16.85  cnf(d169, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | sK142 != sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(demodulation, [status(thm)], [d168,d154])).
% 67.86/16.85  cnf(d170, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK153(sK136(sK143,sK144),sK142,sK139,sK140),sK139,sK140), inference(equality_resolution, [status(thm)], [d169])).
% 67.86/16.85  cnf(d171, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d170,c165])).
% 67.86/16.85  cnf(d172, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d171,c155])).
% 67.86/16.85  cnf(d173, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d172,d0])).
% 67.86/16.85  cnf(d174, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | in(sK136(sK143,sK144),sK144) | ~in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d173,d54])).
% 67.86/16.85  cnf(d175, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | in(sK136(sK143,sK144),sK144) | sK144 = sK143 | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d174,c143])).
% 67.86/16.85  cnf(d176, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d175])).
% 67.86/16.85  cnf(d177, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(resolution, [status(thm)], [d176,d34])).
% 67.86/16.85  cnf(d178, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(demodulation, [status(thm)], [d177,d30])).
% 67.86/16.85  cnf(d179, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK152(sK136(sK143,sK144),sK142,sK140,sK139)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(demodulation, [status(thm)], [d178,d137])).
% 67.86/16.85  cnf(d180, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(demodulation, [status(thm)], [d179,d30])).
% 67.86/16.85  cnf(d181, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(demodulation, [status(thm)], [d180,d137])).
% 67.86/16.85  cnf(d182, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(demodulation, [status(thm)], [d181,d94])).
% 67.86/16.85  cnf(d183, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) != sK151(sK136(sK143,sK144),sK142,sK140,sK139) | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(equality_factoring, [status(thm)], [d182])).
% 67.86/16.85  cnf(d184, plain, 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK151(sK136(sK143,sK144),sK142,sK140,sK139), inference(equality_resolution, [status(thm)], [d183])).
% 67.86/16.85  cnf(d185, plain, 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(superposition, [status(thm)], [d137,c154])).
% 67.86/16.85  cnf(d186, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d185,d137])).
% 67.86/16.85  cnf(d187, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d186,d94])).
% 67.86/16.85  cnf(d188, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | 'topstr$uclosure'(sK139,X0) != sK142 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d187,d184])).
% 67.86/16.85  cnf(d189, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | 'topstr$uclosure'(sK139,X0) != sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(superposition, [status(thm)], [d137,c156])).
% 67.86/16.85  cnf(d190, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d189,d137])).
% 67.86/16.85  cnf(d191, plain, 'topstr$uclosure'(sK139,X0) != sK142 | 'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) != X0 | sK136(sK143,sK144) != X1 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK143) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(demodulation, [status(thm)], [d190,d94])).
% 67.86/16.85  cnf(d192, plain, 'topstr$uclosure'(sK139,'relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))))) != sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'('relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))),sK139,sK140), inference(equality_resolution, [status(thm)], [d191])).
% 67.86/16.85  cnf(d193, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) != sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'('relation$urng'('the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))),sK139,sK140), inference(demodulation, [status(thm)], [d192,d184])).
% 67.86/16.85  cnf(d194, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) != sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(demodulation, [status(thm)], [d193,d184])).
% 67.86/16.85  cnf(d195, plain, sK142 != sK142 | sK136(sK143,sK144) != X0 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(demodulation, [status(thm)], [d194,d73])).
% 67.86/16.85  cnf(d196, plain, sK142 != sK142 | ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d195])).
% 67.86/16.85  cnf(d197, plain, ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d196])).
% 67.86/16.85  cnf(d198, plain, ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~'Ts137'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(resolution, [status(thm)], [d197,c159])).
% 67.86/16.85  cnf(d199, plain, ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d198,c153])).
% 67.86/16.85  cnf(d200, plain, ~element(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d199,d33])).
% 67.86/16.85  cnf(d201, plain, ~in(sK136(sK143,sK144),sK144) | in(sK136(sK143,sK144),sK143) | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d200,d32])).
% 67.86/16.85  cnf(d202, plain, in(sK136(sK143,sK144),sK143) | sK144 = sK143 | in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d201,c143])).
% 67.86/16.85  cnf(d203, plain, in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [c157,d202])).
% 67.86/16.85  cnf(d204, plain, element(sK136(sK143,sK144),'the$ucarrier'(sK140)), inference(resolution, [status(thm)], [d203,d54])).
% 67.86/16.85  cnf(d205, plain, 'topstr$uclosure'(sK139,X0) != sK142 | sK136(sK143,sK144) != X1 | sK151(sK136(sK143,sK144),sK142,sK140,sK139) != X0 | ~in(X1,'the$ucarrier'(sK140)) | in(X1,sK144) | ~'netstr$uinduced$usubset'(X0,sK139,sK140), inference(resolution, [status(thm)], [d204,d188])).
% 67.86/16.85  cnf(d206, plain, 'topstr$uclosure'(sK139,sK151(sK136(sK143,sK144),sK142,sK140,sK139)) != sK142 | sK136(sK143,sK144) != X0 | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK144) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d205])).
% 67.86/16.85  cnf(d207, plain, sK142 != sK142 | sK136(sK143,sK144) != X0 | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK144) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(demodulation, [status(thm)], [d206,d73])).
% 67.86/16.85  cnf(d208, plain, sK144 = sK143 | ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [d203,c144])).
% 67.86/16.85  cnf(d209, plain, ~in(sK136(sK143,sK144),sK144), inference(resolution, [status(thm)], [c157,d208])).
% 67.86/16.85  cnf(d210, plain, sK144 = sK143 | 'topstr$uclosure'(sK139,sK153(sK136(sK143,sK144),sK142,sK139,sK140)) = sK142, inference(resolution, [status(thm)], [d209,d138])).
% 67.86/16.85  cnf(d211, plain, sK142 = sK142 | sK144 = sK143, inference(demodulation, [status(thm)], [d210,d154])).
% 67.86/16.85  cnf(d212, plain, sK142 = sK142, inference(resolution, [status(thm)], [c157,d211])).
% 67.86/16.85  cnf(d213, plain, sK136(sK143,sK144) != X0 | ~in(X0,'the$ucarrier'(sK140)) | in(X0,sK144) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(resolution, [status(thm)], [d212,d207])).
% 67.86/16.85  cnf(d214, plain, ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | in(sK136(sK143,sK144),sK144) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(equality_resolution, [status(thm)], [d213])).
% 67.86/16.85  cnf(d215, plain, ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140), inference(resolution, [status(thm)], [d209,d214])).
% 67.86/16.85  cnf(d216, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) = 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))), inference(demodulation, [status(thm)], [d94,d184])).
% 67.86/16.85  cnf(d217, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(resolution, [status(thm)], [d203,d11])).
% 67.86/16.85  cnf(d218, plain, 'relation$urng$uas$usubset'('the$ucarrier'('subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(demodulation, [status(thm)], [d217,d52])).
% 67.86/16.85  cnf(d219, plain, 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK154(sK136(sK143,sK144),sK142,sK139,sK140)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(demodulation, [status(thm)], [d218,d137])).
% 67.86/16.85  cnf(d220, plain, 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'subnetstr$uof$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(demodulation, [status(thm)], [d219,d52])).
% 67.86/16.85  cnf(d221, plain, 'relation$urng$uas$usubset'('the$ucarrier'('netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144))),'the$ucarrier'(sK139),'the$umapping'(sK139,'netstr$urestr$uto$uelement'(sK139,sK140,sK136(sK143,sK144)))) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(demodulation, [status(thm)], [d220,d137])).
% 67.86/16.85  cnf(d222, plain, sK151(sK136(sK143,sK144),sK142,sK140,sK139) = sK153(sK136(sK143,sK144),sK142,sK139,sK140), inference(demodulation, [status(thm)], [d221,d216])).
% 67.86/16.85  cnf(d223, plain, 'netstr$uinduced$usubset'(sK151(sK136(sK143,sK144),sK142,sK140,sK139),sK139,sK140) | ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)), inference(superposition, [status(thm)], [d222,c165])).
% 67.86/16.85  cnf(d224, plain, ~'Ts138'(sK139,sK140,sK142,sK136(sK143,sK144)) | ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)), inference(resolution, [status(thm)], [d223,d215])).
% 67.86/16.85  cnf(d225, plain, ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)) | ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d224,c155])).
% 67.86/16.85  cnf(d226, plain, ~in(sK136(sK143,sK144),'the$ucarrier'(sK140)), inference(resolution, [status(thm)], [d203,d225])).
% 67.86/16.85  cnf(d227, plain, ~in(sK136(sK143,sK144),sK143), inference(resolution, [status(thm)], [d226,d0])).
% 67.86/16.85  cnf(d228, plain, $false, inference(resolution, [status(thm)], [d203,d227])).
% 67.86/16.85  % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------