%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:19:23 AM UTC 2026
% Result : Unsatisfiable 2.40s 0.86s
% Output : Proof 2.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n018.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 10:54:08 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.42 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.40/0.86 Command-line arguments: --flatten --complete-subsets
% 2.40/0.86
% 2.40/0.86 % SZS status Unsatisfiable
% 2.40/0.86
% 2.40/0.89 % SZS output start Proof
% 2.40/0.89 Axiom 1 (constructor8): d3 = f3.
% 2.40/0.89 Axiom 2 (constructor9): d1 = not(e1).
% 2.40/0.89 Axiom 3 (constructor10): d2 = not(e2).
% 2.40/0.89 Axiom 4 (constructor3): b1 = not(d1).
% 2.40/0.89 Axiom 5 (constructor4): b2 = not(d2).
% 2.40/0.89 Axiom 6 (not_definition2): not(n1) = n0.
% 2.40/0.89 Axiom 7 (constructor13): f1 = not(i1).
% 2.40/0.89 Axiom 8 (constructor14): f2 = not(i2).
% 2.40/0.89 Axiom 9 (not_simplification): not(not(X)) = X.
% 2.40/0.89 Axiom 10 (and_commutativity): and(X, Y) = and(Y, X).
% 2.40/0.89 Axiom 11 (and_not_simplification1): and(X, not(X)) = n0.
% 2.40/0.89 Axiom 12 (constructor1): a1 = and(b1, b3).
% 2.40/0.89 Axiom 13 (constructor2): a2 = and(b2, b3).
% 2.40/0.89 Axiom 14 (constructor15): f3 = and(i1, i2).
% 2.40/0.89 Axiom 15 (or_commutativity): or(X, Y) = or(Y, X).
% 2.40/0.89 Axiom 16 (or_definition1): or(X, n0) = X.
% 2.40/0.89 Axiom 17 (constructor5): b3 = or(c1, c2).
% 2.40/0.89 Axiom 18 (constructor11): e1 = or(f1, f3).
% 2.40/0.89 Axiom 19 (constructor12): e2 = or(f2, f3).
% 2.40/0.89 Axiom 20 (constructor6): c1 = or(d1, d3).
% 2.40/0.89 Axiom 21 (constructor7): c2 = or(d2, d3).
% 2.40/0.89 Axiom 22 (not_canonicalization1): not(and(X, Y)) = or(not(X), not(Y)).
% 2.40/0.89 Axiom 23 (not_canonicalization2): not(or(X, Y)) = and(not(X), not(Y)).
% 2.40/0.89 Axiom 24 (and_simplification3): and(and(X, Y), X) = and(X, Y).
% 2.40/0.89 Axiom 25 (and_simplification2): and(and(X, Y), Y) = and(X, Y).
% 2.40/0.89 Axiom 26 (or_simplification2): or(or(X, Y), Y) = or(X, Y).
% 2.40/0.89 Axiom 27 (or_associativity): or(X, or(Y, Z)) = or(or(X, Y), Z).
% 2.40/0.89 Axiom 28 (circuit_description): circuit(input(i1, i2), output(a1, a2)) = true.
% 2.40/0.89 Axiom 29 (and_or_not_simplification2): or(and(X, Y), and(Y, not(X))) = Y.
% 2.40/0.89 Axiom 30 (and_or_canonicalization): and(or(X, Y), Z) = or(and(X, Z), and(Y, Z)).
% 2.40/0.89
% 2.40/0.89 Lemma 31: and(i1, i2) = d3.
% 2.40/0.89 Proof:
% 2.40/0.89 and(i1, i2)
% 2.40/0.89 = { by axiom 14 (constructor15) R->L }
% 2.40/0.89 f3
% 2.40/0.89 = { by axiom 1 (constructor8) R->L }
% 2.40/0.89 d3
% 2.40/0.89
% 2.40/0.89 Lemma 32: or(and(i1, i2), not(e2)) = or(d2, d3).
% 2.40/0.89 Proof:
% 2.40/0.89 or(and(i1, i2), not(e2))
% 2.40/0.89 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.89 or(not(e2), and(i1, i2))
% 2.40/0.89 = { by lemma 31 }
% 2.40/0.89 or(not(e2), d3)
% 2.40/0.89 = { by axiom 3 (constructor10) R->L }
% 2.40/0.89 or(d2, d3)
% 2.40/0.89
% 2.40/0.89 Lemma 33: or(f2, f3) = not(d2).
% 2.40/0.89 Proof:
% 2.40/0.89 or(f2, f3)
% 2.40/0.89 = { by axiom 19 (constructor12) R->L }
% 2.40/0.89 e2
% 2.40/0.89 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.89 not(not(e2))
% 2.40/0.89 = { by axiom 3 (constructor10) R->L }
% 2.40/0.89 not(d2)
% 2.40/0.89
% 2.40/0.89 Lemma 34: not(or(f2, f3)) = not(e2).
% 2.40/0.89 Proof:
% 2.40/0.89 not(or(f2, f3))
% 2.40/0.89 = { by lemma 33 }
% 2.40/0.89 not(not(d2))
% 2.40/0.89 = { by axiom 3 (constructor10) }
% 2.40/0.89 not(not(not(e2)))
% 2.40/0.89 = { by axiom 9 (not_simplification) }
% 2.40/0.89 not(e2)
% 2.40/0.89
% 2.40/0.89 Lemma 35: and(i2, not(and(i1, i2))) = not(e2).
% 2.40/0.89 Proof:
% 2.40/0.89 and(i2, not(and(i1, i2)))
% 2.40/0.89 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.89 and(not(and(i1, i2)), i2)
% 2.40/0.89 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.89 and(not(and(i1, i2)), not(not(i2)))
% 2.40/0.89 = { by axiom 23 (not_canonicalization2) R->L }
% 2.40/0.89 not(or(and(i1, i2), not(i2)))
% 2.40/0.89 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.89 not(or(not(i2), and(i1, i2)))
% 2.40/0.89 = { by lemma 31 }
% 2.40/0.89 not(or(not(i2), d3))
% 2.40/0.89 = { by axiom 1 (constructor8) }
% 2.40/0.89 not(or(not(i2), f3))
% 2.40/0.89 = { by axiom 8 (constructor14) R->L }
% 2.40/0.89 not(or(f2, f3))
% 2.40/0.89 = { by lemma 34 }
% 2.40/0.89 not(e2)
% 2.40/0.89
% 2.40/0.89 Lemma 36: or(d2, d3) = i2.
% 2.40/0.89 Proof:
% 2.40/0.89 or(d2, d3)
% 2.40/0.89 = { by lemma 32 R->L }
% 2.40/0.89 or(and(i1, i2), not(e2))
% 2.40/0.89 = { by axiom 25 (and_simplification2) R->L }
% 2.40/0.89 or(and(and(i1, i2), i2), not(e2))
% 2.40/0.89 = { by lemma 35 R->L }
% 2.40/0.89 or(and(and(i1, i2), i2), and(i2, not(and(i1, i2))))
% 2.40/0.89 = { by axiom 29 (and_or_not_simplification2) }
% 2.40/0.89 i2
% 2.40/0.89
% 2.40/0.89 Lemma 37: or(f1, f3) = not(d1).
% 2.40/0.89 Proof:
% 2.40/0.89 or(f1, f3)
% 2.40/0.89 = { by axiom 18 (constructor11) R->L }
% 2.40/0.89 e1
% 2.40/0.89 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.89 not(not(e1))
% 2.40/0.89 = { by axiom 2 (constructor9) R->L }
% 2.40/0.89 not(d1)
% 2.40/0.89
% 2.40/0.89 Lemma 38: or(not(e2), not(or(c1, c2))) = not(and(b2, b3)).
% 2.40/0.89 Proof:
% 2.40/0.89 or(not(e2), not(or(c1, c2)))
% 2.40/0.89 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.89 or(not(or(c1, c2)), not(e2))
% 2.40/0.89 = { by lemma 34 R->L }
% 2.40/0.89 or(not(or(c1, c2)), not(or(f2, f3)))
% 2.40/0.89 = { by axiom 22 (not_canonicalization1) R->L }
% 2.40/0.89 not(and(or(c1, c2), or(f2, f3)))
% 2.40/0.89 = { by lemma 33 }
% 2.40/0.89 not(and(or(c1, c2), not(d2)))
% 2.40/0.89 = { by axiom 17 (constructor5) R->L }
% 2.40/0.89 not(and(b3, not(d2)))
% 2.40/0.89 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.89 not(and(not(d2), b3))
% 2.40/0.89 = { by axiom 5 (constructor4) R->L }
% 2.40/0.89 not(and(b2, b3))
% 2.40/0.89
% 2.40/0.89 Lemma 39: not(or(f1, f3)) = not(e1).
% 2.40/0.89 Proof:
% 2.40/0.89 not(or(f1, f3))
% 2.40/0.89 = { by lemma 37 }
% 2.40/0.89 not(not(d1))
% 2.40/0.89 = { by axiom 2 (constructor9) }
% 2.40/0.89 not(not(not(e1)))
% 2.40/0.89 = { by axiom 9 (not_simplification) }
% 2.40/0.89 not(e1)
% 2.40/0.89
% 2.40/0.89 Lemma 40: or(and(i1, i2), not(i1)) = or(f1, f3).
% 2.40/0.89 Proof:
% 2.40/0.89 or(and(i1, i2), not(i1))
% 2.40/0.89 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.89 or(not(i1), and(i1, i2))
% 2.40/0.89 = { by lemma 31 }
% 2.40/0.89 or(not(i1), d3)
% 2.40/0.89 = { by axiom 1 (constructor8) }
% 2.40/0.89 or(not(i1), f3)
% 2.40/0.89 = { by axiom 7 (constructor13) R->L }
% 2.40/0.89 or(f1, f3)
% 2.40/0.89
% 2.40/0.89 Lemma 41: not(and(b2, b3)) = not(i1).
% 2.40/0.89 Proof:
% 2.40/0.89 not(and(b2, b3))
% 2.40/0.89 = { by lemma 38 R->L }
% 2.40/0.89 or(not(e2), not(or(c1, c2)))
% 2.40/0.89 = { by axiom 23 (not_canonicalization2) }
% 2.40/0.89 or(not(e2), and(not(c1), not(c2)))
% 2.40/0.89 = { by axiom 20 (constructor6) }
% 2.40/0.89 or(not(e2), and(not(or(d1, d3)), not(c2)))
% 2.40/0.89 = { by axiom 21 (constructor7) }
% 2.40/0.89 or(not(e2), and(not(or(d1, d3)), not(or(d2, d3))))
% 2.40/0.89 = { by lemma 36 }
% 2.40/0.89 or(not(e2), and(not(or(d1, d3)), not(i2)))
% 2.40/0.89 = { by axiom 2 (constructor9) }
% 2.40/0.89 or(not(e2), and(not(or(not(e1), d3)), not(i2)))
% 2.40/0.89 = { by lemma 31 R->L }
% 2.40/0.89 or(not(e2), and(not(or(not(e1), and(i1, i2))), not(i2)))
% 2.40/0.89 = { by axiom 15 (or_commutativity) }
% 2.40/0.89 or(not(e2), and(not(or(and(i1, i2), not(e1))), not(i2)))
% 2.40/0.89 = { by axiom 24 (and_simplification3) R->L }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), not(e1))), not(i2)))
% 2.40/0.89 = { by lemma 39 R->L }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), not(or(f1, f3)))), not(i2)))
% 2.40/0.89 = { by lemma 40 R->L }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), not(or(and(i1, i2), not(i1))))), not(i2)))
% 2.40/0.89 = { by axiom 23 (not_canonicalization2) }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), and(not(and(i1, i2)), not(not(i1))))), not(i2)))
% 2.40/0.89 = { by axiom 9 (not_simplification) }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), and(not(and(i1, i2)), i1))), not(i2)))
% 2.40/0.89 = { by axiom 10 (and_commutativity) }
% 2.40/0.89 or(not(e2), and(not(or(and(and(i1, i2), i1), and(i1, not(and(i1, i2))))), not(i2)))
% 2.40/0.89 = { by axiom 29 (and_or_not_simplification2) }
% 2.40/0.89 or(not(e2), and(not(i1), not(i2)))
% 2.40/0.89 = { by lemma 36 R->L }
% 2.40/0.89 or(not(e2), and(not(i1), not(or(d2, d3))))
% 2.40/0.89 = { by lemma 35 R->L }
% 2.40/0.89 or(and(i2, not(and(i1, i2))), and(not(i1), not(or(d2, d3))))
% 2.40/0.89 = { by axiom 10 (and_commutativity) }
% 2.40/0.89 or(and(not(and(i1, i2)), i2), and(not(i1), not(or(d2, d3))))
% 2.40/0.89 = { by lemma 36 R->L }
% 2.40/0.89 or(and(not(and(i1, i2)), or(d2, d3)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 10 (and_commutativity) }
% 2.40/0.90 or(and(or(d2, d3), not(and(i1, i2))), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 22 (not_canonicalization1) }
% 2.40/0.90 or(and(or(d2, d3), or(not(i1), not(i2))), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.90 or(and(or(d2, d3), or(not(i2), not(i1))), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.90 or(and(or(not(i2), not(i1)), or(d2, d3)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by lemma 36 }
% 2.40/0.90 or(and(or(not(i2), not(i1)), i2), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 30 (and_or_canonicalization) }
% 2.40/0.90 or(or(and(not(i2), i2), and(not(i1), i2)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.90 or(or(and(i2, not(i2)), and(not(i1), i2)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 11 (and_not_simplification1) }
% 2.40/0.90 or(or(n0, and(not(i1), i2)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 6 (not_definition2) R->L }
% 2.40/0.90 or(or(not(n1), and(not(i1), i2)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.90 or(or(and(not(i1), i2), not(n1)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 6 (not_definition2) }
% 2.40/0.90 or(or(and(not(i1), i2), n0), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 16 (or_definition1) }
% 2.40/0.90 or(and(not(i1), i2), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by lemma 36 R->L }
% 2.40/0.90 or(and(not(i1), or(d2, d3)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 10 (and_commutativity) }
% 2.40/0.90 or(and(or(d2, d3), not(i1)), and(not(i1), not(or(d2, d3))))
% 2.40/0.90 = { by axiom 29 (and_or_not_simplification2) }
% 2.40/0.90 not(i1)
% 2.40/0.90
% 2.40/0.90 Goal 1 (prove_interchange): circuit(input(i1, i2), output(i2, i1)) = true.
% 2.40/0.90 Proof:
% 2.40/0.90 circuit(input(i1, i2), output(i2, i1))
% 2.40/0.90 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(i2)), i1))
% 2.40/0.90 = { by axiom 29 (and_or_not_simplification2) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(and(or(c1, c2), not(i2)), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(and(not(i2), or(c1, c2)), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(and(not(i2), not(not(or(c1, c2)))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 36 R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(and(not(or(d2, d3)), not(not(or(c1, c2)))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 23 (not_canonicalization2) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(or(d2, d3), not(or(c1, c2)))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 32 R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(or(and(i1, i2), not(e2)), not(or(c1, c2)))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 27 (or_associativity) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(and(i1, i2), or(not(e2), not(or(c1, c2))))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 38 }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(and(i1, i2), not(and(b2, b3)))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 41 }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(and(i1, i2), not(i1))), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 40 }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(f1, f3)), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 39 }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), and(not(i2), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by lemma 36 R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), and(not(or(d2, d3)), not(or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 23 (not_canonicalization2) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), not(or(or(d2, d3), or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 21 (constructor7) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), not(or(c2, or(c1, c2))))), i1))
% 2.40/0.90 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), not(or(or(c1, c2), c2)))), i1))
% 2.40/0.90 = { by axiom 26 (or_simplification2) }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(e1), not(or(c1, c2)))), i1))
% 2.40/0.90 = { by axiom 15 (or_commutativity) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(c1, c2)), not(e1))), i1))
% 2.40/0.90 = { by lemma 39 R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(or(not(or(c1, c2)), not(or(f1, f3)))), i1))
% 2.40/0.90 = { by axiom 22 (not_canonicalization1) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(and(or(c1, c2), or(f1, f3)))), i1))
% 2.40/0.90 = { by lemma 37 }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(and(or(c1, c2), not(d1)))), i1))
% 2.40/0.90 = { by axiom 17 (constructor5) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(and(b3, not(d1)))), i1))
% 2.40/0.90 = { by axiom 10 (and_commutativity) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(and(not(d1), b3))), i1))
% 2.40/0.90 = { by axiom 4 (constructor3) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(not(not(and(b1, b3))), i1))
% 2.40/0.90 = { by axiom 9 (not_simplification) }
% 2.40/0.90 circuit(input(i1, i2), output(and(b1, b3), i1))
% 2.40/0.90 = { by axiom 9 (not_simplification) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(and(b1, b3), not(not(i1))))
% 2.40/0.90 = { by lemma 41 R->L }
% 2.40/0.90 circuit(input(i1, i2), output(and(b1, b3), not(not(and(b2, b3)))))
% 2.40/0.90 = { by axiom 9 (not_simplification) }
% 2.40/0.90 circuit(input(i1, i2), output(and(b1, b3), and(b2, b3)))
% 2.40/0.90 = { by axiom 13 (constructor2) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(and(b1, b3), a2))
% 2.40/0.90 = { by axiom 12 (constructor1) R->L }
% 2.40/0.90 circuit(input(i1, i2), output(a1, a2))
% 2.40/0.90 = { by axiom 28 (circuit_description) }
% 2.40/0.90 true
% 2.40/0.90 % SZS output end Proof
% 2.40/0.90
% 2.40/0.90 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------