%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP230+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:48:41 PM UTC 2025
% Result : CounterSatisfiable 34.73s 19.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP230+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n013.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 09:35:47 EDT 2025
% 0.14/0.35 % CPUTime :
% 34.73/19.18
% 34.73/19.18 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.73/19.18
% 34.73/19.18 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.73/19.19 %$ be > theme > of > agent > vincent_forename > think_believe_consider > state > smoke > proposition > present > man > jules_forename > forename > event > accessible_world > actual_world > #nlpp > #skF_33 > #skF_20 > #skF_18 > #skF_11 > #skF_25 > #skF_31 > #skF_19 > #skF_7 > #skF_10 > #skF_16 > #skF_17 > #skF_15 > #skF_26 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_9 > #skF_32 > #skF_8 > #skF_30 > #skF_4 > #skF_22 > #skF_29 > #skF_28 > #skF_24 > #skF_27 > #skF_23 > #skF_12
% 34.73/19.19
% 34.73/19.19 %Foreground sorts:
% 34.73/19.19
% 34.73/19.19
% 34.73/19.19 %Background operators:
% 34.73/19.19
% 34.73/19.19
% 34.73/19.19 %Foreground operators:
% 34.73/19.19 tff(forename, type, forename: ($i * $i) > $o).
% 34.73/19.19 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 34.73/19.19 tff(theme, type, theme: ($i * $i * $i) > $o).
% 34.73/19.19 tff('#skF_33', type, '#skF_33': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 34.73/19.19 tff('#skF_20', type, '#skF_20': $i).
% 34.73/19.19 tff(present, type, present: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_18', type, '#skF_18': $i).
% 34.73/19.19 tff('#skF_11', type, '#skF_11': $i).
% 34.73/19.19 tff('#skF_25', type, '#skF_25': $i).
% 34.73/19.19 tff('#skF_31', type, '#skF_31': $i > $i).
% 34.73/19.19 tff(proposition, type, proposition: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_19', type, '#skF_19': $i).
% 34.73/19.19 tff(of, type, of: ($i * $i * $i) > $o).
% 34.73/19.19 tff('#skF_7', type, '#skF_7': $i).
% 34.73/19.19 tff(actual_world, type, actual_world: $i > $o).
% 34.73/19.19 tff(agent, type, agent: ($i * $i * $i) > $o).
% 34.73/19.19 tff('#skF_10', type, '#skF_10': $i).
% 34.73/19.19 tff('#skF_16', type, '#skF_16': $i).
% 34.73/19.19 tff('#skF_17', type, '#skF_17': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 34.73/19.19 tff('#skF_15', type, '#skF_15': $i > $i).
% 34.73/19.19 tff('#skF_26', type, '#skF_26': $i).
% 34.73/19.19 tff('#skF_14', type, '#skF_14': $i).
% 34.73/19.19 tff('#skF_5', type, '#skF_5': $i).
% 34.73/19.19 tff(jules_forename, type, jules_forename: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_6', type, '#skF_6': $i).
% 34.73/19.19 tff(smoke, type, smoke: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_13', type, '#skF_13': $i).
% 34.73/19.19 tff('#skF_2', type, '#skF_2': $i).
% 34.73/19.19 tff('#skF_3', type, '#skF_3': $i).
% 34.73/19.19 tff(event, type, event: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_1', type, '#skF_1': $i).
% 34.73/19.19 tff('#skF_21', type, '#skF_21': $i).
% 34.73/19.19 tff('#skF_9', type, '#skF_9': $i).
% 34.73/19.19 tff('#skF_32', type, '#skF_32': $i).
% 34.73/19.19 tff(state, type, state: ($i * $i) > $o).
% 34.73/19.19 tff(think_believe_consider, type, think_believe_consider: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_8', type, '#skF_8': $i).
% 34.73/19.19 tff('#skF_30', type, '#skF_30': $i).
% 34.73/19.19 tff(man, type, man: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_4', type, '#skF_4': $i).
% 34.73/19.19 tff(vincent_forename, type, vincent_forename: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_22', type, '#skF_22': $i).
% 34.73/19.19 tff('#skF_29', type, '#skF_29': $i).
% 34.73/19.19 tff('#skF_28', type, '#skF_28': $i).
% 34.73/19.19 tff('#skF_24', type, '#skF_24': $i).
% 34.73/19.19 tff('#skF_27', type, '#skF_27': $i).
% 34.73/19.19 tff('#skF_23', type, '#skF_23': $i).
% 34.73/19.19 tff(accessible_world, type, accessible_world: ($i * $i) > $o).
% 34.73/19.19 tff('#skF_12', type, '#skF_12': $i).
% 34.73/19.19
% 34.73/19.19 %Saturated clause set:
% 34.73/19.19 tff(c_30134, plain, (~man('#skF_9', '#skF_11'))).
% 34.73/19.19 tff(c_30133, plain, (~man('#skF_9', '#skF_2'))).
% 34.73/19.19 tff(c_30132, plain, (~man('#skF_9', '#skF_6'))).
% 34.73/19.19 tff(c_30110, plain, (![X15_24116, X9_24118, X13_24119]: (~forename('#skF_1', X15_24116) | ~vincent_forename('#skF_1', X15_24116) | ~agent('#skF_1', '#skF_8', X9_24118) | ~man('#skF_1', X9_24118) | ~of('#skF_1', X15_24116, X9_24118) | ~forename('#skF_1', X13_24119) | ~jules_forename('#skF_1', X13_24119) | ~of('#skF_1', X13_24119, X9_24118) | ~man('#skF_9', X9_24118)))).
% 34.73/19.19 tff(c_30104, plain, (![X15_24112, X23_24114, X9_26, X13_24115]: (~forename('#skF_1', X15_24112) | ~vincent_forename('#skF_1', X15_24112) | ~think_believe_consider('#skF_1', X23_24114) | ~present('#skF_1', X23_24114) | ~event('#skF_1', X23_24114) | ~theme('#skF_1', X23_24114, '#skF_9') | ~agent('#skF_1', X23_24114, X9_26) | ~man('#skF_1', X9_26) | ~of('#skF_1', X15_24112, X9_26) | ~forename('#skF_1', X13_24115) | ~jules_forename('#skF_1', X13_24115) | ~of('#skF_1', X13_24115, X9_26) | ~man('#skF_9', X9_26)))).
% 34.73/19.19 tff(c_30080, plain, (![X16_24090, X21_24087, X12_24092, X22_24089, X9_26, X18_24083, X15_24086, X13_24085, X23_24088, X17_24084, X20_24091]: (~event('#skF_9', '#skF_15'(X9_26)) | ~think_believe_consider(X12_24092, X23_24088) | ~present(X12_24092, X23_24088) | ~event(X12_24092, X23_24088) | ~theme(X12_24092, X23_24088, '#skF_9') | ~agent(X12_24092, X23_24088, X9_26) | ~be(X12_24092, X22_24089, X21_24087, X21_24087) | ~state(X12_24092, X22_24089) | ~forename(X12_24092, X20_24091) | ~jules_forename(X12_24092, X20_24091) | ~man(X12_24092, X21_24087) | ~of(X12_24092, X20_24091, X21_24087) | ~accessible_world(X12_24092, '#skF_9') | ~think_believe_consider(X12_24092, X18_24083) | ~present(X12_24092, X18_24083) | ~event(X12_24092, X18_24083) | ~theme(X12_24092, X18_24083, '#skF_9') | ~agent(X12_24092, X18_24083, X16_24090) | ~proposition(X12_24092, '#skF_9') | ~forename(X12_24092, X17_24084) | ~vincent_forename(X12_24092, X17_24084) | ~man(X12_24092, X16_24090) | ~of(X12_24092, X17_24084, X16_24090) | ~forename(X12_24092, X15_24086) | ~vincent_forename(X12_24092, X15_24086) | ~man(X12_24092, X9_26) | ~of(X12_24092, X15_24086, X9_26) | ~forename(X12_24092, X13_24085) | ~jules_forename(X12_24092, X13_24085) | ~of(X12_24092, X13_24085, X9_26) | ~actual_world(X12_24092) | ~man('#skF_9', '#skF_17'('#skF_9', X13_24085, X12_24092, X9_26, X16_24090, X21_24087, X22_24089, X20_24091, '#skF_9', X15_24086, X18_24083, X17_24084, X23_24088)) | ~man('#skF_9', X9_26)))).
% 34.73/19.19 tff(c_30072, plain, (~vincent_forename('#skF_1', '#skF_5'))).
% 34.73/19.19 tff(c_30065, plain, (![X15_23921]: (~forename('#skF_1', X15_23921) | ~vincent_forename('#skF_1', X15_23921) | ~of('#skF_1', X15_23921, '#skF_4')))).
% 34.73/19.19 tff(c_30012, plain, (![X16_24036, X20_24040, X13_24033, X21_24039, X12_24032, X23_24034, X18_24029, X17_24038, X22_24037, X15_24031]: (~accessible_world(X12_24032, '#skF_14') | ~think_believe_consider(X12_24032, X23_24034) | ~present(X12_24032, X23_24034) | ~event(X12_24032, X23_24034) | ~theme(X12_24032, X23_24034, '#skF_14') | ~agent(X12_24032, X23_24034, '#skF_4') | ~proposition(X12_24032, '#skF_14') | ~be(X12_24032, X22_24037, X21_24039, X21_24039) | ~state(X12_24032, X22_24037) | ~forename(X12_24032, X20_24040) | ~jules_forename(X12_24032, X20_24040) | ~man(X12_24032, X21_24039) | ~of(X12_24032, X20_24040, X21_24039) | ~accessible_world(X12_24032, '#skF_9') | ~think_believe_consider(X12_24032, X18_24029) | ~present(X12_24032, X18_24029) | ~event(X12_24032, X18_24029) | ~theme(X12_24032, X18_24029, '#skF_9') | ~agent(X12_24032, X18_24029, X16_24036) | ~proposition(X12_24032, '#skF_9') | ~forename(X12_24032, X17_24038) | ~vincent_forename(X12_24032, X17_24038) | ~man(X12_24032, X16_24036) | ~of(X12_24032, X17_24038, X16_24036) | ~forename(X12_24032, X15_24031) | ~vincent_forename(X12_24032, X15_24031) | ~man(X12_24032, '#skF_4') | ~of(X12_24032, X15_24031, '#skF_4') | ~forename(X12_24032, X13_24033) | ~jules_forename(X12_24032, X13_24033) | ~of(X12_24032, X13_24033, '#skF_4') | ~actual_world(X12_24032) | ~man('#skF_9', '#skF_17'('#skF_14', X13_24033, X12_24032, '#skF_4', X16_24036, X21_24039, X22_24037, X20_24040, '#skF_9', X15_24031, X18_24029, X17_24038, X23_24034))))).
% 34.73/19.19 tff(c_30021, plain, (![X16_24036, X20_24040, X13_24033, X21_24039, X12_24032, X23_24034, X18_24029, X17_24038, X22_24037, X15_24031]: (~accessible_world(X12_24032, '#skF_30') | ~think_believe_consider(X12_24032, X23_24034) | ~present(X12_24032, X23_24034) | ~event(X12_24032, X23_24034) | ~theme(X12_24032, X23_24034, '#skF_30') | ~agent(X12_24032, X23_24034, '#skF_20') | ~proposition(X12_24032, '#skF_30') | ~be(X12_24032, X22_24037, X21_24039, X21_24039) | ~state(X12_24032, X22_24037) | ~forename(X12_24032, X20_24040) | ~jules_forename(X12_24032, X20_24040) | ~man(X12_24032, X21_24039) | ~of(X12_24032, X20_24040, X21_24039) | ~accessible_world(X12_24032, '#skF_9') | ~think_believe_consider(X12_24032, X18_24029) | ~present(X12_24032, X18_24029) | ~event(X12_24032, X18_24029) | ~theme(X12_24032, X18_24029, '#skF_9') | ~agent(X12_24032, X18_24029, X16_24036) | ~proposition(X12_24032, '#skF_9') | ~forename(X12_24032, X17_24038) | ~vincent_forename(X12_24032, X17_24038) | ~man(X12_24032, X16_24036) | ~of(X12_24032, X17_24038, X16_24036) | ~forename(X12_24032, X15_24031) | ~vincent_forename(X12_24032, X15_24031) | ~man(X12_24032, '#skF_20') | ~of(X12_24032, X15_24031, '#skF_20') | ~forename(X12_24032, X13_24033) | ~jules_forename(X12_24032, X13_24033) | ~of(X12_24032, X13_24033, '#skF_20') | ~actual_world(X12_24032) | ~man('#skF_9', '#skF_17'('#skF_30', X13_24033, X12_24032, '#skF_20', X16_24036, X21_24039, X22_24037, X20_24040, '#skF_9', X15_24031, X18_24029, X17_24038, X23_24034))))).
% 34.73/19.20 tff(c_29990, plain, (![X20_24019, X16_24026, X23_24028, X17_24017, X18_24018, X22_24027, X12_24023, X14_24022, X27_24021, X13_24020, X24_24016, X15_24025, X21_24024]: (~smoke(X24_24016, X27_24021) | ~present(X24_24016, X27_24021) | ~agent(X24_24016, X27_24021, X14_24022) | ~event(X24_24016, X27_24021) | ~accessible_world(X12_24023, X24_24016) | ~think_believe_consider(X12_24023, X23_24028) | ~present(X12_24023, X23_24028) | ~event(X12_24023, X23_24028) | ~theme(X12_24023, X23_24028, X24_24016) | ~agent(X12_24023, X23_24028, X14_24022) | ~proposition(X12_24023, X24_24016) | ~be(X12_24023, X22_24027, X21_24024, X21_24024) | ~state(X12_24023, X22_24027) | ~forename(X12_24023, X20_24019) | ~jules_forename(X12_24023, X20_24019) | ~man(X12_24023, X21_24024) | ~of(X12_24023, X20_24019, X21_24024) | ~accessible_world(X12_24023, '#skF_9') | ~think_believe_consider(X12_24023, X18_24018) | ~present(X12_24023, X18_24018) | ~event(X12_24023, X18_24018) | ~theme(X12_24023, X18_24018, '#skF_9') | ~agent(X12_24023, X18_24018, X16_24026) | ~proposition(X12_24023, '#skF_9') | ~forename(X12_24023, X17_24017) | ~vincent_forename(X12_24023, X17_24017) | ~man(X12_24023, X16_24026) | ~of(X12_24023, X17_24017, X16_24026) | ~forename(X12_24023, X15_24025) | ~vincent_forename(X12_24023, X15_24025) | ~man(X12_24023, X14_24022) | ~of(X12_24023, X15_24025, X14_24022) | ~forename(X12_24023, X13_24020) | ~jules_forename(X12_24023, X13_24020) | ~of(X12_24023, X13_24020, X14_24022) | ~actual_world(X12_24023) | ~man('#skF_9', '#skF_17'(X24_24016, X13_24020, X12_24023, X14_24022, X16_24026, X21_24024, X22_24027, X20_24019, '#skF_9', X15_24025, X18_24018, X17_24017, X23_24028))))).
% 34.73/19.20 tff(c_29963, plain, (![X16_52, X13_49, X21_57, X23_59, X14_50, X19_55, X18_54, X26_66, X27_67, X22_58, X17_53, X12_28, X24_60, X15_51, X20_56]: (~smoke(X19_55, X26_66) | ~present(X19_55, X26_66) | ~agent(X19_55, X26_66, '#skF_17'(X24_60, X13_49, X12_28, X14_50, X16_52, X21_57, X22_58, X20_56, X19_55, X15_51, X18_54, X17_53, X23_59)) | ~event(X19_55, X26_66) | ~smoke(X24_60, X27_67) | ~present(X24_60, X27_67) | ~agent(X24_60, X27_67, X14_50) | ~event(X24_60, X27_67) | ~accessible_world(X12_28, X24_60) | ~think_believe_consider(X12_28, X23_59) | ~present(X12_28, X23_59) | ~event(X12_28, X23_59) | ~theme(X12_28, X23_59, X24_60) | ~agent(X12_28, X23_59, X14_50) | ~proposition(X12_28, X24_60) | ~be(X12_28, X22_58, X21_57, X21_57) | ~state(X12_28, X22_58) | ~forename(X12_28, X20_56) | ~jules_forename(X12_28, X20_56) | ~man(X12_28, X21_57) | ~of(X12_28, X20_56, X21_57) | ~accessible_world(X12_28, X19_55) | ~think_believe_consider(X12_28, X18_54) | ~present(X12_28, X18_54) | ~event(X12_28, X18_54) | ~theme(X12_28, X18_54, X19_55) | ~agent(X12_28, X18_54, X16_52) | ~proposition(X12_28, X19_55) | ~forename(X12_28, X17_53) | ~vincent_forename(X12_28, X17_53) | ~man(X12_28, X16_52) | ~of(X12_28, X17_53, X16_52) | ~forename(X12_28, X15_51) | ~vincent_forename(X12_28, X15_51) | ~man(X12_28, X14_50) | ~of(X12_28, X15_51, X14_50) | ~forename(X12_28, X13_49) | ~jules_forename(X12_28, X13_49) | ~of(X12_28, X13_49, X14_50) | ~actual_world(X12_28)))).
% 34.73/19.20 tff(c_29896, plain, (~proposition('#skF_18', '#skF_9'))).
% 34.73/19.20 tff(c_29883, plain, (![X13_23942, X21_23945, X16_23952, X15_23947, X23_23951, X18_23949, X19_23953, X17_23950, X9_26, X20_23944, X12_23946, X22_23948]: (man(X19_23953, '#skF_17'('#skF_9', X13_23942, X12_23946, X9_26, X16_23952, X21_23945, X22_23948, X20_23944, X19_23953, X15_23947, X18_23949, X17_23950, X23_23951)) | ~event('#skF_9', '#skF_15'(X9_26)) | ~accessible_world(X12_23946, '#skF_9') | ~think_believe_consider(X12_23946, X23_23951) | ~present(X12_23946, X23_23951) | ~event(X12_23946, X23_23951) | ~theme(X12_23946, X23_23951, '#skF_9') | ~agent(X12_23946, X23_23951, X9_26) | ~proposition(X12_23946, '#skF_9') | ~be(X12_23946, X22_23948, X21_23945, X21_23945) | ~state(X12_23946, X22_23948) | ~forename(X12_23946, X20_23944) | ~jules_forename(X12_23946, X20_23944) | ~man(X12_23946, X21_23945) | ~of(X12_23946, X20_23944, X21_23945) | ~accessible_world(X12_23946, X19_23953) | ~think_believe_consider(X12_23946, X18_23949) | ~present(X12_23946, X18_23949) | ~event(X12_23946, X18_23949) | ~theme(X12_23946, X18_23949, X19_23953) | ~agent(X12_23946, X18_23949, X16_23952) | ~proposition(X12_23946, X19_23953) | ~forename(X12_23946, X17_23950) | ~vincent_forename(X12_23946, X17_23950) | ~man(X12_23946, X16_23952) | ~of(X12_23946, X17_23950, X16_23952) | ~forename(X12_23946, X15_23947) | ~vincent_forename(X12_23946, X15_23947) | ~man(X12_23946, X9_26) | ~of(X12_23946, X15_23947, X9_26) | ~forename(X12_23946, X13_23942) | ~jules_forename(X12_23946, X13_23942) | ~of(X12_23946, X13_23942, X9_26) | ~actual_world(X12_23946) | ~man('#skF_9', X9_26)))).
% 34.73/19.20 tff(c_29874, plain, (~smoke('#skF_1', '#skF_8'))).
% 34.73/19.20 tff(c_29873, plain, (~smoke('#skF_1', '#skF_13'))).
% 34.73/19.20 tff(c_29871, plain, (~smoke('#skF_18', '#skF_29'))).
% 34.73/19.20 tff(c_29870, plain, (~smoke('#skF_18', '#skF_24'))).
% 34.73/19.20 tff(c_29868, plain, (~man('#skF_18', '#skF_4'))).
% 34.73/19.20 tff(c_29829, plain, (![X17_23890, X21_23883, X23_23891, X22_23885, X13_23879, X15_23888, X16_23882, X12_23880, X19_23887, X20_23886, X18_23889]: (man(X19_23887, '#skF_17'('#skF_14', X13_23879, X12_23880, '#skF_4', X16_23882, X21_23883, X22_23885, X20_23886, X19_23887, X15_23888, X18_23889, X17_23890, X23_23891)) | ~accessible_world(X12_23880, '#skF_14') | ~think_believe_consider(X12_23880, X23_23891) | ~present(X12_23880, X23_23891) | ~event(X12_23880, X23_23891) | ~theme(X12_23880, X23_23891, '#skF_14') | ~agent(X12_23880, X23_23891, '#skF_4') | ~proposition(X12_23880, '#skF_14') | ~be(X12_23880, X22_23885, X21_23883, X21_23883) | ~state(X12_23880, X22_23885) | ~forename(X12_23880, X20_23886) | ~jules_forename(X12_23880, X20_23886) | ~man(X12_23880, X21_23883) | ~of(X12_23880, X20_23886, X21_23883) | ~accessible_world(X12_23880, X19_23887) | ~think_believe_consider(X12_23880, X18_23889) | ~present(X12_23880, X18_23889) | ~event(X12_23880, X18_23889) | ~theme(X12_23880, X18_23889, X19_23887) | ~agent(X12_23880, X18_23889, X16_23882) | ~proposition(X12_23880, X19_23887) | ~forename(X12_23880, X17_23890) | ~vincent_forename(X12_23880, X17_23890) | ~man(X12_23880, X16_23882) | ~of(X12_23880, X17_23890, X16_23882) | ~forename(X12_23880, X15_23888) | ~vincent_forename(X12_23880, X15_23888) | ~man(X12_23880, '#skF_4') | ~of(X12_23880, X15_23888, '#skF_4') | ~forename(X12_23880, X13_23879) | ~jules_forename(X12_23880, X13_23879) | ~of(X12_23880, X13_23879, '#skF_4') | ~actual_world(X12_23880)))).
% 34.73/19.20 tff(c_29854, plain, (~man('#skF_1', '#skF_20'))).
% 34.73/19.20 tff(c_29852, plain, (![X23_23897, X16_23892, X18_23894, X13_23899, X19_23901, X17_23893, X15_23902, X20_23900]: (man(X19_23901, '#skF_17'('#skF_30', X13_23899, '#skF_18', '#skF_20', X16_23892, '#skF_27', '#skF_28', X20_23900, X19_23901, X15_23902, X18_23894, X17_23893, X23_23897)) | ~think_believe_consider('#skF_18', X23_23897) | ~present('#skF_18', X23_23897) | ~event('#skF_18', X23_23897) | ~theme('#skF_18', X23_23897, '#skF_30') | ~agent('#skF_18', X23_23897, '#skF_20') | ~forename('#skF_18', X20_23900) | ~jules_forename('#skF_18', X20_23900) | ~of('#skF_18', X20_23900, '#skF_27') | ~accessible_world('#skF_18', X19_23901) | ~think_believe_consider('#skF_18', X18_23894) | ~present('#skF_18', X18_23894) | ~event('#skF_18', X18_23894) | ~theme('#skF_18', X18_23894, X19_23901) | ~agent('#skF_18', X18_23894, X16_23892) | ~proposition('#skF_18', X19_23901) | ~forename('#skF_18', X17_23893) | ~vincent_forename('#skF_18', X17_23893) | ~man('#skF_18', X16_23892) | ~of('#skF_18', X17_23893, X16_23892) | ~forename('#skF_18', X15_23902) | ~vincent_forename('#skF_18', X15_23902) | ~of('#skF_18', X15_23902, '#skF_20') | ~forename('#skF_18', X13_23899) | ~jules_forename('#skF_18', X13_23899) | ~of('#skF_18', X13_23899, '#skF_20')))).
% 34.73/19.20 tff(c_29838, plain, (![X17_23890, X21_23883, X23_23891, X22_23885, X13_23879, X15_23888, X16_23882, X12_23880, X19_23887, X20_23886, X18_23889]: (man(X19_23887, '#skF_17'('#skF_30', X13_23879, X12_23880, '#skF_20', X16_23882, X21_23883, X22_23885, X20_23886, X19_23887, X15_23888, X18_23889, X17_23890, X23_23891)) | ~accessible_world(X12_23880, '#skF_30') | ~think_believe_consider(X12_23880, X23_23891) | ~present(X12_23880, X23_23891) | ~event(X12_23880, X23_23891) | ~theme(X12_23880, X23_23891, '#skF_30') | ~agent(X12_23880, X23_23891, '#skF_20') | ~proposition(X12_23880, '#skF_30') | ~be(X12_23880, X22_23885, X21_23883, X21_23883) | ~state(X12_23880, X22_23885) | ~forename(X12_23880, X20_23886) | ~jules_forename(X12_23880, X20_23886) | ~man(X12_23880, X21_23883) | ~of(X12_23880, X20_23886, X21_23883) | ~accessible_world(X12_23880, X19_23887) | ~think_believe_consider(X12_23880, X18_23889) | ~present(X12_23880, X18_23889) | ~event(X12_23880, X18_23889) | ~theme(X12_23880, X18_23889, X19_23887) | ~agent(X12_23880, X18_23889, X16_23882) | ~proposition(X12_23880, X19_23887) | ~forename(X12_23880, X17_23890) | ~vincent_forename(X12_23880, X17_23890) | ~man(X12_23880, X16_23882) | ~of(X12_23880, X17_23890, X16_23882) | ~forename(X12_23880, X15_23888) | ~vincent_forename(X12_23880, X15_23888) | ~man(X12_23880, '#skF_20') | ~of(X12_23880, X15_23888, '#skF_20') | ~forename(X12_23880, X13_23879) | ~jules_forename(X12_23880, X13_23879) | ~of(X12_23880, X13_23879, '#skF_20') | ~actual_world(X12_23880)))).
% 34.73/19.20 tff(c_29806, plain, (![X16_52, X13_49, X21_57, X23_59, X14_50, X19_55, X18_54, X27_67, X22_58, X17_53, X12_28, X24_60, X15_51, X20_56]: (man(X19_55, '#skF_17'(X24_60, X13_49, X12_28, X14_50, X16_52, X21_57, X22_58, X20_56, X19_55, X15_51, X18_54, X17_53, X23_59)) | ~smoke(X24_60, X27_67) | ~present(X24_60, X27_67) | ~agent(X24_60, X27_67, X14_50) | ~event(X24_60, X27_67) | ~accessible_world(X12_28, X24_60) | ~think_believe_consider(X12_28, X23_59) | ~present(X12_28, X23_59) | ~event(X12_28, X23_59) | ~theme(X12_28, X23_59, X24_60) | ~agent(X12_28, X23_59, X14_50) | ~proposition(X12_28, X24_60) | ~be(X12_28, X22_58, X21_57, X21_57) | ~state(X12_28, X22_58) | ~forename(X12_28, X20_56) | ~jules_forename(X12_28, X20_56) | ~man(X12_28, X21_57) | ~of(X12_28, X20_56, X21_57) | ~accessible_world(X12_28, X19_55) | ~think_believe_consider(X12_28, X18_54) | ~present(X12_28, X18_54) | ~event(X12_28, X18_54) | ~theme(X12_28, X18_54, X19_55) | ~agent(X12_28, X18_54, X16_52) | ~proposition(X12_28, X19_55) | ~forename(X12_28, X17_53) | ~vincent_forename(X12_28, X17_53) | ~man(X12_28, X16_52) | ~of(X12_28, X17_53, X16_52) | ~forename(X12_28, X15_51) | ~vincent_forename(X12_28, X15_51) | ~man(X12_28, X14_50) | ~of(X12_28, X15_51, X14_50) | ~forename(X12_28, X13_49) | ~jules_forename(X12_28, X13_49) | ~of(X12_28, X13_49, X14_50) | ~actual_world(X12_28)))).
% 34.73/19.20 tff(c_27427, plain, (![X9_26]: (agent('#skF_9', '#skF_15'(X9_26), X9_26) | ~man('#skF_9', X9_26)))).
% 34.73/19.20 tff(c_23595, plain, (![X9_26]: (smoke('#skF_9', '#skF_15'(X9_26)) | ~man('#skF_9', X9_26)))).
% 34.73/19.20 tff(c_18363, plain, (![X9_26]: (event('#skF_9', '#skF_15'(X9_26)) | ~man('#skF_9', X9_26)))).
% 34.73/19.20 tff(c_12501, plain, (![X9_26]: (present('#skF_9', '#skF_15'(X9_26)) | ~man('#skF_9', X9_26)))).
% 34.73/19.20 tff(c_5413, plain, (![X25_92]: (present('#skF_25', '#skF_31'(X25_92)) | ~man('#skF_25', X25_92)))).
% 34.73/19.20 tff(c_5411, plain, (![X25_92]: (smoke('#skF_25', '#skF_31'(X25_92)) | ~man('#skF_25', X25_92)))).
% 34.73/19.20 tff(c_5409, plain, (![X25_92]: (event('#skF_25', '#skF_31'(X25_92)) | ~man('#skF_25', X25_92)))).
% 34.73/19.20 tff(c_5386, plain, (be('#skF_1', '#skF_12', '#skF_11', '#skF_11'))).
% 34.73/19.20 tff(c_5349, plain, (theme('#skF_1', '#skF_13', '#skF_14'))).
% 34.73/19.20 tff(c_5337, plain, (agent('#skF_1', '#skF_13', '#skF_2'))).
% 34.73/19.20 tff(c_5326, plain, (agent('#skF_14', '#skF_16', '#skF_4'))).
% 34.73/19.20 tff(c_5315, plain, (of('#skF_1', '#skF_5', '#skF_4'))).
% 34.73/19.20 tff(c_5310, plain, (agent('#skF_1', '#skF_8', '#skF_6'))).
% 34.73/19.20 tff(c_5285, plain, (of('#skF_1', '#skF_10', '#skF_11'))).
% 34.73/19.20 tff(c_5282, plain, (of('#skF_1', '#skF_3', '#skF_2'))).
% 34.73/19.20 tff(c_5280, plain, (of('#skF_1', '#skF_7', '#skF_6'))).
% 34.73/19.20 tff(c_5279, plain, (theme('#skF_1', '#skF_8', '#skF_9'))).
% 34.73/19.20 tff(c_5234, plain, (accessible_world('#skF_1', '#skF_14'))).
% 34.73/19.20 tff(c_5225, plain, (vincent_forename('#skF_1', '#skF_3'))).
% 34.73/19.20 tff(c_5218, plain, (forename('#skF_1', '#skF_7'))).
% 34.73/19.20 tff(c_5212, plain, (proposition('#skF_1', '#skF_14'))).
% 34.73/19.20 tff(c_5208, plain, (event('#skF_14', '#skF_16'))).
% 34.73/19.20 tff(c_5203, plain, (jules_forename('#skF_1', '#skF_5'))).
% 34.73/19.20 tff(c_5174, plain, (jules_forename('#skF_1', '#skF_10'))).
% 34.73/19.20 tff(c_5167, plain, (forename('#skF_1', '#skF_10'))).
% 34.73/19.20 tff(c_5159, plain, (present('#skF_1', '#skF_8'))).
% 34.73/19.20 tff(c_5158, plain, (man('#skF_1', '#skF_2'))).
% 34.73/19.20 tff(c_5156, plain, (state('#skF_1', '#skF_12'))).
% 34.73/19.20 tff(c_5154, plain, (think_believe_consider('#skF_1', '#skF_8'))).
% 34.73/19.20 tff(c_5151, plain, (proposition('#skF_1', '#skF_9'))).
% 34.73/19.20 tff(c_5150, plain, (vincent_forename('#skF_1', '#skF_7'))).
% 34.73/19.21 tff(c_5149, plain, (man('#skF_1', '#skF_11'))).
% 34.73/19.21 tff(c_5145, plain, (forename('#skF_1', '#skF_5'))).
% 34.73/19.21 tff(c_5143, plain, (event('#skF_1', '#skF_8'))).
% 34.73/19.21 tff(c_5139, plain, (present('#skF_1', '#skF_13'))).
% 34.73/19.21 tff(c_5137, plain, (think_believe_consider('#skF_1', '#skF_13'))).
% 34.73/19.21 tff(c_5136, plain, (man('#skF_1', '#skF_4'))).
% 34.73/19.21 tff(c_5134, plain, (present('#skF_14', '#skF_16'))).
% 34.73/19.21 tff(c_5132, plain, (forename('#skF_1', '#skF_3'))).
% 34.73/19.21 tff(c_5126, plain, (accessible_world('#skF_1', '#skF_9'))).
% 34.73/19.21 tff(c_5124, plain, (event('#skF_1', '#skF_13'))).
% 34.73/19.21 tff(c_5123, plain, (man('#skF_1', '#skF_6'))).
% 34.73/19.21 tff(c_5122, plain, (smoke('#skF_14', '#skF_16'))).
% 34.73/19.21 tff(c_5103, plain, (actual_world('#skF_1'))).
% 34.73/19.21 tff(c_4944, plain, (be('#skF_18', '#skF_28', '#skF_27', '#skF_27'))).
% 34.73/19.21 tff(c_4454, plain, (of('#skF_18', '#skF_21', '#skF_20'))).
% 34.73/19.21 tff(c_4376, plain, (of('#skF_18', '#skF_23', '#skF_22'))).
% 34.73/19.21 tff(c_4336, plain, (theme('#skF_18', '#skF_29', '#skF_30'))).
% 34.73/19.21 tff(c_4283, plain, (agent('#skF_18', '#skF_29', '#skF_20'))).
% 34.73/19.21 tff(c_4178, plain, (theme('#skF_18', '#skF_24', '#skF_25'))).
% 34.73/19.21 tff(c_4130, plain, (agent('#skF_30', '#skF_32', '#skF_20'))).
% 34.73/19.21 tff(c_4072, plain, (agent('#skF_18', '#skF_24', '#skF_22'))).
% 34.73/19.21 tff(c_3990, plain, (of('#skF_18', '#skF_19', '#skF_20'))).
% 34.73/19.21 tff(c_3870, plain, (of('#skF_18', '#skF_26', '#skF_27'))).
% 34.73/19.21 tff(c_3836, plain, (think_believe_consider('#skF_18', '#skF_24'))).
% 34.73/19.21 tff(c_3835, plain, (proposition('#skF_18', '#skF_25'))).
% 34.73/19.21 tff(c_3834, plain, (think_believe_consider('#skF_18', '#skF_29'))).
% 34.73/19.21 tff(c_3833, plain, (jules_forename('#skF_18', '#skF_19'))).
% 34.73/19.21 tff(c_3830, plain, (man('#skF_18', '#skF_22'))).
% 34.73/19.21 tff(c_3827, plain, (present('#skF_18', '#skF_29'))).
% 34.73/19.21 tff(c_3826, plain, (present('#skF_18', '#skF_24'))).
% 34.73/19.21 tff(c_3825, plain, (accessible_world('#skF_18', '#skF_30'))).
% 34.73/19.21 tff(c_3823, plain, (proposition('#skF_18', '#skF_30'))).
% 34.73/19.21 tff(c_3822, plain, (event('#skF_18', '#skF_29'))).
% 34.73/19.21 tff(c_3820, plain, (event('#skF_18', '#skF_24'))).
% 34.73/19.21 tff(c_3817, plain, (smoke('#skF_30', '#skF_32'))).
% 34.73/19.21 tff(c_3816, plain, (accessible_world('#skF_18', '#skF_25'))).
% 34.73/19.21 tff(c_3813, plain, (event('#skF_30', '#skF_32'))).
% 34.73/19.21 tff(c_3812, plain, (present('#skF_30', '#skF_32'))).
% 34.73/19.21 tff(c_3810, plain, (forename('#skF_18', '#skF_21'))).
% 34.73/19.21 tff(c_3809, plain, (forename('#skF_18', '#skF_19'))).
% 34.73/19.21 tff(c_3805, plain, (forename('#skF_18', '#skF_26'))).
% 34.73/19.21 tff(c_3804, plain, (vincent_forename('#skF_18', '#skF_23'))).
% 34.73/19.21 tff(c_3801, plain, (man('#skF_18', '#skF_20'))).
% 34.73/19.21 tff(c_3795, plain, (state('#skF_18', '#skF_28'))).
% 34.73/19.21 tff(c_3794, plain, (jules_forename('#skF_18', '#skF_26'))).
% 34.73/19.21 tff(c_3792, plain, (man('#skF_18', '#skF_27'))).
% 34.73/19.21 tff(c_3790, plain, (forename('#skF_18', '#skF_23'))).
% 34.73/19.21 tff(c_3788, plain, (vincent_forename('#skF_18', '#skF_21'))).
% 34.73/19.21 tff(c_3785, plain, (actual_world('#skF_18'))).
% 34.73/19.21 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.73/19.21
%------------------------------------------------------------------------------