%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP222+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n026.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 03:16:15 EDT 2022 % Result : CounterSatisfiable 0.40s 0.57s % Output : Saturation 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP222+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 00:24:04 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.40/0.57 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.57 % 0.40/0.57 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.57 |- ~definitionFOFtoCNF_0 $X3 $Y \/ man $Y $X3 % 0.40/0.57 |- ~man $Y $X3 \/ agent $Y (skolemFOFtoCNF_X4_1 $X3 $Y) $X3 \/ % 0.40/0.57 definitionFOFtoCNF_0 $X3 $Y % 0.40/0.57 |- ~man $Y $X3 \/ definitionFOFtoCNF_0 $X3 $Y \/ % 0.40/0.57 event $Y (skolemFOFtoCNF_X4_1 $X3 $Y) % 0.40/0.57 |- ~man $Y $X3 \/ definitionFOFtoCNF_0 $X3 $Y \/ % 0.40/0.57 present $Y (skolemFOFtoCNF_X4_1 $X3 $Y) % 0.40/0.57 |- ~man $Y $X3 \/ definitionFOFtoCNF_0 $X3 $Y \/ % 0.40/0.57 smoke $Y (skolemFOFtoCNF_X4_1 $X3 $Y) % 0.40/0.57 |- ~agent $Y $X4 $X3 \/ ~definitionFOFtoCNF_0 $X3 $Y \/ ~event $Y $X4 \/ % 0.40/0.57 ~present $Y $X4 \/ ~smoke $Y $X4 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ actual_world skolemFOFtoCNF_X5 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6 % 0.40/0.57 skolemFOFtoCNF_X12 \/ definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $W $V \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) $X14 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $W $V \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $W $V \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~man skolemFOFtoCNF_X11 $X14 \/ ~of $U $W $V \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.57 |- actual_world skolemFOFtoCNF_X5_1 % 0.40/0.57 |- accessible_world skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X11_1 % 0.40/0.57 |- agent skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X8_1 % 0.40/0.57 |- be skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X13_1 skolemFOFtoCNF_X6_1 % 0.40/0.57 skolemFOFtoCNF_X12_1 % 0.40/0.57 |- event skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 % 0.40/0.57 |- forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 % 0.40/0.57 |- forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1 % 0.40/0.57 |- jules_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 % 0.40/0.57 |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X12_1 % 0.40/0.57 |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X6_1 % 0.40/0.57 |- man skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X8_1 % 0.40/0.57 |- of skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X7_1 skolemFOFtoCNF_X6_1 % 0.40/0.57 |- of skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1 skolemFOFtoCNF_X8_1 % 0.40/0.57 |- present skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 % 0.40/0.57 |- proposition skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X11_1 % 0.40/0.57 |- state skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X13_1 % 0.40/0.57 |- theme skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 skolemFOFtoCNF_X11_1 % 0.40/0.57 |- think_believe_consider skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 % 0.40/0.57 |- vincent_forename skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X9_1 % 0.40/0.57 |- ~man skolemFOFtoCNF_X11_1 $X14 \/ % 0.40/0.57 agent skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14) $X14 % 0.40/0.57 |- ~man skolemFOFtoCNF_X11_1 $X14 \/ % 0.40/0.57 event skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14) % 0.40/0.57 |- ~man skolemFOFtoCNF_X11_1 $X14 \/ % 0.40/0.57 present skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14) % 0.40/0.57 |- ~man skolemFOFtoCNF_X11_1 $X14 \/ % 0.40/0.57 smoke skolemFOFtoCNF_X11_1 (skolemFOFtoCNF_X15_1 $X14) % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $V \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $W \/ % 0.40/0.57 ~forename $U $Z \/ ~jules_forename $U $Z \/ ~man $U $V \/ ~man $U $X1 \/ % 0.40/0.57 ~of $U $W $V \/ ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.57 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $W \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3_1 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 accessible_world skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ actual_world skolemFOFtoCNF_X5 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 agent skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X8 \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 be skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 skolemFOFtoCNF_X6 % 0.40/0.57 skolemFOFtoCNF_X12 \/ definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 event skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 jules_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X12 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X6 % 0.40/0.57 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.57 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.57 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.57 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.57 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.57 ~vincent_forename $U $Z \/ % 0.40/0.57 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.57 man skolemFOFtoCNF_X5 skolemFOFtoCNF_X8 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 of skolemFOFtoCNF_X5 skolemFOFtoCNF_X7 skolemFOFtoCNF_X6 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 of skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 skolemFOFtoCNF_X8 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 present skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 proposition skolemFOFtoCNF_X5 skolemFOFtoCNF_X11 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 state skolemFOFtoCNF_X5 skolemFOFtoCNF_X13 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 theme skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 skolemFOFtoCNF_X11 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 think_believe_consider skolemFOFtoCNF_X5 skolemFOFtoCNF_X10 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.40/0.58 ~present $U $X \/ ~proposition $U $Y \/ ~state $U $X2 \/ % 0.40/0.58 ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 vincent_forename skolemFOFtoCNF_X5 skolemFOFtoCNF_X9 % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~man skolemFOFtoCNF_X11 $X14 \/ % 0.40/0.58 ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.58 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 agent skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) $X14 \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~man skolemFOFtoCNF_X11 $X14 \/ % 0.40/0.58 ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.58 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 event skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~man skolemFOFtoCNF_X11 $X14 \/ % 0.40/0.58 ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.58 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 present skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.58 |- ~accessible_world $U $Y \/ ~actual_world $U \/ ~agent $U $X $X1 \/ % 0.40/0.58 ~be $U $X2 $X1 $X1 \/ ~event $U $X \/ ~forename $U $Z \/ % 0.40/0.58 ~jules_forename $U $Z \/ ~man $U $X1 \/ ~man skolemFOFtoCNF_X11 $X14 \/ % 0.40/0.58 ~of $U $Z $X1 \/ ~present $U $X \/ ~proposition $U $Y \/ % 0.40/0.58 ~state $U $X2 \/ ~theme $U $X $Y \/ ~think_believe_consider $U $X \/ % 0.40/0.58 ~vincent_forename $U $Z \/ % 0.40/0.58 definitionFOFtoCNF_0 (skolemFOFtoCNF_X3 $Y) $Y \/ % 0.40/0.58 smoke skolemFOFtoCNF_X11 (skolemFOFtoCNF_X15 $X14) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 event skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 event skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 event skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 present skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 present skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 present skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 smoke skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 smoke skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 smoke skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 |- agent skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 skolemFOFtoCNF_X12_1 \/ % 0.40/0.58 definitionFOFtoCNF_0 skolemFOFtoCNF_X12_1 skolemFOFtoCNF_X5_1 % 0.40/0.58 |- agent skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 skolemFOFtoCNF_X6_1 \/ % 0.40/0.58 definitionFOFtoCNF_0 skolemFOFtoCNF_X6_1 skolemFOFtoCNF_X5_1 % 0.40/0.58 |- agent skolemFOFtoCNF_X5_1 % 0.40/0.58 (skolemFOFtoCNF_X4_1 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1) % 0.40/0.58 skolemFOFtoCNF_X8_1 \/ % 0.40/0.58 definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 % 0.40/0.58 |- ~definitionFOFtoCNF_0 skolemFOFtoCNF_X8_1 skolemFOFtoCNF_X5_1 \/ % 0.40/0.58 ~smoke skolemFOFtoCNF_X5_1 skolemFOFtoCNF_X10_1 % 0.40/0.58 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.58 %------------------------------------------------------------------------------