%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : PLA026+1 : TPTP v6.1.0. Bugfixed v2.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n020.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16127.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Fri Aug 1 22:08:19 EDT 2014 % Result : CounterSatisfiable 32.90s % Output : Model 32.90s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : PLA026+1 : TPTP v6.1.0. Bugfixed v2.5.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n020.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 16127.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Fri Jul 25 15:42:36 CDT 2014 % % CPUTime : 32.90 % E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % % % Defaulting to tptp format. % Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % Parsing /export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax ... % % % % Proving ... % % % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % a_block(block_4) % a_block(block_1) % a_block(block_5) % a_block(block_2) % a_block(table) % a_block(block_3) % clear(block_4, s(s(s(s(s(time_0)))))) % clear(block_4, s(s(s(time_0)))) % clear(block_4, s(s(time_0))) % clear(block_4, s(time_0)) % clear(block_5, s(s(s(s(s(time_0)))))) % clear(block_5, s(s(s(s(time_0))))) % clear(block_5, s(s(s(time_0)))) % clear(block_5, s(time_0)) % clear(block_5, time_0) % clear(block_3, s(s(s(s(s(time_0)))))) % clear(block_3, s(s(s(s(time_0))))) % clear(block_3, time_0) % destination(block_4, s(s(s(time_0)))) % destination(block_5, s(time_0)) % destination(table, s(s(s(s(time_0))))) % destination(table, s(s(time_0))) % destination(block_3, time_0) % different(block_4, block_5) % different(block_4, table) % different(block_1, block_4) % different(block_1, block_5) % different(block_1, block_2) % different(block_1, table) % different(block_1, block_3) % different(block_5, table) % different(block_2, block_4) % different(block_2, block_5) % different(block_2, table) % different(block_2, block_3) % different(block_3, block_4) % different(block_3, block_5) % different(block_3, table) % fixed(table) % goal_time(s(s(s(s(time_0))))) % goal_time(sK0) % neq(block_4, block_1) % neq(block_4, block_5) % neq(block_4, block_2) % neq(block_4, table) % neq(block_4, block_3) % neq(block_1, block_4) % neq(block_1, block_5) % neq(block_1, block_2) % neq(block_1, table) % neq(block_1, block_3) % neq(block_5, block_4) % neq(block_5, block_1) % neq(block_5, block_2) % neq(block_5, table) % neq(block_5, block_3) % neq(block_2, block_4) % neq(block_2, block_1) % neq(block_2, block_5) % neq(block_2, table) % neq(block_2, block_3) % neq(table, block_4) % neq(table, block_1) % neq(table, block_5) % neq(table, block_2) % neq(table, block_3) % neq(block_3, block_4) % neq(block_3, block_1) % neq(block_3, block_5) % neq(block_3, block_2) % neq(block_3, table) % nonfixed(block_4) % nonfixed(block_1) % nonfixed(block_5) % nonfixed(block_2) % nonfixed(block_3) % object(block_4, s(s(time_0))) % object(block_4, s(time_0)) % object(block_5, s(s(s(s(time_0))))) % object(block_5, s(s(s(time_0)))) % object(block_5, time_0) % on(block_4, block_5, s(s(time_0))) % on(block_4, table, s(s(s(s(s(time_0)))))) % on(block_4, table, s(s(s(s(time_0))))) % on(block_4, table, s(s(s(time_0)))) % on(block_4, table, s(time_0)) % on(block_4, table, time_0) % on(block_1, table, s(s(s(s(s(time_0)))))) % on(block_1, table, s(s(s(s(time_0))))) % on(block_1, table, s(s(s(time_0)))) % on(block_1, table, s(s(time_0))) % on(block_1, table, s(time_0)) % on(block_1, table, time_0) % on(block_5, block_4, s(s(s(s(time_0))))) % on(block_5, block_4, time_0) % on(block_5, table, s(s(s(s(s(time_0)))))) % on(block_5, block_3, s(s(s(time_0)))) % on(block_5, block_3, s(s(time_0))) % on(block_5, block_3, s(time_0)) % on(block_2, block_1, s(s(s(s(s(time_0)))))) % on(block_2, block_1, s(s(s(s(time_0))))) % on(block_2, block_1, s(s(s(time_0)))) % on(block_2, block_1, s(s(time_0))) % on(block_2, block_1, s(time_0)) % on(block_2, block_1, time_0) % on(block_3, block_2, s(s(s(s(s(time_0)))))) % on(block_3, block_2, s(s(s(s(time_0))))) % on(block_3, block_2, s(s(s(time_0)))) % on(block_3, block_2, s(s(time_0))) % on(block_3, block_2, s(time_0)) % on(block_3, block_2, time_0) % source(block_4, s(s(s(s(time_0))))) % source(block_4, time_0) % source(block_5, s(s(time_0))) % source(table, s(time_0)) % source(block_3, s(s(s(time_0)))) % time(s(s(s(s(time_0))))) % time(s(s(s(time_0)))) % time(s(s(time_0))) % time(s(time_0)) % time(time_0) % true % END OF MODEL % EOF %------------------------------------------------------------------------------