%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV679+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:49:03 AM UTC 2026
% Result : Theorem 68.68s 14.08s
% Output : CNFRefutation 68.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV679+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n002.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 11:40:20 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 68.68/14.08 % SZS status Theorem for theBenchmark.p
% 68.68/14.08 % SZS output start CNFRefutation for theBenchmark.p
% 68.68/14.08 fof(PLF.References.STLCRef.preservation, axiom, ! [X0] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) => ! [X1] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) => ! [X2] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X2) => ! [X3] : (('cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X3) => ! [X4] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X4) => ! [X5] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X5) => ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,X1,X3) => ('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,X4) => ('cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X4),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X2,X5)) => ? [X6] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X6) & ('cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(X6,X0) & ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X6,X2,X3) & 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X6,X5))))))))))))))))))))).
% 68.68/14.08 fof(_HAMMER_GOAL, conjecture, ! [X0] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) => ! [X1] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) => ! [X2] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X2) => ! [X3] : (('cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X3) => ! [X4] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X4) => ! [X5] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X5) => ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,X1,X3) => ('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,X4) => ('cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X4),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X2,X5)) => ? [X6] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X6) & ('cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(X6,X0) & ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X6,X2,X3) & 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X6,X5))))))))))))))))))))).
% 68.68/14.08 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) => ! [X1] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) => ! [X2] : (('cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X2) => ! [X3] : (('cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X3) => ! [X4] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X4) => ! [X5] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X5) => ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,X1,X3) => ('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,X4) => ('cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X4),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X2,X5)) => ? [X6] : (('cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X6) & ('cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(X6,X0) & ('cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X6,X2,X3) & 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X6,X5)))))))))))))))))))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 68.68/14.08 cnf(c259, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X2,X1,X3,X0)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X2) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X4,X5),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X0)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X2,X4,X3) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X3) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X4) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X2,X5), inference(clausification, [status(esa)], [PLF.References.STLCRef.preservation])).
% 68.68/14.08 cnf(c260, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X2) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X3,X4),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X0)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X2,X3,X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X4) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X2,X1,X5,X0),X2) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X3) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X2,X4), inference(clausification, [status(esa)], [PLF.References.STLCRef.preservation])).
% 68.68/14.08 cnf(c261, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X2) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X3,X4),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X0)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X2,X3,X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X5) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X2,X1,X5,X0),X1,X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X4) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X3) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X2,X4), inference(clausification, [status(esa)], [PLF.References.STLCRef.preservation])).
% 68.68/14.08 cnf(c262, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X2,X3),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',X1,X0)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X4,X2,X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X5) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(X3) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X4) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X4,X1,X5,X0),X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(X2) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X4,X3), inference(clausification, [status(esa)], [PLF.References.STLCRef.preservation])).
% 68.68/14.08 cnf(c283, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK401), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c284, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK402), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c285, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c286, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c287, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c288, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c289, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c290, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c291, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estep$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',sK402,sK405),'cCoq$u2eInit$u2eDatatypes$u2epair$u$u$u24a4'('cPLF$u2eReferences$u2eSTLCRef$u2etm','cPLF$u2eReferences$u2eSTLCRef$u2estore',sK403,sK406)), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(c292, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(X0,sK401) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK403,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK406), inference(clausification, [status(esa)], [negated_conjecture])).
% 68.68/14.08 cnf(d0, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK402) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,X1,sK406),X0), inference(resolution, [status(thm)], [c260,c291])).
% 68.68/14.08 cnf(d1, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,X1,sK406),X0), inference(resolution, [status(thm)], [c284,d0])).
% 68.68/14.08 cnf(d2, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,X1,sK406),X0), inference(resolution, [status(thm)], [c285,d1])).
% 68.68/14.08 cnf(d3, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,X1,sK406),X0), inference(resolution, [status(thm)], [c287,d2])).
% 68.68/14.08 cnf(d4, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,X1,sK406),X0), inference(resolution, [status(thm)], [c288,d3])).
% 68.68/14.09 cnf(d5, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X0,sK403,X1,sK406),sK403,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK402) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c261,c291])).
% 68.68/14.09 cnf(d6, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X0,sK403,X1,sK406),sK403,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c284,d5])).
% 68.68/14.09 cnf(d7, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X0,sK403,X1,sK406),sK403,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c285,d6])).
% 68.68/14.09 cnf(d8, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X0,sK403,X1,sK406),sK403,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c287,d7])).
% 68.68/14.09 cnf(d9, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | 'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK367(X0,sK403,X1,sK406),sK403,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c288,d8])).
% 68.68/14.09 cnf(d10, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,sK404,sK406),sK401), inference(resolution, [status(thm)], [d9,c292])).
% 68.68/14.09 cnf(d11, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2eextends$u$u$u24a2'(sK367(X0,sK403,sK404,sK406),sK401), inference(resolution, [status(thm)], [c286,d10])).
% 68.68/14.09 cnf(d12, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK401) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK401) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [d11,d4])).
% 68.68/14.09 cnf(d13, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [c283,d12])).
% 68.68/14.09 cnf(d14, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404), inference(resolution, [status(thm)], [c286,d13])).
% 68.68/14.09 cnf(d15, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404), inference(resolution, [status(thm)], [c290,d14])).
% 68.68/14.09 cnf(d16, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406), inference(resolution, [status(thm)], [c289,d15])).
% 68.68/14.09 cnf(d17, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,X1,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK402) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c259,c291])).
% 68.68/14.09 cnf(d18, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,X1,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c284,d17])).
% 68.68/14.09 cnf(d19, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,X1,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c285,d18])).
% 68.68/14.09 cnf(d20, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,X1,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c287,d19])).
% 68.68/14.09 cnf(d21, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(X0,sK403,X1,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c288,d20])).
% 68.68/14.09 cnf(d22, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK401) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [d21,c289])).
% 68.68/14.09 cnf(d23, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [c283,d22])).
% 68.68/14.09 cnf(d24, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405), inference(resolution, [status(thm)], [c286,d23])).
% 68.68/14.09 cnf(d25, plain, 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK367(sK401,sK403,sK404,sK406)), inference(resolution, [status(thm)], [c290,d24])).
% 68.68/14.09 cnf(d26, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(sK401,sK403,sK404,sK406),sK406), inference(resolution, [status(thm)], [d25,d16])).
% 68.68/14.09 cnf(d27, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,X1,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK402) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c262,c291])).
% 68.68/14.09 cnf(d28, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,X1,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2etm$u$u$u24t'(sK403) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c284,d27])).
% 68.68/14.09 cnf(d29, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,X1,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c285,d28])).
% 68.68/14.09 cnf(d30, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$u$u24t'(sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,X1,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c287,d29])).
% 68.68/14.09 cnf(d31, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(X0) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(X0,sK405) | 'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK367(X0,sK403,X1,sK406),sK406) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),X0,sK402,X1) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(X1), inference(resolution, [status(thm)], [c288,d30])).
% 68.68/14.09 cnf(d32, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uty$u$u$u24t'(sK401) | ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [d31,d26])).
% 68.68/14.09 cnf(d33, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ety$u$u$u24t'(sK404), inference(resolution, [status(thm)], [c283,d32])).
% 68.68/14.09 cnf(d34, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2estore$u$uwell$u$utyped$u$u$u24a2'(sK401,sK405) | ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404), inference(resolution, [status(thm)], [c286,d33])).
% 68.68/14.09 cnf(d35, plain, ~'cPLF$u2eReferences$u2eSTLCRef$u2ehas$u$utype$u$u$u24a4'('cPLF$u2eMaps$u2eempty$u$u$u24a1'('cPLF$u2eReferences$u2eSTLCRef$u2ety'),sK401,sK402,sK404), inference(resolution, [status(thm)], [c290,d34])).
% 68.68/14.09 cnf(d36, plain, $false, inference(resolution, [status(thm)], [c289,d35])).
% 68.68/14.09 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------