%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:04:57 AM UTC 2026
% Result : Theorem 22.08s 13.40s
% Output : CNFRefutation 22.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR117+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/10.51 % Computer : n012.cluster.edu
% 0.05/10.51 % Model : x86_64 x86_64
% 0.05/10.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/10.51 % Memory : 8046.5625MB
% 0.05/10.51 % OS : Linux 6.8.0-71-generic
% 0.05/10.51 % CPULimit : 300
% 0.05/10.51 % WCLimit : 300
% 0.05/10.51 % DateTime : Sun Sep 27 01:16:03 UTC 2026
% 0.05/10.51 % CPUTime :
% 0.05/10.51 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.08/13.40 % SZS status Theorem for theBenchmark.p
% 22.08/13.40 % SZS output start CNFRefutation for theBenchmark.p
% 22.08/13.40 fof(kb_SUMO_MILO_701, axiom, ! [X0] : (('s$u$uRegion'(X0) => 's$u$uObject'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_6365, axiom, ! [X0] : (('s$u$uGeographicArea'(X0) => 's$u$uRegion'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_6345, axiom, ! [X0] : (('s$u$uGeopoliticalArea'(X0) => 's$u$uGeographicArea'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_6428, axiom, ! [X0] : (('s$u$uNation'(X0) => 's$u$uGeopoliticalArea'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_6437, axiom, ! [X0] : (('s$u$uCity'(X0) => 's$u$uGeopoliticalArea'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_Domains_9582, axiom, ! [X0] : (('s$u$uBodyOfWater'(X0) => 's$u$uWaterArea'(X0)))).
% 22.08/13.40 fof(kb_SUMO_MILO_Domains_9679, axiom, ! [X0] : (('s$u$uSea'(X0) => 's$u$uBodyOfWater'(X0)))).
% 22.08/13.40 fof(coastal_cities_near_water, axiom, ! [X0] : (('s$u$uCity'(X0) => ('is$uinstance'(X0,'s$u$uCoastalCitiesClass') => ? [X1] : (('s$u$uSea'(X1) & 's$u$uorientation'(X0,X1,'s$u$uNear'))))))).
% 22.08/13.40 fof(flood_near_water, axiom, ! [X0] : ! [X1] : ((('s$u$uWaterArea'(X0) & 's$u$uCity'(X1)) => ('s$u$uorientation'(X1,X0,'s$u$uNear') => 's$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1))))).
% 22.08/13.40 fof(int_type, axiom, ? [X0] : int(X0)).
% 22.08/13.40 fof(copenhagen_coastal, axiom, 'is$uinstance'('s$u$uCopenhagen','s$u$uCoastalCitiesClass')).
% 22.08/13.40 fof(s__Denmark_type, axiom, 's$u$uNation'('s$u$uDenmark')).
% 22.08/13.40 fof(s__Denmark_OECD, axiom, 'is$uinstance'('s$u$uDenmark','s$u$uOECDMemberEconomiesClass')).
% 22.08/13.40 fof(s__Copenhagen_type, axiom, 's$u$uCity'('s$u$uCopenhagen')).
% 22.08/13.40 fof(s__Copenhagen_s__Denmark, axiom, 'capital$ucity'('s$u$uCopenhagen','s$u$uDenmark')).
% 22.08/13.40 fof(copenhagen_lat_type, axiom, real('\'55.67631\'')).
% 22.08/13.40 fof(copenhagen_long_type, axiom, real('\'12.569355\'')).
% 22.08/13.40 fof(copenhagen_type, axiom, 's$u$uSymbolicString'(copenhagen)).
% 22.08/13.40 fof(dk_type, axiom, 's$u$uSymbolicString'(dk)).
% 22.08/13.40 fof(latlong_s__Copenhagen, axiom, latlong('s$u$uCopenhagen','\'55.67631\'','\'12.569355\'',copenhagen,dk)).
% 22.08/13.40 fof(moscow_lat_type, axiom, real('\'55.75695\'')).
% 22.08/13.40 fof(moscow_long_type, axiom, real('\'37.614975\'')).
% 22.08/13.40 fof(moscow_type, axiom, 's$u$uSymbolicString'(moscow)).
% 22.08/13.40 fof(ru_type, axiom, 's$u$uSymbolicString'(ru)).
% 22.08/13.40 fof(latlong_s__Moscow, axiom, latlong('s$u$uMoscow','\'55.75695\'','\'37.614975\'',moscow,ru)).
% 22.08/13.40 fof(s__Copenhagen_not_s__Moscow, axiom, 'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow')).
% 22.08/13.40 fof(55.67631_55, axiom, 'to$uint'('\'55.67631\'') = '\'55\'').
% 22.08/13.40 fof(55.75695_55, axiom, 'to$uint'('\'55.75695\'') = '\'55\'').
% 22.08/13.40 fof(where, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ? [X10] : (('s$u$uObject'(X0) & ('s$u$uObject'(X1) & (real(X2) & (real(X3) & ('s$u$uSymbolicString'(X4) & ('s$u$uSymbolicString'(X5) & (int(X6) & (real(X7) & (real(X8) & ('s$u$uSymbolicString'(X9) & ('s$u$uSymbolicString'(X10) & ('is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') & ('capital$ucity'(X0,X1) & ('look$udifferent'(X0,'s$u$uMoscow') & (latlong(X0,X2,X3,X4,X5) & (latlong('s$u$uMoscow',X7,X8,X9,X10) & ('to$uint'(X2) = 'to$uint'(X7) & 's$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0)))))))))))))))))))).
% 22.08/13.40 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ? [X10] : (('s$u$uObject'(X0) & ('s$u$uObject'(X1) & (real(X2) & (real(X3) & ('s$u$uSymbolicString'(X4) & ('s$u$uSymbolicString'(X5) & (int(X6) & (real(X7) & (real(X8) & ('s$u$uSymbolicString'(X9) & ('s$u$uSymbolicString'(X10) & ('is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') & ('capital$ucity'(X0,X1) & ('look$udifferent'(X0,'s$u$uMoscow') & (latlong(X0,X2,X3,X4,X5) & (latlong('s$u$uMoscow',X7,X8,X9,X10) & ('to$uint'(X2) = 'to$uint'(X7) & 's$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0))))))))))))))))))), inference(negate_conjecture, [status(cth)], [where])).
% 22.08/13.40 cnf(c14, plain, ~'s$u$uRegion'(X0) | 's$u$uObject'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_701])).
% 22.08/13.40 cnf(c15, plain, ~'s$u$uGeographicArea'(X0) | 's$u$uRegion'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_6365])).
% 22.08/13.40 cnf(c16, plain, ~'s$u$uGeopoliticalArea'(X0) | 's$u$uGeographicArea'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_6345])).
% 22.08/13.40 cnf(c17, plain, ~'s$u$uNation'(X0) | 's$u$uGeopoliticalArea'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_6428])).
% 22.08/13.40 cnf(c18, plain, ~'s$u$uCity'(X0) | 's$u$uGeopoliticalArea'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_6437])).
% 22.08/13.40 cnf(c20, plain, ~'s$u$uBodyOfWater'(X0) | 's$u$uWaterArea'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_Domains_9582])).
% 22.08/13.40 cnf(c21, plain, ~'s$u$uSea'(X0) | 's$u$uBodyOfWater'(X0), inference(clausification, [status(esa)], [kb_SUMO_MILO_Domains_9679])).
% 22.08/13.40 cnf(c26, plain, ~'s$u$uCity'(X0) | ~'is$uinstance'(X0,'s$u$uCoastalCitiesClass') | 's$u$uSea'(sK24(X0)), inference(clausification, [status(esa)], [coastal_cities_near_water])).
% 22.08/13.40 cnf(c27, plain, ~'s$u$uCity'(X0) | ~'is$uinstance'(X0,'s$u$uCoastalCitiesClass') | 's$u$uorientation'(X0,sK24(X0),'s$u$uNear'), inference(clausification, [status(esa)], [coastal_cities_near_water])).
% 22.08/13.40 cnf(c28, plain, ~'s$u$uWaterArea'(X0) | ~'s$u$uCity'(X1) | ~'s$u$uorientation'(X1,X0,'s$u$uNear') | 's$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1), inference(clausification, [status(esa)], [flood_near_water])).
% 22.08/13.40 cnf(c30, plain, int(sK28), inference(clausification, [status(esa)], [int_type])).
% 22.08/13.40 cnf(c33, plain, 'is$uinstance'('s$u$uCopenhagen','s$u$uCoastalCitiesClass'), inference(clausification, [status(esa)], [copenhagen_coastal])).
% 22.08/13.40 cnf(c38, plain, 's$u$uNation'('s$u$uDenmark'), inference(clausification, [status(esa)], [s__Denmark_type])).
% 22.08/13.40 cnf(c39, plain, 'is$uinstance'('s$u$uDenmark','s$u$uOECDMemberEconomiesClass'), inference(clausification, [status(esa)], [s__Denmark_OECD])).
% 22.08/13.40 cnf(c100, plain, 's$u$uCity'('s$u$uCopenhagen'), inference(clausification, [status(esa)], [s__Copenhagen_type])).
% 22.08/13.40 cnf(c101, plain, 'capital$ucity'('s$u$uCopenhagen','s$u$uDenmark'), inference(clausification, [status(esa)], [s__Copenhagen_s__Denmark])).
% 22.08/13.40 cnf(c148, plain, real('\'55.67631\''), inference(clausification, [status(esa)], [copenhagen_lat_type])).
% 22.08/13.40 cnf(c149, plain, real('\'12.569355\''), inference(clausification, [status(esa)], [copenhagen_long_type])).
% 22.08/13.40 cnf(c150, plain, 's$u$uSymbolicString'(copenhagen), inference(clausification, [status(esa)], [copenhagen_type])).
% 22.08/13.40 cnf(c151, plain, 's$u$uSymbolicString'(dk), inference(clausification, [status(esa)], [dk_type])).
% 22.08/13.40 cnf(c152, plain, latlong('s$u$uCopenhagen','\'55.67631\'','\'12.569355\'',copenhagen,dk), inference(clausification, [status(esa)], [latlong_s__Copenhagen])).
% 22.08/13.40 cnf(c168, plain, real('\'55.75695\''), inference(clausification, [status(esa)], [moscow_lat_type])).
% 22.08/13.40 cnf(c169, plain, real('\'37.614975\''), inference(clausification, [status(esa)], [moscow_long_type])).
% 22.08/13.40 cnf(c170, plain, 's$u$uSymbolicString'(moscow), inference(clausification, [status(esa)], [moscow_type])).
% 22.08/13.40 cnf(c171, plain, 's$u$uSymbolicString'(ru), inference(clausification, [status(esa)], [ru_type])).
% 22.08/13.40 cnf(c172, plain, latlong('s$u$uMoscow','\'55.75695\'','\'37.614975\'',moscow,ru), inference(clausification, [status(esa)], [latlong_s__Moscow])).
% 22.08/13.40 cnf(c204, plain, 'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow'), inference(clausification, [status(esa)], [s__Copenhagen_not_s__Moscow])).
% 22.08/13.40 cnf(c235, plain, 'to$uint'('\'55.67631\'') = '\'55\'', inference(clausification, [status(esa)], [55.67631_55])).
% 22.08/13.40 cnf(c236, plain, 'to$uint'('\'55.75695\'') = '\'55\'', inference(clausification, [status(esa)], [55.75695_55])).
% 22.08/13.40 cnf(c269, plain, ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0) | ~real(X1) | 'to$uint'(X2) != 'to$uint'(X1) | ~latlong(X0,X2,X3,X4,X5) | ~real(X6) | ~int(X7) | ~'capital$ucity'(X0,X8) | ~'s$u$uSymbolicString'(X5) | ~'s$u$uSymbolicString'(X9) | ~'s$u$uObject'(X8) | ~'is$uinstance'(X8,'s$u$uOECDMemberEconomiesClass') | ~real(X3) | ~'s$u$uSymbolicString'(X4) | ~real(X2) | ~'look$udifferent'(X0,'s$u$uMoscow') | ~latlong('s$u$uMoscow',X1,X6,X9,X10) | ~'s$u$uObject'(X0) | ~'s$u$uSymbolicString'(X10), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.08/13.40 cnf(d0, plain, ~'s$u$uCity'(X0) | ~'s$u$uWaterArea'(sK24(X0)) | 's$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0) | ~'s$u$uCity'(X0) | ~'is$uinstance'(X0,'s$u$uCoastalCitiesClass'), inference(resolution, [status(thm)], [c28,c27])).
% 22.08/13.40 cnf(d1, plain, '\'55\'' != 'to$uint'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uObject'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(X4) | ~'s$u$uSymbolicString'(X5) | ~'s$u$uSymbolicString'(X6) | ~'is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X2) | ~real(X7) | ~real('\'55.67631\'') | ~real(X8) | ~real(X0) | ~int(X9) | ~'capital$ucity'(X2,X1) | ~latlong(X2,'\'55.67631\'',X7,X4,X3) | ~latlong('s$u$uMoscow',X0,X8,X6,X5) | ~'look$udifferent'(X2,'s$u$uMoscow'), inference(superposition, [status(thm)], [c235,c269])).
% 22.08/13.40 cnf(d2, plain, '\'55\'' != 'to$uint'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uObject'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(X4) | ~'s$u$uSymbolicString'(X5) | ~'s$u$uSymbolicString'(X6) | ~'is$uinstance'(X2,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1) | ~real(X7) | ~real(X8) | ~real(X0) | ~int(X9) | ~'capital$ucity'(X1,X2) | ~latlong(X1,'\'55.67631\'',X8,X5,X6) | ~latlong('s$u$uMoscow',X0,X7,X3,X4) | ~'look$udifferent'(X1,'s$u$uMoscow'), inference(resolution, [status(thm)], [c148,d1])).
% 22.08/13.40 cnf(d3, plain, '\'55\'' != '\'55\'' | ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(X4) | ~'s$u$uSymbolicString'(X5) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1) | ~real(X6) | ~real(X7) | ~real('\'55.75695\'') | ~int(X8) | ~'capital$ucity'(X1,X0) | ~latlong(X1,'\'55.67631\'',X6,X3,X2) | ~latlong('s$u$uMoscow','\'55.75695\'',X7,X5,X4) | ~'look$udifferent'(X1,'s$u$uMoscow'), inference(superposition, [status(thm)], [c236,d2])).
% 22.08/13.40 cnf(d4, plain, '\'55\'' != '\'55\'' | ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(X4) | ~'s$u$uSymbolicString'(X5) | ~'is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0) | ~real(X6) | ~real(X7) | ~int(X8) | ~'capital$ucity'(X0,X1) | ~latlong(X0,'\'55.67631\'',X7,X4,X5) | ~latlong('s$u$uMoscow','\'55.75695\'',X6,X2,X3) | ~'look$udifferent'(X0,'s$u$uMoscow'), inference(resolution, [status(thm)], [c168,d3])).
% 22.08/13.40 cnf(d5, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(X4) | ~'s$u$uSymbolicString'(X5) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1) | ~real(X6) | ~real(X7) | ~int(X8) | ~'capital$ucity'(X1,X0) | ~latlong(X1,'\'55.67631\'',X6,X3,X2) | ~latlong('s$u$uMoscow','\'55.75695\'',X7,X5,X4) | ~'look$udifferent'(X1,'s$u$uMoscow'), inference(equality_resolution, [status(thm)], [d4])).
% 22.08/13.40 cnf(d6, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(moscow) | ~'s$u$uSymbolicString'(ru) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0) | ~real('\'37.614975\'') | ~real(X4) | ~int(X5) | ~'capital$ucity'(X0,X1) | ~latlong(X0,'\'55.67631\'',X4,X2,X3) | ~'look$udifferent'(X0,'s$u$uMoscow'), inference(resolution, [status(thm)], [d5,c172])).
% 22.08/13.40 cnf(d7, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(moscow) | ~'s$u$uSymbolicString'(ru) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1) | ~real(X4) | ~int(X5) | ~'capital$ucity'(X1,X0) | ~latlong(X1,'\'55.67631\'',X4,X3,X2) | ~'look$udifferent'(X1,'s$u$uMoscow'), inference(resolution, [status(thm)], [c169,d6])).
% 22.08/13.40 cnf(d8, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'s$u$uSymbolicString'(ru) | ~'is$uinstance'(X1,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X0) | ~real(X4) | ~int(X5) | ~'capital$ucity'(X0,X1) | ~latlong(X0,'\'55.67631\'',X4,X2,X3) | ~'look$udifferent'(X0,'s$u$uMoscow'), inference(resolution, [status(thm)], [c170,d7])).
% 22.08/13.40 cnf(d9, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'(X1) | ~'s$u$uSymbolicString'(X2) | ~'s$u$uSymbolicString'(X3) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um',X1) | ~real(X4) | ~int(X5) | ~'capital$ucity'(X1,X0) | ~latlong(X1,'\'55.67631\'',X4,X3,X2) | ~'look$udifferent'(X1,'s$u$uMoscow'), inference(resolution, [status(thm)], [c171,d8])).
% 22.08/13.40 cnf(d10, plain, ~'s$u$uObject'('s$u$uCopenhagen') | ~'s$u$uObject'(X0) | ~'s$u$uSymbolicString'(copenhagen) | ~'s$u$uSymbolicString'(dk) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~real('\'12.569355\'') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0) | ~'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow'), inference(resolution, [status(thm)], [d9,c152])).
% 22.08/13.40 cnf(d11, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'('s$u$uCopenhagen') | ~'s$u$uSymbolicString'(copenhagen) | ~'s$u$uSymbolicString'(dk) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0) | ~'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow'), inference(resolution, [status(thm)], [c149,d10])).
% 22.08/13.40 cnf(d12, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'('s$u$uCopenhagen') | ~'s$u$uSymbolicString'(dk) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0) | ~'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow'), inference(resolution, [status(thm)], [c150,d11])).
% 22.08/13.40 cnf(d13, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'('s$u$uCopenhagen') | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0) | ~'look$udifferent'('s$u$uCopenhagen','s$u$uMoscow'), inference(resolution, [status(thm)], [c151,d12])).
% 22.08/13.40 cnf(d14, plain, ~'s$u$uObject'(X0) | ~'s$u$uObject'('s$u$uCopenhagen') | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0), inference(resolution, [status(thm)], [c204,d13])).
% 22.08/13.40 cnf(d15, plain, 's$u$uGeopoliticalArea'('s$u$uCopenhagen'), inference(resolution, [status(thm)], [c100,c18])).
% 22.08/13.40 cnf(d16, plain, 's$u$uGeographicArea'('s$u$uCopenhagen'), inference(resolution, [status(thm)], [d15,c16])).
% 22.08/13.40 cnf(d17, plain, 's$u$uRegion'('s$u$uCopenhagen'), inference(resolution, [status(thm)], [d16,c15])).
% 22.08/13.40 cnf(d18, plain, 's$u$uObject'('s$u$uCopenhagen'), inference(resolution, [status(thm)], [d17,c14])).
% 22.08/13.40 cnf(d19, plain, ~'s$u$uObject'(X0) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~'s$u$ucapability'('s$u$uFlooding$u$ut','s$u$ulocated$u$um','s$u$uCopenhagen') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0), inference(resolution, [status(thm)], [d18,d14])).
% 22.08/13.40 cnf(d20, plain, ~'s$u$uObject'(X0) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0) | ~'s$u$uCity'('s$u$uCopenhagen') | ~'s$u$uWaterArea'(sK24('s$u$uCopenhagen')) | ~'is$uinstance'('s$u$uCopenhagen','s$u$uCoastalCitiesClass'), inference(resolution, [status(thm)], [d19,d0])).
% 22.08/13.40 cnf(d21, plain, ~'s$u$uObject'(X0) | ~'s$u$uCity'('s$u$uCopenhagen') | ~'s$u$uWaterArea'(sK24('s$u$uCopenhagen')) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0), inference(resolution, [status(thm)], [c33,d20])).
% 22.08/13.40 cnf(d22, plain, ~'s$u$uObject'(X0) | ~'s$u$uWaterArea'(sK24('s$u$uCopenhagen')) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0), inference(resolution, [status(thm)], [c100,d21])).
% 22.08/13.40 cnf(d23, plain, ~'s$u$uCity'('s$u$uCopenhagen') | 's$u$uSea'(sK24('s$u$uCopenhagen')), inference(resolution, [status(thm)], [c33,c26])).
% 22.08/13.40 cnf(d24, plain, 's$u$uSea'(sK24('s$u$uCopenhagen')), inference(resolution, [status(thm)], [c100,d23])).
% 22.08/13.40 cnf(d25, plain, 's$u$uBodyOfWater'(sK24('s$u$uCopenhagen')), inference(resolution, [status(thm)], [d24,c21])).
% 22.08/13.40 cnf(d26, plain, 's$u$uWaterArea'(sK24('s$u$uCopenhagen')), inference(resolution, [status(thm)], [d25,c20])).
% 22.08/13.40 cnf(d27, plain, ~'s$u$uObject'(X0) | ~'is$uinstance'(X0,'s$u$uOECDMemberEconomiesClass') | ~int(X1) | ~'capital$ucity'('s$u$uCopenhagen',X0), inference(resolution, [status(thm)], [d26,d22])).
% 22.08/13.40 cnf(d28, plain, ~'s$u$uObject'('s$u$uDenmark') | ~'is$uinstance'('s$u$uDenmark','s$u$uOECDMemberEconomiesClass') | ~int(X0), inference(resolution, [status(thm)], [d27,c101])).
% 22.08/13.40 cnf(d29, plain, ~'s$u$uObject'('s$u$uDenmark') | ~int(X0), inference(resolution, [status(thm)], [c39,d28])).
% 22.08/13.40 cnf(d30, plain, 's$u$uGeopoliticalArea'('s$u$uDenmark'), inference(resolution, [status(thm)], [c38,c17])).
% 22.08/13.40 cnf(d31, plain, 's$u$uGeographicArea'('s$u$uDenmark'), inference(resolution, [status(thm)], [d30,c16])).
% 22.08/13.40 cnf(d32, plain, 's$u$uRegion'('s$u$uDenmark'), inference(resolution, [status(thm)], [d31,c15])).
% 22.08/13.40 cnf(d33, plain, 's$u$uObject'('s$u$uDenmark'), inference(resolution, [status(thm)], [d32,c14])).
% 22.08/13.40 cnf(d34, plain, ~int(X0), inference(resolution, [status(thm)], [d33,d29])).
% 22.08/13.40 cnf(d35, plain, $false, inference(resolution, [status(thm)], [d34,c30])).
% 22.08/13.40 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------