%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : MGT104+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n002.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 : Wed Apr 29 02:09:05 PM UTC 2026 % Result : Unsatisfiable 9.64s 3.40s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : MGT104+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.35 % Computer : n002.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue Apr 28 19:20:16 EDT 2026 % 0.18/0.35 % CPUTime : % 9.64/3.40 % SZS status Theorem % 10.09/3.50 % SZS status Error % 10.09/3.50 % Exception: No conjecture found in the problem. % 10.09/3.50 % lisa.tptp.Problem.conjecture$$anonfun$2(package.scala:27) % 10.09/3.50 % scala.Option.getOrElse(Option.scala:201) % 10.09/3.50 % lisa.tptp.Problem.conjecture(package.scala:27) % 10.09/3.50 % TPTP_Lisa$.tableau(TPTP_Lisa.scala:53) % 10.09/3.50 % TPTP_Lisa$.$anonfun$4(TPTP_Lisa.scala:80) % 10.09/3.50 % mainargs.Invoker$.$anonfun$2(Invoker.scala:77) % 10.09/3.50 % mainargs.Result.flatMap(Result.scala:13) % 10.09/3.50 % mainargs.Result.flatMap$(Result.scala:7) % 10.09/3.50 % mainargs.Result$Success.flatMap(Result.scala:23) % 10.09/3.50 % mainargs.Invoker$.invoke0(Invoker.scala:77) % 10.09/3.50 % mainargs.Invoker$.invoke(Invoker.scala:86) % 10.09/3.50 % mainargs.Invoker$.invokeLocal$1(Invoker.scala:106) % 10.09/3.50 % mainargs.Invoker$.groupArgs$1$$anonfun$2(Invoker.scala:121) % 10.09/3.50 % mainargs.Result.flatMap(Result.scala:13) % 10.09/3.50 % mainargs.Result.flatMap$(Result.scala:7) % 10.09/3.50 % mainargs.Result$Success.flatMap(Result.scala:23) % 10.09/3.50 % mainargs.Invoker$.groupArgs$1(Invoker.scala:121) % 10.09/3.50 % mainargs.Invoker$.runMains(Invoker.scala:139) % 10.09/3.50 % mainargs.ParserForMethods.runRaw0(Parser.scala:290) % 10.09/3.50 % mainargs.ParserForMethods.runEither(Parser.scala:178) % 10.09/3.50 % mainargs.ParserForMethods.runOrThrow(Parser.scala:154) % 10.09/3.50 % TPTP_Lisa$.main(TPTP_Lisa.scala:80) % 10.09/3.50 % TPTP_Lisa.main(TPTP_Lisa.scala) %------------------------------------------------------------------------------