%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : NLP101-1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n014.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:19 EDT 2024 % Result : Unknown 0.39s 0.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NLP101-1 : TPTP v8.2.0. Released v2.4.0. % 0.03/0.13 % Command : run_zenon_modulo %d %s % 0.13/0.35 % Computer : n014.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sat Jun 22 23:15:54 EDT 2024 % 0.13/0.35 % CPUTime : % 0.39/0.56 Zenon error: exhausted search space without finding a proof % 0.39/0.56 (* Current branch: % 0.39/0.56 ((skf9 zenon_X40) != zenon_X98) % 0.39/0.56 (-. (event (skc17) zenon_X118)) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X102) % 0.39/0.56 (past (skc6) (skf8 zenon_X19)) % 0.39/0.56 (patient (skc17) (skf17 zenon_X13) (skc19)) % 0.39/0.56 ((skf9 zenon_X31) != zenon_X84) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X115) % 0.39/0.56 ((skc18) != (skf9 zenon_X40)) % 0.39/0.56 (agent (skc6) (skf9 zenon_X48) (skf11 zenon_X48)) % 0.39/0.56 ((skc18) != zenon_X84) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X98) % 0.39/0.56 ((skf9 zenon_X31) != zenon_X79) % 0.39/0.56 (-. (human_person (skc17) zenon_X93)) % 0.39/0.56 (-. (drink (skc6) zenon_X79)) % 0.39/0.56 (-. (restaurant (skc17) (skf22 zenon_X1))) % 0.39/0.56 ((skf10 zenon_X43) != zenon_X105) % 0.39/0.56 ((skc22) != zenon_X89) % 0.39/0.56 ((skf22 zenon_X1) != zenon_X101) % 0.39/0.56 ((skc18) != (skf8 zenon_X16)) % 0.39/0.56 ((skc20) != zenon_X96) % 0.39/0.56 (customer zenon_X0 (skf27 zenon_X0)) % 0.39/0.56 (zenon_X6 != zenon_X4) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X111) % 0.39/0.56 ((skc20) != (skf22 zenon_X1)) % 0.39/0.56 ((skf9 zenon_X37) != (skf17 zenon_X4)) % 0.39/0.56 (-. (event (skc17) (skf8 zenon_X16))) % 0.39/0.56 ((skf11 zenon_X28) != zenon_X122) % 0.39/0.56 (-. (event (skc6) zenon_X126)) % 0.39/0.56 (patient (skc6) (skf9 zenon_X51) (skf10 zenon_X51)) % 0.39/0.56 (-. (coffee (skc6) zenon_X105)) % 0.39/0.56 (-. (actual_world zenon_X73)) % 0.39/0.56 ((skf8 zenon_X25) != (skc18)) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X118) % 0.39/0.56 (past (skc17) (skf17 zenon_X6)) % 0.39/0.56 (-. (event (skc17) zenon_X120)) % 0.39/0.56 (drink (skc17) (skc18)) % 0.39/0.56 (agent (skc6) (skf8 zenon_X45) zenon_X45) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X120) % 0.39/0.56 (past (skc6) (skf9 zenon_X37)) % 0.39/0.56 ((skc18) != zenon_X102) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X120) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X102) % 0.39/0.56 ((skc18) != zenon_X79) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X126) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X120) % 0.39/0.56 ((skf22 zenon_X1) != zenon_X96) % 0.39/0.56 (ssSkC0) % 0.39/0.56 (-. (restaurant (skc17) zenon_X96)) % 0.39/0.56 (event (skc6) (skf9 zenon_X40)) % 0.39/0.56 (patient (skc6) (skf8 zenon_X54) (skf11 zenon_X54)) % 0.39/0.56 (-. (past (skc17) (skf17 zenon_X4))) % 0.39/0.56 ((skc17) != zenon_X73) % 0.39/0.56 (event (skc17) (skf17 zenon_X4)) % 0.39/0.56 (zenon_X1 != (skc6)) % 0.39/0.56 (agent (skc17) (skf17 zenon_X11) zenon_X11) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X102) % 0.39/0.56 ((skc18) != zenon_X115) % 0.39/0.56 (see (skc17) (skf17 zenon_X10)) % 0.39/0.56 ((skc20) != zenon_X101) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X121) % 0.39/0.56 ((skc6) != (skc17)) % 0.39/0.56 (nonreflexive (skc6) (skf9 zenon_X34)) % 0.39/0.56 ((skc18) != zenon_X111) % 0.39/0.56 (zenon_X1 != (skc17)) % 0.39/0.56 (in zenon_X62 (skf13 zenon_X62 zenon_X66 zenon_X67) zenon_X66) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X115) % 0.39/0.56 (nonreflexive (skc6) (skf8 zenon_X22)) % 0.39/0.56 ((skc6) != zenon_X73) % 0.39/0.56 (-. (restaurant (skc6) zenon_X125)) % 0.39/0.56 (drink (skc6) (skf9 zenon_X31)) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X111) % 0.39/0.56 (-. (restaurant (skc6) zenon_X110)) % 0.39/0.56 (nonreflexive (skc17) (skc18)) % 0.39/0.56 ((skc18) != zenon_X118) % 0.39/0.56 (in zenon_X2 (skf27 zenon_X2) (skf22 zenon_X2)) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X111) % 0.39/0.56 (-. (event (skc6) zenon_X111)) % 0.39/0.56 (customer zenon_X55 (skf13 zenon_X55 zenon_X61 zenon_X59)) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X118) % 0.39/0.56 ((skf11 zenon_X28) != zenon_X93) % 0.39/0.56 (see (skc6) (skf8 zenon_X25)) % 0.39/0.56 ((skc18) != (skf17 zenon_X4)) % 0.39/0.56 ((skf17 zenon_X4) != (skf8 zenon_X16)) % 0.39/0.56 (-. (restaurant (skc6) zenon_X101)) % 0.39/0.56 ((skf17 zenon_X4) != (skf9 zenon_X40)) % 0.39/0.56 (-. (event (skc17) (skf9 zenon_X40))) % 0.39/0.56 (human_person (skc6) (skf11 zenon_X28)) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X115) % 0.39/0.56 (actual_world (skc17)) % 0.39/0.56 (restaurant zenon_X1 (skf22 zenon_X1)) % 0.39/0.56 (actual_world (skc6)) % 0.39/0.56 (-. (event (skc17) zenon_X98)) % 0.39/0.56 (-. (event (skc6) zenon_X102)) % 0.39/0.56 ((skc18) != zenon_X120) % 0.39/0.56 ((skf9 zenon_X40) != zenon_X121) % 0.39/0.56 (-. (drink (skc17) zenon_X84)) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X118) % 0.39/0.56 ((skc20) != zenon_X110) % 0.39/0.56 (nonreflexive (skc17) (skf17 zenon_X8)) % 0.39/0.56 ((skf17 zenon_X4) != zenon_X98) % 0.39/0.56 ((skf8 zenon_X19) != (skf17 zenon_X4)) % 0.39/0.56 (agent (skc17) (skc18) (skc19)) % 0.39/0.56 (human_person (skc17) (skc19)) % 0.39/0.56 (-. (event (skc6) zenon_X121)) % 0.39/0.56 ((skc18) != zenon_X98) % 0.39/0.56 (-. (event (skc17) zenon_X115)) % 0.39/0.56 (patient (skc17) (skc18) (skc22)) % 0.39/0.56 (event (skc6) (skf8 zenon_X16)) % 0.39/0.56 (-. (see (skc17) (skc18))) % 0.39/0.56 (-. (restaurant (skc6) (skf22 zenon_X1))) % 0.39/0.56 (past (skc17) (skc18)) % 0.39/0.56 (restaurant (skc17) (skc20)) % 0.39/0.56 ((skf17 zenon_X10) != (skc18)) % 0.39/0.56 ((skc19) != zenon_X93) % 0.39/0.56 ((skc22) != zenon_X105) % 0.39/0.56 (-. (coffee (skc17) zenon_X89)) % 0.39/0.56 (coffee (skc6) (skf10 zenon_X43)) % 0.39/0.56 ((skf17 zenon_X6) != (skf17 zenon_X4)) % 0.39/0.56 (-. (restaurant (skc6) (skc20))) % 0.39/0.56 (-. (human_person (skc6) zenon_X122)) % 0.39/0.56 ((skf10 zenon_X43) != zenon_X89) % 0.39/0.56 (event (skc17) (skc18)) % 0.39/0.56 (coffee (skc17) (skc22)) % 0.39/0.56 ((skf8 zenon_X16) != zenon_X126) % 0.39/0.57 *) % 0.39/0.57 (* NO-PROOF *) % 0.39/0.57 % SZS status GaveUp % 0.39/0.57 Number of rewrites on terms: 0 % 0.39/0.57 Number of rewrites on props: 0 % 0.39/0.57 nodes searched: 459 % 0.39/0.57 max branch formulas: 338 % 0.39/0.57 proof nodes created: 69 % 0.39/0.57 formulas created: 4657 % 0.39/0.57 %------------------------------------------------------------------------------