%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : NLP221+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n005.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 : Tue Jun 25 02:03:37 EDT 2024 % Result : Unknown 0.17s 0.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : NLP221+1 : TPTP v8.2.0. Released v2.4.0. % 0.11/0.11 % Command : run_zenon_modulo %d %s % 0.11/0.32 % Computer : n005.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sat Jun 22 22:26:24 EDT 2024 % 0.11/0.32 % CPUTime : % 0.17/0.51 Zenon error: exhausted search space without finding a proof % 0.17/0.51 (* Current branch: % 0.17/0.51 (Tau_7 != zenon_X81) % 0.17/0.51 (Tau_5 != zenon_X60) % 0.17/0.51 (Tau_7 != zenon_X31) % 0.17/0.51 (Tau_1 != zenon_X21) % 0.17/0.51 (-. (be Tau_0 zenon_X78 Tau_1 Tau_7)) % 0.17/0.51 (-. (be Tau_0 zenon_X96 Tau_1 zenon_X95)) % 0.17/0.51 (Tau_8 != zenon_X90) % 0.17/0.51 (Tau_7 != zenon_X97) % 0.17/0.51 (-. (accessible_world Tau_0 zenon_X83)) % 0.17/0.51 (-. (be Tau_0 zenon_X75 Tau_1 zenon_X74)) % 0.17/0.51 (-. (be Tau_0 zenon_X79 Tau_1 Tau_7)) % 0.17/0.51 (Tau_7 != zenon_X92) % 0.17/0.51 (-. (accessible_world Tau_0 zenon_X91)) % 0.17/0.51 (Tau_2 != Tau_4) % 0.17/0.51 (-. (forename Tau_0 zenon_X20)) % 0.17/0.51 (-. (be Tau_0 zenon_X27 zenon_X21 Tau_7)) % 0.17/0.51 (Tau_8 != zenon_X59) % 0.17/0.51 (Tau_7 != zenon_X84) % 0.17/0.51 (-. (be Tau_0 zenon_X82 Tau_1 zenon_X81)) % 0.17/0.51 (Tau_7 != zenon_X44) % 0.17/0.51 (-. (be Tau_0 zenon_X58 Tau_1 Tau_7)) % 0.17/0.51 (-. (be Tau_0 zenon_X26 zenon_X21 zenon_X25)) % 0.17/0.51 (actual_world Tau_0) % 0.17/0.51 (think_believe_consider Tau_0 Tau_5) % 0.17/0.51 (-. (forename Tau_0 zenon_X53)) % 0.17/0.51 (-. (jules_forename Tau_0 Tau_4)) % 0.17/0.51 (event Tau_0 Tau_5) % 0.17/0.51 (smoke Tau_6 Tau_10) % 0.17/0.51 (man Tau_0 Tau_1) % 0.17/0.51 (-. (be Tau_0 zenon_X71 Tau_1 zenon_X70)) % 0.17/0.51 (Tau_4 != zenon_X53) % 0.17/0.51 (Tau_7 != zenon_X95) % 0.17/0.51 (-. (accessible_world Tau_0 zenon_X87)) % 0.17/0.51 (Tau_2 != zenon_X48) % 0.17/0.51 (-. (think_believe_consider Tau_0 zenon_X64)) % 0.17/0.51 (Tau_5 != zenon_X72) % 0.17/0.51 (man Tau_0 Tau_3) % 0.17/0.51 (-. (be zenon_X11 zenon_X18 zenon_X13 zenon_X17)) % 0.17/0.51 (-. (be Tau_0 zenon_X94 Tau_1 Tau_7)) % 0.17/0.51 (Tau_7 != zenon_X103) % 0.17/0.51 (Tau_1 != zenon_X40) % 0.17/0.51 (Tau_7 != zenon_X74) % 0.17/0.51 (Tau_108 != Tau_5) % 0.17/0.51 (-. (be Tau_0 zenon_X90 Tau_1 Tau_7)) % 0.17/0.51 (-. (accessible_world Tau_0 zenon_X80)) % 0.17/0.51 (-. (be Tau_0 Tau_8 zenon_X21 Tau_7)) % 0.17/0.51 (present Tau_6 Tau_10) % 0.17/0.51 (Tau_7 != zenon_X88) % 0.17/0.51 (Tau_7 != zenon_X66) % 0.17/0.51 (proposition Tau_0 Tau_6) % 0.17/0.51 (-. (be Tau_0 zenon_X45 zenon_X40 zenon_X44)) % 0.17/0.51 (-. (be Tau_0 zenon_X67 Tau_1 zenon_X66)) % 0.17/0.51 (-. (be Tau_0 zenon_X63 Tau_1 zenon_X62)) % 0.17/0.51 (-. (be Tau_0 zenon_X93 Tau_1 zenon_X92)) % 0.17/0.51 (be Tau_0 Tau_8 Tau_1 Tau_7) % 0.17/0.51 (Tau_1 != zenon_X34) % 0.17/0.51 (of Tau_0 Tau_2 Tau_1) % 0.17/0.51 (Tau_3 != Tau_1) % 0.17/0.51 (Tau_8 != zenon_X46) % 0.17/0.51 (state Tau_0 Tau_8) % 0.17/0.51 (Tau_8 != zenon_X76) % 0.17/0.51 (Tau_7 != zenon_X56) % 0.17/0.51 (Tau_7 != zenon_X100) % 0.17/0.51 (Tau_7 != zenon_X25) % 0.17/0.51 (Tau_8 != zenon_X27) % 0.17/0.51 (Tau_6 != zenon_X80) % 0.17/0.51 (-. (be Tau_0 zenon_X47 zenon_X40 Tau_7)) % 0.17/0.51 (-. (be zenon_X11 zenon_X19 zenon_X13 Tau_7)) % 0.17/0.51 (Tau_8 != zenon_X33) % 0.17/0.51 (Tau_2 != zenon_X53) % 0.17/0.51 (-. (be Tau_0 zenon_X105 Tau_1 Tau_7)) % 0.17/0.51 (-. (be Tau_0 zenon_X89 Tau_1 zenon_X88)) % 0.17/0.51 (zenon_X9 != Tau_1) % 0.17/0.51 (-. (think_believe_consider Tau_0 zenon_X60)) % 0.17/0.51 (-. (be Tau_0 zenon_X57 Tau_1 zenon_X56)) % 0.17/0.51 (forename Tau_0 Tau_4) % 0.17/0.51 (Tau_8 != zenon_X58) % 0.17/0.51 (Tau_7 != zenon_X17) % 0.17/0.51 (-. (be Tau_0 zenon_X99 Tau_1 Tau_7)) % 0.17/0.51 (Tau_5 != zenon_X64) % 0.17/0.51 (-. (be Tau_0 zenon_X101 Tau_1 zenon_X100)) % 0.17/0.51 (smoke Tau_6 Tau_108) % 0.17/0.51 (agent Tau_0 Tau_5 Tau_3) % 0.17/0.51 (Tau_6 != zenon_X91) % 0.17/0.51 (-. (be Tau_0 zenon_X86 Tau_1 Tau_7)) % 0.17/0.51 (-. (forename Tau_0 zenon_X48)) % 0.17/0.51 (Tau_8 != zenon_X105) % 0.17/0.51 (jules_forename Tau_0 Tau_2) % 0.17/0.51 (present Tau_6 Tau_108) % 0.17/0.51 (Tau_2 != zenon_X20) % 0.17/0.51 (-. (be Tau_0 zenon_X76 Tau_1 Tau_7)) % 0.17/0.51 (-. (be Tau_0 zenon_X85 Tau_1 zenon_X84)) % 0.17/0.51 (accessible_world Tau_0 Tau_6) % 0.17/0.51 (-. (be Tau_0 zenon_X104 Tau_1 zenon_X103)) % 0.17/0.51 (Tau_6 != zenon_X83) % 0.17/0.51 (-. (agent Tau_0 Tau_5 Tau_1)) % 0.17/0.51 (Tau_8 != zenon_X102) % 0.17/0.51 (Tau_5 != zenon_X68) % 0.17/0.51 (Tau_8 != zenon_X94) % 0.17/0.51 (-. (be Tau_0 zenon_X39 zenon_X34 zenon_X38)) % 0.17/0.51 (theme Tau_0 Tau_5 Tau_6) % 0.17/0.51 (-. (be Tau_0 zenon_X77 Tau_1 Tau_7)) % 0.17/0.51 (Tau_8 != zenon_X78) % 0.17/0.52 (-. (be Tau_0 zenon_X102 Tau_1 Tau_7)) % 0.17/0.52 (Tau_0 != zenon_X11) % 0.17/0.52 (-. (think_believe_consider Tau_0 zenon_X72)) % 0.17/0.52 (Tau_4 != zenon_X20) % 0.17/0.52 (-. (be Tau_0 Tau_8 zenon_X40 Tau_7)) % 0.17/0.52 (Tau_8 != zenon_X86) % 0.17/0.52 (-. (be Tau_0 zenon_X59 Tau_1 Tau_7)) % 0.17/0.52 (event Tau_6 Tau_108) % 0.17/0.52 (Tau_8 != zenon_X99) % 0.17/0.52 (-. (be Tau_0 zenon_X32 Tau_1 zenon_X31)) % 0.17/0.52 (present Tau_0 Tau_5) % 0.17/0.52 (agent Tau_6 Tau_10 zenon_X9) % 0.17/0.52 (event Tau_6 Tau_10) % 0.17/0.52 (Tau_8 != zenon_X47) % 0.17/0.52 (-. (be Tau_0 zenon_X33 Tau_1 Tau_7)) % 0.17/0.52 (-. (be Tau_0 Tau_8 zenon_X34 Tau_7)) % 0.17/0.52 (Tau_6 != zenon_X87) % 0.17/0.52 (of Tau_0 Tau_4 Tau_3) % 0.17/0.52 (forename Tau_0 Tau_2) % 0.17/0.52 (-. (be Tau_0 zenon_X46 zenon_X34 Tau_7)) % 0.17/0.52 (Tau_7 != zenon_X38) % 0.17/0.52 (man Tau_0 Tau_7) % 0.17/0.52 (Tau_7 != zenon_X51) % 0.17/0.52 (-. (be Tau_0 zenon_X98 Tau_1 zenon_X97)) % 0.17/0.52 (Tau_7 != zenon_X62) % 0.17/0.52 (Tau_8 != zenon_X79) % 0.17/0.52 (-. (think_believe_consider Tau_0 zenon_X68)) % 0.17/0.52 (vincent_forename Tau_0 Tau_4) % 0.17/0.52 (agent Tau_6 Tau_108 Tau_1) % 0.17/0.52 (Tau_4 != zenon_X48) % 0.17/0.52 (-. (be Tau_0 zenon_X52 Tau_1 zenon_X51)) % 0.17/0.52 (Tau_7 != zenon_X70) % 0.17/0.52 (Tau_8 != zenon_X77) % 0.17/0.52 *) % 0.17/0.52 (* NO-PROOF *) % 0.17/0.52 % SZS status GaveUp % 0.17/0.52 Number of rewrites on terms: 0 % 0.17/0.52 Number of rewrites on props: 0 % 0.17/0.52 nodes searched: 433 % 0.17/0.52 max branch formulas: 310 % 0.17/0.52 proof nodes created: 93 % 0.17/0.52 formulas created: 4712 % 0.17/0.52 %------------------------------------------------------------------------------