%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : PLA025+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 : n031.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 22.37s % Output : Model 22.37s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : PLA025+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 : n031.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:39:16 CDT 2014 % % CPUTime : 22.37 % 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_8) % a_block(block_1) % a_block(block_5) % a_block(block_9) % a_block(block_2) % a_block(block_6) % a_block(table) % a_block(block_3) % a_block(block_7) % clear(block_4, s(s(s(s(s(s(s(time_0)))))))) % clear(block_4, s(s(s(s(s(s(time_0))))))) % clear(block_4, s(s(s(s(s(time_0)))))) % clear(block_4, 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(s(s(time_0)))))))) % clear(block_5, s(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_9, s(s(s(s(s(s(s(time_0)))))))) % clear(block_9, s(s(s(s(s(time_0)))))) % clear(block_9, s(s(s(s(time_0))))) % clear(block_9, s(s(time_0))) % clear(block_9, s(time_0)) % clear(block_9, time_0) % clear(block_3, time_0) % destination(block_5, s(s(s(s(time_0))))) % destination(block_5, s(time_0)) % destination(block_9, s(s(s(s(s(time_0)))))) % destination(block_9, s(s(time_0))) % destination(table, s(s(s(s(s(s(time_0))))))) % destination(table, s(s(s(time_0)))) % destination(block_3, time_0) % different(block_4, block_8) % different(block_4, block_5) % different(block_4, block_9) % different(block_4, block_6) % different(block_4, table) % different(block_4, block_7) % different(block_8, block_9) % different(block_8, table) % different(block_1, block_4) % different(block_1, block_8) % different(block_1, block_5) % different(block_1, block_9) % different(block_1, block_2) % different(block_1, block_6) % different(block_1, table) % different(block_1, block_3) % different(block_1, block_7) % different(block_5, block_8) % different(block_5, block_9) % different(block_5, block_6) % different(block_5, table) % different(block_5, block_7) % different(block_9, table) % different(block_2, block_4) % different(block_2, block_8) % different(block_2, block_5) % different(block_2, block_9) % different(block_2, block_6) % different(block_2, table) % different(block_2, block_3) % different(block_2, block_7) % different(block_6, block_8) % different(block_6, block_9) % different(block_6, table) % different(block_6, block_7) % different(block_3, block_4) % different(block_3, block_8) % different(block_3, block_5) % different(block_3, block_9) % different(block_3, block_6) % different(block_3, table) % different(block_3, block_7) % different(block_7, block_8) % different(block_7, block_9) % different(block_7, table) % fixed(table) % goal_time(s(s(s(s(s(s(time_0))))))) % goal_time(sK0) % neq(block_4, block_8) % neq(block_4, block_1) % neq(block_4, block_5) % neq(block_4, block_9) % neq(block_4, block_2) % neq(block_4, block_6) % neq(block_4, table) % neq(block_4, block_3) % neq(block_4, block_7) % neq(block_8, block_4) % neq(block_8, block_1) % neq(block_8, block_5) % neq(block_8, block_9) % neq(block_8, block_2) % neq(block_8, block_6) % neq(block_8, table) % neq(block_8, block_3) % neq(block_8, block_7) % neq(block_1, block_4) % neq(block_1, block_8) % neq(block_1, block_5) % neq(block_1, block_9) % neq(block_1, block_2) % neq(block_1, block_6) % neq(block_1, table) % neq(block_1, block_3) % neq(block_1, block_7) % neq(block_5, block_4) % neq(block_5, block_8) % neq(block_5, block_1) % neq(block_5, block_9) % neq(block_5, block_2) % neq(block_5, block_6) % neq(block_5, table) % neq(block_5, block_3) % neq(block_5, block_7) % neq(block_9, block_4) % neq(block_9, block_8) % neq(block_9, block_1) % neq(block_9, block_5) % neq(block_9, block_2) % neq(block_9, block_6) % neq(block_9, table) % neq(block_9, block_3) % neq(block_9, block_7) % neq(block_2, block_4) % neq(block_2, block_8) % neq(block_2, block_1) % neq(block_2, block_5) % neq(block_2, block_9) % neq(block_2, block_6) % neq(block_2, table) % neq(block_2, block_3) % neq(block_2, block_7) % neq(block_6, block_4) % neq(block_6, block_8) % neq(block_6, block_1) % neq(block_6, block_5) % neq(block_6, block_9) % neq(block_6, block_2) % neq(block_6, table) % neq(block_6, block_3) % neq(block_6, block_7) % neq(table, block_4) % neq(table, block_8) % neq(table, block_1) % neq(table, block_5) % neq(table, block_9) % neq(table, block_2) % neq(table, block_6) % neq(table, block_3) % neq(table, block_7) % neq(block_3, block_4) % neq(block_3, block_8) % neq(block_3, block_1) % neq(block_3, block_5) % neq(block_3, block_9) % neq(block_3, block_2) % neq(block_3, block_6) % neq(block_3, table) % neq(block_3, block_7) % neq(block_7, block_4) % neq(block_7, block_8) % neq(block_7, block_1) % neq(block_7, block_5) % neq(block_7, block_9) % neq(block_7, block_2) % neq(block_7, block_6) % neq(block_7, table) % neq(block_7, block_3) % nonfixed(block_4) % nonfixed(block_8) % nonfixed(block_1) % nonfixed(block_5) % nonfixed(block_9) % nonfixed(block_2) % nonfixed(block_6) % nonfixed(block_3) % nonfixed(block_7) % object(block_4, s(s(s(s(s(s(time_0))))))) % object(block_4, s(s(s(s(s(time_0)))))) % object(block_4, s(s(s(s(time_0))))) % object(block_4, s(s(s(time_0)))) % object(block_4, s(s(time_0))) % object(block_4, s(time_0)) % object(block_5, time_0) % on(block_4, block_5, s(s(s(s(s(time_0)))))) % on(block_4, block_5, s(s(time_0))) % on(block_4, block_9, s(s(s(s(s(s(time_0))))))) % on(block_4, block_9, s(s(s(time_0)))) % on(block_4, table, s(s(s(s(s(s(s(time_0)))))))) % on(block_4, table, s(s(s(s(time_0))))) % on(block_4, table, s(time_0)) % on(block_4, table, time_0) % on(block_8, block_7, s(s(s(s(s(s(s(time_0)))))))) % on(block_8, block_7, s(s(s(s(s(s(time_0))))))) % on(block_8, block_7, s(s(s(s(s(time_0)))))) % on(block_8, block_7, s(s(s(s(time_0))))) % on(block_8, block_7, s(s(s(time_0)))) % on(block_8, block_7, s(s(time_0))) % on(block_8, block_7, s(time_0)) % on(block_8, block_7, time_0) % on(block_1, table, s(s(s(s(s(s(s(time_0)))))))) % on(block_1, table, s(s(s(s(s(s(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, time_0) % on(block_5, block_3, s(s(s(s(s(s(s(time_0)))))))) % on(block_5, block_3, s(s(s(s(s(s(time_0))))))) % on(block_5, block_3, s(s(s(s(s(time_0)))))) % on(block_5, block_3, 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_9, block_8, s(s(s(s(s(s(s(time_0)))))))) % on(block_9, block_8, s(s(s(s(s(s(time_0))))))) % on(block_9, block_8, s(s(s(s(s(time_0)))))) % on(block_9, block_8, s(s(s(s(time_0))))) % on(block_9, block_8, s(s(s(time_0)))) % on(block_9, block_8, s(s(time_0))) % on(block_9, block_8, s(time_0)) % on(block_9, block_8, time_0) % on(block_2, block_1, s(s(s(s(s(s(s(time_0)))))))) % on(block_2, block_1, s(s(s(s(s(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_6, table, s(s(s(s(s(s(s(time_0)))))))) % on(block_6, table, s(s(s(s(s(s(time_0))))))) % on(block_6, table, s(s(s(s(s(time_0)))))) % on(block_6, table, s(s(s(s(time_0))))) % on(block_6, table, s(s(s(time_0)))) % on(block_6, table, s(s(time_0))) % on(block_6, table, s(time_0)) % on(block_6, table, time_0) % on(block_3, block_2, s(s(s(s(s(s(s(time_0)))))))) % on(block_3, block_2, s(s(s(s(s(s(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) % on(block_7, block_6, s(s(s(s(s(s(s(time_0)))))))) % on(block_7, block_6, s(s(s(s(s(s(time_0))))))) % on(block_7, block_6, s(s(s(s(s(time_0)))))) % on(block_7, block_6, s(s(s(s(time_0))))) % on(block_7, block_6, s(s(s(time_0)))) % on(block_7, block_6, s(s(time_0))) % on(block_7, block_6, s(time_0)) % on(block_7, block_6, time_0) % source(block_4, time_0) % source(block_5, s(s(s(s(s(time_0)))))) % source(block_5, s(s(time_0))) % source(block_9, s(s(s(s(s(s(time_0))))))) % source(block_9, s(s(s(time_0)))) % source(table, s(s(s(s(time_0))))) % source(table, s(time_0)) % time(s(s(s(s(s(s(time_0))))))) % time(s(s(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 %------------------------------------------------------------------------------