%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : NLP239-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n011.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 : 600s % DateTime : Mon Jul 18 02:14:16 EDT 2022 % Result : Satisfiable 0.19s 0.44s % Output : CNFRefutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP239-1 : TPTP v8.1.0. Released v2.4.0. % 0.08/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 1 11:46:04 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.38 # No SInE strategy applied % 0.13/0.38 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.13/0.38 # and selection function SelectComplexExceptUniqMaxHorn. % 0.13/0.38 # % 0.13/0.38 # Presaturation interreduction done % 0.13/0.38 # Number of axioms: 84 Number of unprocessed: 84 % 0.13/0.38 # Tableaux proof search. % 0.13/0.38 # APR header successfully linked. % 0.13/0.38 # Hello from C++ % 0.13/0.39 # The folding up rule is enabled... % 0.13/0.39 # Local unification is enabled... % 0.13/0.39 # Any saturation attempts will use folding labels... % 0.13/0.39 # 84 beginning clauses after preprocessing and clausification % 0.13/0.39 # Creating start rules for all 84 conjectures. % 0.13/0.39 # There are 84 start rule candidates: % 0.13/0.39 # Found 2 unit axioms. % 0.13/0.39 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.13/0.39 # 84 start rule tableaux created. % 0.13/0.39 # 82 extension rule candidate clauses % 0.13/0.39 # 2 unit axiom clauses % 0.13/0.39 % 0.13/0.39 # Requested 8, 32 cores available to the main process. % 0.19/0.44 # Ran out of tableaux, making start rules for all clauses % 0.19/0.44 # 29723 Satisfiable branch % 0.19/0.44 # Ran out of tableaux, making start rules for all clauses % 0.19/0.44 # 29722 Satisfiable branch % 0.19/0.44 # Satisfiable branch found. % 0.19/0.44 # There were 1 total branch saturation attempts. % 0.19/0.44 # There were 0 of these attempts blocked. % 0.19/0.44 # There were 0 deferred branch saturation attempts. % 0.19/0.44 # There were 0 free duplicated saturations. % 0.19/0.44 # There were 0 total successful branch saturations. % 0.19/0.44 # There were 0 successful branch saturations in interreduction. % 0.19/0.44 # There were 0 successful branch saturations on the branch. % 0.19/0.44 # There were 0 successful branch saturations after the branch. % 0.19/0.44 # Satisfiable branch found. % 0.19/0.44 # There were 1 total branch saturation attempts. % 0.19/0.44 # There were 0 of these attempts blocked. % 0.19/0.44 # There were 0 deferred branch saturation attempts. % 0.19/0.44 # There were 0 free duplicated saturations. % 0.19/0.44 # There were 0 total successful branch saturations. % 0.19/0.44 # There were 0 successful branch saturations in interreduction. % 0.19/0.44 # There were 0 successful branch saturations on the branch. % 0.19/0.44 # There were 0 successful branch saturations after the branch. % 0.19/0.44 # SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.44 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.44 # Begin clausification derivation % 0.19/0.44 % 0.19/0.44 # End clausification derivation % 0.19/0.44 # Begin listing active clauses obtained from FOF to CNF conversion % 0.19/0.44 cnf(i_0_85, negated_conjecture, (actual_world(skc45))). % 0.19/0.44 cnf(i_0_86, negated_conjecture, (actual_world(skc28))). % 0.19/0.44 cnf(i_0_117, negated_conjecture, (accessible_world(skc28,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_118, negated_conjecture, (accessible_world(skc28,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_116, negated_conjecture, (proposition(skc28,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_87, negated_conjecture, (accessible_world(skc45,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_102, negated_conjecture, (accessible_world(skc45,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_119, negated_conjecture, (proposition(skc28,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_120, negated_conjecture, (event(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_133, negated_conjecture, (event(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_128, negated_conjecture, (event(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_88, negated_conjecture, (proposition(skc45,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_121, negated_conjecture, (present(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_132, negated_conjecture, (present(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_127, negated_conjecture, (present(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_122, negated_conjecture, (think_believe_consider(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_101, negated_conjecture, (proposition(skc45,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_89, negated_conjecture, (event(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_131, negated_conjecture, (think_believe_consider(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_115, negated_conjecture, (forename(skc28,skc42)|~ssSkC0)). % 0.19/0.44 cnf(i_0_123, negated_conjecture, (forename(skc28,skc35)|~ssSkC0)). % 0.19/0.44 cnf(i_0_129, negated_conjecture, (forename(skc28,skc37)|~ssSkC0)). % 0.19/0.44 cnf(i_0_105, negated_conjecture, (event(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_135, negated_conjecture, (forename(skc28,skc31)|~ssSkC0)). % 0.19/0.44 cnf(i_0_124, negated_conjecture, (vincent_forename(skc28,skc35)|~ssSkC0)). % 0.19/0.44 cnf(i_0_134, negated_conjecture, (vincent_forename(skc28,skc31)|~ssSkC0)). % 0.19/0.44 cnf(i_0_113, negated_conjecture, (man(skc28,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_99, negated_conjecture, (event(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_90, negated_conjecture, (present(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_125, negated_conjecture, (man(skc28,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_136, negated_conjecture, (man(skc28,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_114, negated_conjecture, (jules_forename(skc28,skc42)|~ssSkC0)). % 0.19/0.44 cnf(i_0_130, negated_conjecture, (jules_forename(skc28,skc37)|~ssSkC0)). % 0.19/0.44 cnf(i_0_104, negated_conjecture, (present(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_126, negated_conjecture, (smoke(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_112, negated_conjecture, (state(skc28,skc40)|~ssSkC0)). % 0.19/0.44 cnf(i_0_98, negated_conjecture, (present(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_91, negated_conjecture, (think_believe_consider(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_103, negated_conjecture, (think_believe_consider(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_92, negated_conjecture, (forename(skc45,skc57)|ssSkC0)). % 0.19/0.44 cnf(i_0_96, negated_conjecture, (forename(skc45,skc52)|ssSkC0)). % 0.19/0.44 cnf(i_0_107, negated_conjecture, (forename(skc45,skc51)|ssSkC0)). % 0.19/0.44 cnf(i_0_111, negated_conjecture, (forename(skc45,skc50)|ssSkC0)). % 0.19/0.44 cnf(i_0_93, negated_conjecture, (vincent_forename(skc45,skc57)|ssSkC0)). % 0.19/0.44 cnf(i_0_108, negated_conjecture, (vincent_forename(skc45,skc51)|ssSkC0)). % 0.19/0.44 cnf(i_0_94, negated_conjecture, (man(skc45,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_100, negated_conjecture, (man(skc45,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_109, negated_conjecture, (man(skc45,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_95, negated_conjecture, (jules_forename(skc45,skc52)|ssSkC0)). % 0.19/0.44 cnf(i_0_110, negated_conjecture, (jules_forename(skc45,skc50)|ssSkC0)). % 0.19/0.44 cnf(i_0_97, negated_conjecture, (smoke(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_106, negated_conjecture, (state(skc45,skc48)|ssSkC0)). % 0.19/0.44 cnf(i_0_147, negated_conjecture, (theme(skc28,skc34,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_152, negated_conjecture, (theme(skc28,skc30,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_146, negated_conjecture, (of(skc28,skc42,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_137, negated_conjecture, (theme(skc45,skc56,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_148, negat# SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.44 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.44 # Begin clausification derivation % 0.19/0.44 % 0.19/0.44 # End clausification derivation % 0.19/0.44 # Begin listing active clauses obtained from FOF to CNF conversion % 0.19/0.44 cnf(i_0_85, negated_conjecture, (actual_world(skc45))). % 0.19/0.44 cnf(i_0_86, negated_conjecture, (actual_world(skc28))). % 0.19/0.44 cnf(i_0_117, negated_conjecture, (accessible_world(skc28,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_118, negated_conjecture, (accessible_world(skc28,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_116, negated_conjecture, (proposition(skc28,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_87, negated_conjecture, (accessible_world(skc45,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_102, negated_conjecture, (accessible_world(skc45,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_119, negated_conjecture, (proposition(skc28,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_120, negated_conjecture, (event(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_133, negated_conjecture, (event(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_128, negated_conjecture, (event(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_88, negated_conjecture, (proposition(skc45,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_121, negated_conjecture, (present(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_132, negated_conjecture, (present(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_127, negated_conjecture, (present(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_122, negated_conjecture, (think_believe_consider(skc28,skc34)|~ssSkC0)). % 0.19/0.44 cnf(i_0_101, negated_conjecture, (proposition(skc45,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_89, negated_conjecture, (event(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_131, negated_conjecture, (think_believe_consider(skc28,skc30)|~ssSkC0)). % 0.19/0.44 cnf(i_0_115, negated_conjecture, (forename(skc28,skc42)|~ssSkC0)). % 0.19/0.44 cnf(i_0_123, negated_conjecture, (forename(skc28,skc35)|~ssSkC0)). % 0.19/0.44 cnf(i_0_129, negated_conjecture, (forename(skc28,skc37)|~ssSkC0)). % 0.19/0.44 cnf(i_0_105, negated_conjecture, (event(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_135, negated_conjecture, (forename(skc28,skc31)|~ssSkC0)). % 0.19/0.44 cnf(i_0_124, negated_conjecture, (vincent_forename(skc28,skc35)|~ssSkC0)). % 0.19/0.44 cnf(i_0_134, negated_conjecture, (vincent_forename(skc28,skc31)|~ssSkC0)). % 0.19/0.44 cnf(i_0_113, negated_conjecture, (man(skc28,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_99, negated_conjecture, (event(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_90, negated_conjecture, (present(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_125, negated_conjecture, (man(skc28,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_136, negated_conjecture, (man(skc28,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_114, negated_conjecture, (jules_forename(skc28,skc42)|~ssSkC0)). % 0.19/0.44 cnf(i_0_130, negated_conjecture, (jules_forename(skc28,skc37)|~ssSkC0)). % 0.19/0.44 cnf(i_0_104, negated_conjecture, (present(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_126, negated_conjecture, (smoke(skc29,skc38)|~ssSkC0)). % 0.19/0.44 cnf(i_0_112, negated_conjecture, (state(skc28,skc40)|~ssSkC0)). % 0.19/0.44 cnf(i_0_98, negated_conjecture, (present(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_91, negated_conjecture, (think_believe_consider(skc45,skc56)|ssSkC0)). % 0.19/0.44 cnf(i_0_103, negated_conjecture, (think_believe_consider(skc45,skc47)|ssSkC0)). % 0.19/0.44 cnf(i_0_92, negated_conjecture, (forename(skc45,skc57)|ssSkC0)). % 0.19/0.44 cnf(i_0_96, negated_conjecture, (forename(skc45,skc52)|ssSkC0)). % 0.19/0.44 cnf(i_0_107, negated_conjecture, (forename(skc45,skc51)|ssSkC0)). % 0.19/0.44 cnf(i_0_111, negated_conjecture, (forename(skc45,skc50)|ssSkC0)). % 0.19/0.44 cnf(i_0_93, negated_conjecture, (vincent_forename(skc45,skc57)|ssSkC0)). % 0.19/0.44 cnf(i_0_108, negated_conjecture, (vincent_forename(skc45,skc51)|ssSkC0)). % 0.19/0.44 cnf(i_0_94, negated_conjecture, (man(skc45,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_100, negated_conjecture, (man(skc45,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_109, negated_conjecture, (man(skc45,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_95, negated_conjecture, (jules_forename(skc45,skc52)|ssSkC0)). % 0.19/0.44 cnf(i_0_110, negated_conjecture, (jules_forename(skc45,skc50)|ssSkC0)). % 0.19/0.44 cnf(i_0_97, negated_conjecture, (smoke(skc46,skc54)|ssSkC0)). % 0.19/0.44 cnf(i_0_106, negated_conjecture, (state(skc45,skc48)|ssSkC0)). % 0.19/0.44 cnf(i_0_147, negated_conjecture, (theme(skc28,skc34,skc33)|~ssSkC0)). % 0.19/0.44 cnf(i_0_152, negated_conjecture, (theme(skc28,skc30,skc29)|~ssSkC0)). % 0.19/0.44 cnf(i_0_146, negated_conjecture, (of(skc28,skc42,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_137, negated_conjecture, (theme(skc45,skc56,skc55)|ssSkC0)). % 0.19/0.44 cnf(i_0_148, negated_conjecture, (of(skc28,skc35,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_151, negated_conjecture, (of(skc28,skc37,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_154, negated_conjecture, (of(skc28,skc31,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_149, negated_conjecture, (agent(skc28,skc34,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_157, negated_conjecture, (event(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_142, negated_conjecture, (theme(skc45,skc47,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_153, negated_conjecture, (agent(skc28,skc30,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_150, negated_conjecture, (agent(skc29,skc38,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_138, negated_conjecture, (of(skc45,skc57,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_141, negated_conjecture, (of(skc45,skc52,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_143, negated_conjecture, (of(skc45,skc51,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_145, negated_conjecture, (of(skc45,skc50,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_139, negated_conjecture, (agent(skc45,skc56,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_144, negated_conjecture, (agent(skc45,skc47,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_140, negated_conjecture, (agent(skc46,skc54,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_158, negated_conjecture, (present(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_155, negated_conjecture, (be(skc45,skc48,skc49,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_160, negated_conjecture, (event(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_161, negated_conjecture, (present(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_162, negated_conjecture, (smoke(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_156, negated_conjecture, (be(skc28,skc40,skc41,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_159, negated_conjecture, (smoke(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_164, negated_conjecture, (agent(skc33,skf6(X1),X1)|~man(skc33,X1)|~ssSkC0)). % 0.19/0.44 cnf(i_0_163, negated_conjecture, (agent(skc55,skf10(X1),X1)|ssSkC0|~man(skc55,X1))). % 0.19/0.44 cnf(i_0_166, negated_conjecture, (man(X1,skf8(X1))|~be(X2,X3,X4,X4)|~agent(X5,X6,X7)|~agent(X2,X8,X4)|~agent(X2,X9,X10)|~of(X2,X11,X4)|~of(X2,X12,X4)|~of(X2,X13,X7)|~of(X2,X14,X10)|~theme(X2,X8,X5)|~theme(X2,X9,X1)|~state(X2,X3)|~smoke(X5,X6)|~jules_forename(X2,X11)|~jules_forename(X2,X13)|~man(X2,X4)|~man(X2,X7)|~man(X2,X10)|~vincent_forename(X2,X12)|~vincent_forename(X2,X14)|~forename(X2,X11)|~forename(X2,X12)|~forename(X2,X13)|~forename(X2,X14)|~think_believe_consider(X2,X8)|~think_believe_consider(X2,X9)|~present(X5,X6)|~present(X2,X8)|~present(X2,X9)|~event(X5,X6)|~event(X2,X8)|~event(X2,X9)|~proposition(X2,X5)|~proposition(X2,X1)|~accessible_world(X2,X5)|~accessible_world(X2,X1)|~ssSkC0|~actual_world(X2))). % 0.19/0.44 cnf(i_0_165, negated_conjecture, (man(X1,skf12(X1))|ssSkC0|~be(X2,X3,X4,X4)|~agent(X5,X6,X7)|~agent(X2,X8,X9)|~agent(X2,X10,X7)|~of(X2,X11,X9)|~of(X2,X12,X7)|~of(X2,X13,X7)|~of(X2,X14,X4)|~theme(X2,X8,X5)|~theme(X2,X10,X1)|~state(X2,X3)|~smoke(X5,X6)|~jules_forename(X2,X12)|~jules_forename(X2,X14)|~man(X2,X9)|~man(X2,X7)|~man(X2,X4)|~vincent_forename(X2,X11)|~vincent_forename(X2,X13)|~forename(X2,X11)|~forename(X2,X12)|~forename(X2,X13)|~forename(X2,X14)|~think_believe_consider(X2,X8)|~think_believe_consider(X2,X10)|~present(X5,X6)|~present(X2,X8)|~present(X2,X10)|~event(X5,X6)|~event(X2,X8)|~event(X2,X10)|~proposition(X2,X1)|~proposition(X2,X5)|~accessible_world(X2,X1)|~accessible_world(X2,X5)|~actual_world(X2))). % 0.19/0.44 cnf(i_0_167, negated_conjecture, (ssSkC0|~be(X1,X2,X3,X3)|~agent(X4,X5,skf12(X4))|~agent(X6,X7,X8)|~agent(X1,X9,X10)|~agent(X1,X11,X8)|~of(X1,X12,X10)|~of(X1,X13,X8)|~of(X1,X14,X8)|~of(X1,X15,X3)|~theme(X1,X9,X6)|~theme(X1,X11,X4)|~state(X1,X2)|~smoke(X4,X5)|~smoke(X6,X7)|~jules_forename(X1,X13)|~jules_forename(X1,X15)|~man(X1,X10)|~man(X1,X8)|~man(X1,X3)|~vincent_forename(X1,X12)|~vincent_forename(X1,X14)|~forename(X1,X12)|~forename(X1,X13)|~forename(X1,X14)|~forename(X1,X15)|~think_believe_consider(X1,X9)|~think_believe_consider(X1,X11)|~present(X4,X5)|~present(X6,X7)|~present(X1,X9)|~present(X1,X11)|~event(X4,X5)|~event(X6,X7)|~event(X1,X9)|~event(X1,X11)|~proposition(X1,X4)|~proposition(X1,X6)|~accessible_world(X1,X4)|~accessible_world(X1,X6)|~actual_world(X1))). % 0.19/0.44 cnf(i_0_168, negated_conjecture, (~be(X1,X2,X3,X3)|~agent(X4,X5,skf8(X4))|~agent(X6,X7,X8)|~agent(X1,X9,X3)|~agent(X1,X10,X11)|~of(X1,X12,X3)|~of(X1,X13,X3)|~of(X1,X14,X8)|~of(X1,X15,X11)|~theme(X1,X9,X6)|~theme(X1,X10,X4)|~state(X1,X2)|~smoke(X6,X7)|~smoke(X4,X5)|~jules_forename(X1,X12)|~jules_forename(X1,X14)|~man(X1,X3)|~man(X1,X8)|~man(X1,X11)|~vincent_forename(X1,X13)|~vincent_forename(X1,X15)|~forename(X1,X12)|~forename(X1,X13)|~forename(X1,X14)|~forename(X1,X15)|~think_believe_consider(X1,X9)|~think_believe_consider(X1,X10)|~present(X6,X7)|~present(X1,X9)|~present(X1,X10)|~present(X4,X5)|~event(X6,X7)|~event(X1,X9)|~event(X1,X10)|~event(X4,X5)|~proposition(X1,X6)|~proposition(X1,X4)|~accessible_world(X1,X6)|~accessible_world(X1,X4)|~ssSkC0|~actual_world(X1))). % 0.19/0.44 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.19/0.44 # Begin printing tableau % 0.19/0.44 # Found 3 steps % 0.19/0.44 cnf(i_0_86, negated_conjecture, (actual_world(skc28)), inference(start_rule)). % 0.19/0.44 cnf(i_0_6448, plain, (actual_world(skc28)), inference(extension_rule, [i_0_167])). % 0.19/0.44 cnf(i_0_9072, plain, (ssSkC0), inference(extension_rule, [i_0_156])). % 0.19/0.44 # End printing tableau % 0.19/0.44 # SZS output end % 0.19/0.44 # Branches closed with saturation will be marked with an "s" % 0.19/0.44 ed_conjecture, (of(skc28,skc35,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_151, negated_conjecture, (of(skc28,skc37,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_154, negated_conjecture, (of(skc28,skc31,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_149, negated_conjecture, (agent(skc28,skc34,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_157, negated_conjecture, (event(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_142, negated_conjecture, (theme(skc45,skc47,skc46)|ssSkC0)). % 0.19/0.44 cnf(i_0_153, negated_conjecture, (agent(skc28,skc30,skc32)|~ssSkC0)). % 0.19/0.44 cnf(i_0_150, negated_conjecture, (agent(skc29,skc38,skc36)|~ssSkC0)). % 0.19/0.44 cnf(i_0_138, negated_conjecture, (of(skc45,skc57,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_141, negated_conjecture, (of(skc45,skc52,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_143, negated_conjecture, (of(skc45,skc51,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_145, negated_conjecture, (of(skc45,skc50,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_139, negated_conjecture, (agent(skc45,skc56,skc58)|ssSkC0)). % 0.19/0.44 cnf(i_0_144, negated_conjecture, (agent(skc45,skc47,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_140, negated_conjecture, (agent(skc46,skc54,skc53)|ssSkC0)). % 0.19/0.44 cnf(i_0_158, negated_conjecture, (present(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_155, negated_conjecture, (be(skc45,skc48,skc49,skc49)|ssSkC0)). % 0.19/0.44 cnf(i_0_160, negated_conjecture, (event(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_161, negated_conjecture, (present(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_162, negated_conjecture, (smoke(skc33,skf6(X1))|~man(skc33,X2)|~ssSkC0)). % 0.19/0.44 cnf(i_0_156, negated_conjecture, (be(skc28,skc40,skc41,skc41)|~ssSkC0)). % 0.19/0.44 cnf(i_0_159, negated_conjecture, (smoke(skc55,skf10(X1))|ssSkC0|~man(skc55,X2))). % 0.19/0.44 cnf(i_0_164, negated_conjecture, (agent(skc33,skf6(X1),X1)|~man(skc33,X1)|~ssSkC0)). % 0.19/0.44 cnf(i_0_163, negated_conjecture, (agent(skc55,skf10(X1),X1)|ssSkC0|~man(skc55,X1))). % 0.19/0.44 cnf(i_0_166, negated_conjecture, (man(X1,skf8(X1))|~be(X2,X3,X4,X4)|~agent(X5,X6,X7)|~agent(X2,X8,X4)|~agent(X2,X9,X10)|~of(X2,X11,X4)|~of(X2,X12,X4)|~of(X2,X13,X7)|~of(X2,X14,X10)|~theme(X2,X8,X5)|~theme(X2,X9,X1)|~state(X2,X3)|~smoke(X5,X6)|~jules_forename(X2,X11)|~jules_forename(X2,X13)|~man(X2,X4)|~man(X2,X7)|~man(X2,X10)|~vincent_forename(X2,X12)|~vincent_forename(X2,X14)|~forename(X2,X11)|~forename(X2,X12)|~forename(X2,X13)|~forename(X2,X14)|~think_believe_consider(X2,X8)|~think_believe_consider(X2,X9)|~present(X5,X6)|~present(X2,X8)|~present(X2,X9)|~event(X5,X6)|~event(X2,X8)|~event(X2,X9)|~proposition(X2,X5)|~proposition(X2,X1)|~accessible_world(X2,X5)|~accessible_world(X2,X1)|~ssSkC0|~actual_world(X2))). % 0.19/0.44 cnf(i_0_165, negated_conjecture, (man(X1,skf12(X1))|ssSkC0|~be(X2,X3,X4,X4)|~agent(X5,X6,X7)|~agent(X2,X8,X9)|~agent(X2,X10,X7)|~of(X2,X11,X9)|~of(X2,X12,X7)|~of(X2,X13,X7)|~of(X2,X14,X4)|~theme(X2,X8,X5)|~theme(X2,X10,X1)|~state(X2,X3)|~smoke(X5,X6)|~jules_forename(X2,X12)|~jules_forename(X2,X14)|~man(X2,X9)|~man(X2,X7)|~man(X2,X4)|~vincent_forename(X2,X11)|~vincent_forename(X2,X13)|~forename(X2,X11)|~forename(X2,X12)|~forename(X2,X13)|~forename(X2,X14)|~think_believe_consider(X2,X8)|~think_believe_consider(X2,X10)|~present(X5,X6)|~present(X2,X8)|~present(X2,X10)|~event(X5,X6)|~event(X2,X8)|~event(X2,X10)|~proposition(X2,X1)|~proposition(X2,X5)|~accessible_world(X2,X1)|~accessible_world(X2,X5)|~actual_world(X2))). % 0.19/0.44 cnf(i_0_167, negated_conjecture, (ssSkC0|~be(X1,X2,X3,X3)|~agent(X4,X5,skf12(X4))|~agent(X6,X7,X8)|~agent(X1,X9,X10)|~agent(X1,X11,X8)|~of(X1,X12,X10)|~of(X1,X13,X8)|~of(X1,X14,X8)|~of(X1,X15,X3)|~theme(X1,X9,X6)|~theme(X1,X11,X4)|~state(X1,X2)|~smoke(X4,X5)|~smoke(X6,X7)|~jules_forename(X1,X13)|~jules_forename(X1,X15)|~man(X1,X10)|~man(X1,X8)|~man(X1,X3)|~vincent_forename(X1,X12)|~vincent_forename(X1,X14)|~forename(X1,X12)|~forename(X1,X13)|~forename(X1,X14)|~forename(X1,X15)|~think_believe_consider(X1,X9)|~think_believe_consider(X1,X11)|~present(X4,X5)|~present(X6,X7)|~present(X1,X9)|~present(X1,X11)|~event(X4,X5)|~event(X6,X7)|~event(X1,X9)|~event(X1,X11)|~proposition(X1,X4)|~proposition(X1,X6)|~accessible_world(X1,X4)|~accessible_world(X1,X6)|~actual_world(X1))). % 0.19/0.44 cnf(i_0_168, negated_conjecture, (~be(X1,X2,X3,X3)|~agent(X4,X5,skf8(X4))|~agent(X6,X7,X8)|~agent(X1,X9,X3)|~agent(X1,X10,X11)|~of(X1,X12,X3)|~of(X1,X13,X3)|~of(X1,X14,X8)|~of(X1,X15,X11)|~theme(X1,X9,X6)|~theme(X1,X10,X4)|~state(X1,X2)|~smoke(X6,X7)|~smoke(X4,X5)|~jules_forename(X1,X12)|~jules_forename(X1,X14)|~man(X1,X3)|~man(X1,X8)|~man(X1,X11)|~vincent_forename(X1,X13)|~vincent_forename(X1,X15)|~forename(X1,X12)|~forename(X1,X13)|~forename(X1,X14)|~forename(X1,X15)|~think_believe_consider(X1,X9)|~think_believe_consider(X1,X10)|~present(X6,X7)|~present(X1,X9)|~present(X1,X10)|~present(X4,X5)|~event(X6,X7)|~event(X1,X9)|~event(X1,X10)|~event(X4,X5)|~proposition(X1,X6)|~proposition(X1,X4)|~accessible_world(X1,X6)|~accessible_world(X1,X4)|~ssSkC0|~actual_world(X1))). % 0.19/0.44 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.19/0.44 # Begin printing tableau % 0.19/0.44 # Found 3 steps % 0.19/0.44 cnf(i_0_86, negated_conjecture, (actual_world(skc28)), inference(start_rule)). % 0.19/0.44 cnf(i_0_6448, plain, (actual_world(skc28)), inference(extension_rule, [i_0_167])). % 0.19/0.44 cnf(i_0_9072, plain, (ssSkC0), inference(extension_rule, [i_0_156])). % 0.19/0.44 # End printing tableau % 0.19/0.44 # SZS output end % 0.19/0.44 # Branches closed with saturation will be marked with an "s" % 0.19/0.44 # Child (29722) has found a proof. % 0.19/0.44 % 0.19/0.44 # Proof search is over... % 0.19/0.44 # Freeing feature tree %------------------------------------------------------------------------------