%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : COM004-1 : TPTP v8.1.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n010.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 : 600s % DateTime : Fri Jul 15 01:33:15 EDT 2022 % Result : Unsatisfiable 1.44s 1.54s % Output : Proof 1.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : COM004-1 : TPTP v8.1.0. Released v1.1.0. % 0.12/0.13 % Command : moca.sh %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Jun 16 19:30:53 EDT 2022 % 0.12/0.34 % CPUTime : % 1.44/1.54 % SZS status Unsatisfiable % 1.44/1.54 % SZS output start Proof % 1.44/1.54 The input problem is unsatisfiable because % 1.44/1.54 % 1.44/1.54 [1] the following set of Horn clauses is unsatisfiable: % 1.44/1.54 % 1.44/1.54 failure_node(X, or(C, P)) & failure_node(Y, or(D, Q)) & contradictory(P, Q) & siblings(X, Y) ==> failure_node(parent_of(X, Y), or(C, D)) % 1.44/1.54 contradictory(negate(X), X) % 1.44/1.54 contradictory(X, negate(X)) % 1.44/1.54 siblings(left_child_of(X), right_child_of(X)) % 1.44/1.54 failure_node(n_left, or(empty, atom)) % 1.44/1.54 failure_node(n_right, or(empty, negate(atom))) % 1.44/1.54 n_left = left_child_of(n) % 1.44/1.54 n_right = right_child_of(n) % 1.44/1.54 failure_node(Z, or(empty, empty)) ==> \bottom % 1.44/1.54 % 1.44/1.54 This holds because % 1.44/1.54 % 1.44/1.54 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 1.44/1.54 % 1.44/1.54 E: % 1.44/1.54 contradictory(X, negate(X)) = true__ % 1.44/1.54 contradictory(negate(X), X) = true__ % 1.44/1.54 f1(true__, X, Y, C, D) = failure_node(parent_of(X, Y), or(C, D)) % 1.44/1.54 f2(true__, X, C, P, Y, D) = f1(failure_node(X, or(C, P)), X, Y, C, D) % 1.44/1.54 f3(true__, Y, D, Q, X, C, P) = f2(failure_node(Y, or(D, Q)), X, C, P, Y, D) % 1.44/1.54 f4(siblings(X, Y), P, Q, Y, D, X, C) = true__ % 1.44/1.54 f4(true__, P, Q, Y, D, X, C) = f3(contradictory(P, Q), Y, D, Q, X, C, P) % 1.44/1.54 f5(failure_node(Z, or(empty, empty))) = true__ % 1.44/1.54 f5(true__) = false__ % 1.44/1.54 failure_node(n_left, or(empty, atom)) = true__ % 1.44/1.54 failure_node(n_right, or(empty, negate(atom))) = true__ % 1.44/1.54 n_left = left_child_of(n) % 1.44/1.54 n_right = right_child_of(n) % 1.44/1.54 siblings(left_child_of(X), right_child_of(X)) = true__ % 1.44/1.54 G: % 1.44/1.54 true__ = false__ % 1.44/1.54 % 1.44/1.54 This holds because % 1.44/1.54 % 1.44/1.54 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 1.44/1.54 % 1.44/1.54 % 1.44/1.54 contradictory(X, negate(X)) -> true__ % 1.44/1.54 contradictory(negate(X), X) -> true__ % 1.44/1.54 f1(f1(true__, X0, X1, Y1, Y2), parent_of(X0, X1), Y3, Y1, Y4) -> f2(true__, parent_of(X0, X1), Y1, Y2, Y3, Y4) % 1.44/1.54 f1(f2(true__, n_left, empty, atom, Y1, Y3), parent_of(n_left, Y1), Y4, empty, Y5) -> f2(true__, parent_of(n_left, Y1), empty, Y3, Y4, Y5) % 1.44/1.54 f1(f2(true__, n_right, empty, negate(atom), Y1, Y3), parent_of(n_right, Y1), Y4, empty, Y5) -> f2(true__, parent_of(n_right, Y1), empty, Y3, Y4, Y5) % 1.44/1.54 f1(failure_node(X, or(C, P)), X, Y, C, D) -> f2(true__, X, C, P, Y, D) % 1.44/1.54 f1(true__, n_left, Y3, empty, Y4) -> f2(true__, n_left, empty, atom, Y3, Y4) % 1.44/1.54 f1(true__, n_right, Y3, empty, Y4) -> f2(true__, n_right, empty, negate(atom), Y3, Y4) % 1.44/1.54 f2(f1(true__, X0, X1, Y1, Y2), Y3, Y4, Y5, parent_of(X0, X1), Y1) -> f3(true__, parent_of(X0, X1), Y1, Y2, Y3, Y4, Y5) % 1.44/1.54 f2(f2(true__, n_left, empty, atom, Y1, Y3), Y4, Y5, Y6, parent_of(n_left, Y1), empty) -> f3(true__, parent_of(n_left, Y1), empty, Y3, Y4, Y5, Y6) % 1.44/1.54 f2(failure_node(Y, or(D, Q)), X, C, P, Y, D) -> f3(true__, Y, D, Q, X, C, P) % 1.44/1.54 f2(true__, Y3, Y4, Y5, n_left, empty) -> f3(true__, n_left, empty, atom, Y3, Y4, Y5) % 1.44/1.54 f2(true__, Y3, Y4, Y5, n_right, empty) -> f3(true__, n_right, empty, negate(atom), Y3, Y4, Y5) % 1.44/1.54 f3(contradictory(P, Q), Y, D, Q, X, C, P) -> f4(true__, P, Q, Y, D, X, C) % 1.44/1.54 f3(true__, Y2, Y3, Y1, Y4, Y5, negate(Y1)) -> f4(true__, negate(Y1), Y1, Y2, Y3, Y4, Y5) % 1.44/1.54 f3(true__, Y2, Y3, negate(Y0), Y4, Y5, Y0) -> f4(true__, Y0, negate(Y0), Y2, Y3, Y4, Y5) % 1.44/1.54 f4(siblings(X, Y), P, Q, Y, D, X, C) -> true__ % 1.44/1.54 f4(true__, Y0, Y1, n_right, Y3, n_left, Y4) -> true__ % 1.44/1.54 f4(true__, Y2, Y3, right_child_of(X0), Y4, left_child_of(X0), Y5) -> true__ % 1.44/1.54 f5(f1(true__, X0, X1, empty, empty)) -> true__ % 1.44/1.54 f5(f2(true__, n_left, empty, atom, Y1, empty)) -> true__ % 1.44/1.54 f5(f2(true__, n_right, empty, negate(atom), Y1, empty)) -> true__ % 1.44/1.54 f5(f3(true__, n_left, empty, atom, n_left, empty, atom)) -> true__ % 1.44/1.54 f5(f3(true__, n_right, empty, negate(atom), n_right, empty, negate(atom))) -> true__ % 1.44/1.54 f5(f4(true__, negate(atom), atom, n_left, empty, n_right, empty)) -> true__ % 1.44/1.54 f5(failure_node(Z, or(empty, empty))) -> true__ % 1.44/1.54 f5(true__) -> false__ % 1.44/1.54 failure_node(n_left, or(empty, atom)) -> true__ % 1.44/1.54 failure_node(n_right, or(empty, negate(atom))) -> true__ % 1.44/1.54 failure_node(parent_of(X, Y), or(C, D)) -> f1(true__, X, Y, C, D) % 1.44/1.54 false__ -> true__ % 1.44/1.54 left_child_of(n) -> n_left % 1.44/1.54 right_child_of(n) -> n_right % 1.44/1.54 siblings(left_child_of(X), right_child_of(X)) -> true__ % 1.44/1.54 siblings(n_left, n_right) -> true__ % 1.44/1.54 with the LPO induced by % 1.44/1.54 f5 > empty > right_child_of > n_right > left_child_of > n_left > n > atom > negate > siblings > failure_node > f1 > f2 > f3 > f4 > contradictory > or > parent_of > false__ > true__ % 1.44/1.54 % 1.44/1.54 % SZS output end Proof % 1.44/1.54 %------------------------------------------------------------------------------