%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : GRA021+1 : TPTP v6.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n022.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:00:51 EDT 2014 % Result : CounterSatisfiable 6.52s % Output : Model 6.52s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : GRA021+1 : TPTP v6.1.0. Released v3.2.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n022.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:27:01 CDT 2014 % % CPUTime : 6.52 % E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % % % Defaulting to tptp format. % Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % % % % Proving ... % % % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % green(n2, n6) % green(n2, n10) % green(n2, n3) % green(n2, n11) % green(n2, n5) % green(n6, n11) % green(n7, n8) % green(n7, n9) % green(n3, n10) % green(n3, n11) % green(n3, n12) % green(n3, n9) % green(n4, n7) % green(n4, n11) % green(n4, n8) % green(n4, n12) % green(n4, n5) % green(n4, n9) % green(n8, n12) % green(n8, n9) % green(n5, n6) % green(n5, n10) % green(n5, n7) % green(n5, n11) % green(n5, n8) % green(n9, n11) % green(n1, n7) % green(n1, n11) % green(n1, n4) % green(n1, n12) % green(n1, n9) % less_than(n2, n6) % less_than(n2, n10) % less_than(n2, n3) % less_than(n2, n7) % less_than(n2, n11) % less_than(n2, n4) % less_than(n2, n8) % less_than(n2, n12) % less_than(n2, n5) % less_than(n2, n9) % less_than(n6, n10) % less_than(n6, n7) % less_than(n6, n11) % less_than(n6, n8) % less_than(n6, n12) % less_than(n6, n9) % less_than(n10, n11) % less_than(n10, n12) % less_than(n3, n6) % less_than(n3, n10) % less_than(n3, n7) % less_than(n3, n11) % less_than(n3, n4) % less_than(n3, n8) % less_than(n3, n12) % less_than(n3, n5) % less_than(n3, n9) % less_than(n7, n10) % less_than(n7, n11) % less_than(n7, n8) % less_than(n7, n12) % less_than(n7, n9) % less_than(n11, n12) % less_than(n4, n6) % less_than(n4, n10) % less_than(n4, n7) % less_than(n4, n11) % less_than(n4, n8) % less_than(n4, n12) % less_than(n4, n5) % less_than(n4, n9) % less_than(n8, n10) % less_than(n8, n11) % less_than(n8, n12) % less_than(n8, n9) % less_than(n1, n2) % less_than(n1, n6) % less_than(n1, n10) % less_than(n1, n3) % less_than(n1, n7) % less_than(n1, n11) % less_than(n1, n4) % less_than(n1, n8) % less_than(n1, n12) % less_than(n1, n5) % less_than(n1, n9) % less_than(n5, n6) % less_than(n5, n10) % less_than(n5, n7) % less_than(n5, n11) % less_than(n5, n8) % less_than(n5, n12) % less_than(n5, n9) % less_than(n9, n10) % less_than(n9, n11) % less_than(n9, n12) % red(n6, n10) % red(n6, n7) % red(n6, n8) % red(n6, n12) % red(n6, n9) % red(n10, n11) % red(n10, n12) % red(n2, n7) % red(n2, n4) % red(n2, n8) % red(n2, n12) % red(n2, n9) % red(n3, n6) % red(n3, n7) % red(n3, n4) % red(n3, n8) % red(n3, n5) % red(n11, n12) % red(n7, n10) % red(n7, n11) % red(n7, n12) % red(n4, n6) % red(n4, n10) % red(n8, n10) % red(n8, n11) % red(n1, n2) % red(n1, n6) % red(n1, n10) % red(n1, n3) % red(n1, n8) % red(n1, n5) % red(n9, n10) % red(n9, n12) % red(n5, n12) % red(n5, n9) % END OF MODEL % EOF %------------------------------------------------------------------------------