%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : NLP116-1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n007.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:21 EDT 2024 % Result : Unknown 0.41s 0.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NLP116-1 : TPTP v8.2.0. Released v2.4.0. % 0.03/0.13 % Command : run_zenon_modulo %d %s % 0.13/0.34 % Computer : n007.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 : 300 % 0.13/0.34 % DateTime : Sat Jun 22 22:36:39 EDT 2024 % 0.13/0.35 % CPUTime : % 0.41/0.58 Zenon error: exhausted search space without finding a proof % 0.41/0.58 (* Current branch: % 0.41/0.58 (white (skc15) (skc17)) % 0.41/0.58 (chevy (skc15) (skc17)) % 0.41/0.58 (in (skc10) (skc11) (skc13)) % 0.41/0.58 (white (skc10) (skc12)) % 0.41/0.58 (city (skc10) (skc13)) % 0.41/0.58 (lonely (skc10) (skc13)) % 0.41/0.58 ((skc12) != zenon_X61) % 0.41/0.58 ((skc17) != (skc19)) % 0.41/0.58 ((skc13) != zenon_X34) % 0.41/0.58 (-. (agent (skc10) (skc11) (skc12))) % 0.41/0.58 ((skc12) != zenon_X48) % 0.41/0.58 ((skc13) != (skc19)) % 0.41/0.58 ((skc16) != zenon_X41) % 0.41/0.58 (chevy (skc10) (skc12)) % 0.41/0.58 ((skc14) != zenon_X53) % 0.41/0.58 ((skc17) != zenon_X61) % 0.41/0.58 (down (skc10) (skc11) (skc13)) % 0.41/0.58 (in (skc15) (skc16) (skc17)) % 0.41/0.58 (present (skc10) (skc11)) % 0.41/0.58 ((skc14) != zenon_X46) % 0.41/0.58 ((skc11) != zenon_X38) % 0.41/0.58 (-. (chevy (skc10) zenon_X64)) % 0.41/0.58 (-. (chevy (skc15) zenon_X49)) % 0.41/0.58 (city (skc15) (skc17)) % 0.41/0.58 (-. (chevy (skc10) zenon_X67)) % 0.41/0.58 (placename (skc15) (skc18)) % 0.41/0.58 (-. (hollywood_placename (skc15) zenon_X59)) % 0.41/0.58 ((skc18) != zenon_X53) % 0.41/0.58 (barrel (skc15) (skc16)) % 0.41/0.58 (actual_world (skc15)) % 0.41/0.58 (-. (chevy (skc10) zenon_X55)) % 0.41/0.58 (present (skc15) (skc16)) % 0.41/0.58 (-. (city (skc15) (skc19))) % 0.41/0.58 (-. (hollywood_placename (skc10) zenon_X44)) % 0.41/0.58 ((skc18) != zenon_X46) % 0.41/0.58 (-. (chevy (skc10) zenon_X71)) % 0.41/0.58 ((skc16) != zenon_X56) % 0.41/0.58 ((skc10) != zenon_X0) % 0.41/0.58 (street (skc15) (skc19)) % 0.41/0.58 ((skc14) != zenon_X44) % 0.41/0.58 ((skc11) != zenon_X56) % 0.41/0.58 ((skc12) != zenon_X64) % 0.41/0.58 (-. (hollywood_placename (skc15) zenon_X46)) % 0.41/0.58 ((skc10) != (skc15)) % 0.41/0.58 ((skc16) != zenon_X50) % 0.41/0.58 (old (skc10) (skc12)) % 0.41/0.58 ((skc11) != zenon_X41) % 0.41/0.58 (of (skc10) (skc14) (skc13)) % 0.41/0.58 (-. (hollywood_placename (skc10) zenon_X53)) % 0.41/0.58 (-. (lonely (skc15) zenon_X34)) % 0.41/0.58 ((skc13) != zenon_X30) % 0.41/0.58 (actual_world (skc10)) % 0.41/0.58 (-. (hollywood_placename (skc10) zenon_X62)) % 0.41/0.58 (-. (barrel (skc10) zenon_X38)) % 0.41/0.58 (dirty (skc15) (skc17)) % 0.41/0.58 ((skc12) != zenon_X67) % 0.41/0.58 (-. (actual_world zenon_X0)) % 0.41/0.58 (hollywood_placename (skc10) (skc14)) % 0.41/0.58 (dirty (skc10) (skc12)) % 0.41/0.58 (agent (skc15) (skc16) (skc17)) % 0.41/0.58 (-. (chevy (skc10) zenon_X48)) % 0.41/0.58 ((skc19) != zenon_X30) % 0.41/0.58 (hollywood_placename (skc15) (skc18)) % 0.41/0.58 ((skc18) != zenon_X44) % 0.41/0.58 (old (skc15) (skc17)) % 0.41/0.58 (street (skc10) (skc13)) % 0.41/0.58 (event (skc15) (skc16)) % 0.41/0.58 ((skc17) != zenon_X55) % 0.41/0.58 (-. (barrel (skc15) zenon_X56)) % 0.41/0.58 ((skc11) != (skc16)) % 0.41/0.58 (-. (chevy (skc10) (skc17))) % 0.41/0.58 ((skc18) != zenon_X59) % 0.41/0.58 (down (skc15) (skc16) (skc19)) % 0.41/0.58 ((skc15) != zenon_X0) % 0.41/0.58 (-. (lonely (skc15) (skc13))) % 0.41/0.58 (placename (skc10) (skc14)) % 0.41/0.58 (-. (lonely (skc10) zenon_X30)) % 0.41/0.58 (-. (barrel (skc10) (skc16))) % 0.41/0.58 (-. (chevy (skc15) zenon_X61)) % 0.41/0.58 ((skc17) != zenon_X49) % 0.41/0.58 ((skc17) != (skc12)) % 0.41/0.58 ((skc19) != zenon_X34) % 0.41/0.58 (lonely (skc15) (skc19)) % 0.41/0.58 ((skc14) != zenon_X62) % 0.41/0.58 (-. (ssSkC0)) % 0.41/0.58 (-. (barrel (skc15) zenon_X41)) % 0.41/0.58 ((skc14) != zenon_X59) % 0.41/0.58 (-. (barrel (skc10) zenon_X50)) % 0.41/0.58 (barrel (skc10) (skc11)) % 0.41/0.58 ((skc12) != zenon_X55) % 0.41/0.58 ((skc17) != zenon_X48) % 0.41/0.58 (of (skc15) (skc18) (skc17)) % 0.41/0.58 ((skc12) != zenon_X71) % 0.41/0.58 ((skc11) != zenon_X50) % 0.41/0.58 (event (skc10) (skc11)) % 0.41/0.58 ((skc12) != zenon_X49) % 0.41/0.58 ((skc16) != zenon_X38) % 0.41/0.58 *) % 0.41/0.58 (* NO-PROOF *) % 0.41/0.58 % SZS status GaveUp % 0.41/0.58 Number of rewrites on terms: 0 % 0.41/0.58 Number of rewrites on props: 0 % 0.41/0.58 nodes searched: 584 % 0.41/0.58 max branch formulas: 220 % 0.41/0.58 proof nodes created: 162 % 0.41/0.58 formulas created: 4142 % 0.41/0.58 %------------------------------------------------------------------------------