%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : SYO850+1 : TPTP v7.5.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n004.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 : 0s % DateTime : Tue Mar 29 01:53:56 EDT 2022 % Result : CounterSatisfiable 1.82s 2.01s % Output : Model 1.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYO850+1 : TPTP v7.5.0. Released v7.5.0. % 0.06/0.12 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Wed Mar 16 03:45:25 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.12/0.34 % 0.12/0.34 % 0.12/0.34 Defaulting to tptp format. % 0.12/0.34 Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.12/0.34 % 0.12/0.34 % 0.12/0.34 % 0.12/0.36 Proving ... % 0.12/0.36 % 1.82/2.01 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.82/2.01 % 1.82/2.01 START OF MODEL (DIG): % 1.82/2.01 (aun(asm(_0, _1), aint(_0, _1)) = _0) % 1.82/2.01 (aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))) = aun(apow(a2), aint(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), asing(asing(asing(a1)))))) % 1.82/2.01 (asm(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), asing(asing(asing(a1)))) = apow(a2)) % 1.82/2.01 (asm(apow(a2), asing(a1)) = aun(apow(asing(a1)), aint(asm(apow(a2), asing(a1)), asing(a2)))) % 1.82/2.01 (asm(asm(apow(a2), asing(a1)), asing(a2)) = apow(asing(a1))) % 1.82/2.01 aal2(asing(asing(a1))) % 1.82/2.01 aal2(asing(a0)) % 1.82/2.01 aal5(aun(apow(a2), asing(asing(a2)))) % 1.82/2.01 aex3(aint(aun(aun(asing(a2), apow(asing(a2))), asing(asm(a3, asing(a1)))), aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2)))))) % 1.82/2.01 aex3(aint(aun(asing(asing(a1)), aun(asing(asing(a2)), a4)), aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2)))))) % 1.82/2.01 aex4(asm(aun(asing(asing(a2)), a4), asing(a1))) % 1.82/2.01 aex5(aun(asing(asing(asing(a1))), a4)) % 1.82/2.01 ain(a1, aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2))))) % 1.82/2.01 ain(a1, asing(a1)) % 1.82/2.01 ain(a1, asing(apow(asing(a1)))) % 1.82/2.01 ain(asing(a1), aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))) % 1.82/2.01 ain(asing(a2), aun(asing(asing(a2)), aun(a4, asing(apow(a2))))) % 1.82/2.01 ain(a3, a4) % 1.82/2.01 ain(a0, aun(asing(asing(a1)), aun(a4, asing(apow(a2))))) % 1.82/2.01 ain(a0, aun(asing(asing(asing(a1))), aun(a1, asing(apow(a2))))) % 1.82/2.01 ain(a0, asm(a4, asing(a2))) % 1.82/2.01 ain(asm(apow(a2), a2), aun(a3, asing(asm(apow(a2), a2)))) % 1.82/2.01 ain(asm(apow(a2), apow(asing(a2))), asing(asm(apow(a2), apow(asing(a2))))) % 1.82/2.01 asubq(aun(_0, _1), aun(_1, _0)) % 1.82/2.01 asubq(aun(asing(asing(a1)), aun(asing(asing(a2)), a4)), aun(asing(asing(a2)), a4)) % 1.82/2.01 asubq(aun(asing(asing(a2)), a4), aun(asing(asing(a1)), aun(asing(asing(a2)), a4))) % 1.82/2.01 asubq(aun(asing(asing(a2)), a4), a4) % 1.82/2.01 asubq(aun(asing(a0), asing(asm(a3, asing(a1)))), asm(aint(aun(a3, asing(asm(a3, asing(a1)))), apow(asm(a3, asing(a1)))), asing(a1))) % 1.82/2.01 asubq(aun(apow(a2), asing(apow(a2))), apow(a2)) % 1.82/2.01 asubq(aun(aint(_0, _1), asm(_0, _1)), _0) % 1.82/2.01 asubq(aun(aint(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), asing(asing(asing(a1)))), apow(a2)), aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1))))) % 1.82/2.01 asubq(aun(aint(asm(apow(a2), asing(a1)), asing(a2)), apow(asing(a1))), asm(apow(a2), asing(a1))) % 1.82/2.01 asubq(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), aun(aint(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), asing(asing(asing(a1)))), apow(a2))) % 1.82/2.01 asubq(aun(asm(apow(a2), asing(a2)), asing(asm(apow(a2), apow(asing(a2))))), asm(apow(a2), asing(a2))) % 1.82/2.01 asubq(a1, asing(a0)) % 1.82/2.01 asubq(_0, aun(aint(_0, _1), asm(_0, _1))) % 1.82/2.01 asubq(apow(a2), aun(apow(a2), asing(apow(a2)))) % 1.82/2.01 asubq(apow(a2), apow(a2)) % 1.82/2.01 asubq(asing(a2), asm(asm(apow(a2), apow(asing(a1))), asing(a1))) % 1.82/2.01 asubq(asing(a0), a1) % 1.82/2.01 asubq(a4, aun(asing(asing(a2)), a4)) % 1.82/2.01 asubq(a4, a4) % 1.82/2.01 asubq(asm(apow(a2), asing(a1)), aun(aint(asm(apow(a2), asing(a1)), asing(a2)), apow(asing(a1)))) % 1.82/2.01 asubq(asm(apow(a2), asing(a2)), aun(asm(apow(a2), asing(a2)), asing(asm(apow(a2), apow(asing(a2)))))) % 1.82/2.01 asubq(asm(apow(a2), asing(a2)), asm(apow(a2), asing(a2))) % 1.82/2.01 asubq(asm(aint(aun(a3, asing(asm(a3, asing(a1)))), apow(asm(a3, asing(a1)))), asing(a1)), aun(asing(a0), asing(asm(a3, asing(a1))))) % 1.82/2.01 asubq(asm(asm(apow(a2), apow(asing(a1))), asing(a1)), asing(a2)) % 1.82/2.01 END OF MODEL %------------------------------------------------------------------------------