%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 11:42:48 AM UTC 2026
% Result : Unsatisfiable 10.89s 1.86s
% Output : Proof 10.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 13:55:46 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.89/1.86 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-every 2
% 10.89/1.86
% 10.89/1.86 % SZS status Unsatisfiable
% 10.89/1.86
% 10.89/1.88 % SZS output start Proof
% 10.89/1.88 Axiom 1 (commutativity_of_meet): meet(X, Y) = meet(Y, X).
% 10.89/1.88 Axiom 2 (x_meet_0): meet(X, n0) = n0.
% 10.89/1.88 Axiom 3 (commutativity_of_join): join(X, Y) = join(Y, X).
% 10.89/1.88 Axiom 4 (x_join_0): join(X, n0) = X.
% 10.89/1.88 Axiom 5 (absorption1): meet(X, join(X, Y)) = X.
% 10.89/1.88 Axiom 6 (r1_complement_join_a_b_2): meet(r1, join(a, b)) = n0.
% 10.89/1.88 Axiom 7 (r2_complement_meet_a_b_2): meet(r2, meet(a, b)) = n0.
% 10.89/1.88 Axiom 8 (associativity_of_meet): meet(meet(X, Y), Z) = meet(X, meet(Y, Z)).
% 10.89/1.88 Axiom 9 (absorption2): join(X, meet(X, Y)) = X.
% 10.89/1.88 Axiom 10 (define_b2): join(r1, meet(a, r2)) = b2.
% 10.89/1.88 Axiom 11 (define_a2): join(r1, meet(b, r2)) = a2.
% 10.89/1.88 Axiom 12 (associativity_of_join): join(join(X, Y), Z) = join(X, join(Y, Z)).
% 10.89/1.88 Axiom 13 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 10.89/1.88 Axiom 14 (modular): ifeq(meet(X, Y), X, meet(Y, join(X, Z)), join(X, meet(Z, Y))) = join(X, meet(Z, Y)).
% 10.89/1.88
% 10.89/1.88 Lemma 15: meet(X, meet(Y, Z)) = meet(Y, meet(X, Z)).
% 10.89/1.88 Proof:
% 10.89/1.88 meet(X, meet(Y, Z))
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.88 meet(meet(Y, Z), X)
% 10.89/1.88 = { by axiom 8 (associativity_of_meet) }
% 10.89/1.88 meet(Y, meet(Z, X))
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.88 meet(Y, meet(X, Z))
% 10.89/1.88
% 10.89/1.88 Lemma 16: meet(X, join(Y, X)) = X.
% 10.89/1.88 Proof:
% 10.89/1.88 meet(X, join(Y, X))
% 10.89/1.88 = { by axiom 3 (commutativity_of_join) R->L }
% 10.89/1.88 meet(X, join(X, Y))
% 10.89/1.88 = { by axiom 5 (absorption1) }
% 10.89/1.88 X
% 10.89/1.88
% 10.89/1.88 Lemma 17: meet(Y, meet(Z, X)) = meet(X, meet(Y, Z)).
% 10.89/1.88 Proof:
% 10.89/1.88 meet(Y, meet(Z, X))
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.88 meet(meet(Z, X), Y)
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.88 meet(meet(X, Z), Y)
% 10.89/1.88 = { by axiom 8 (associativity_of_meet) }
% 10.89/1.88 meet(X, meet(Z, Y))
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.88 meet(X, meet(Y, Z))
% 10.89/1.88
% 10.89/1.88 Lemma 18: meet(X, meet(Y, join(X, Z))) = meet(X, Y).
% 10.89/1.88 Proof:
% 10.89/1.88 meet(X, meet(Y, join(X, Z)))
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.88 meet(X, meet(join(X, Z), Y))
% 10.89/1.88 = { by axiom 8 (associativity_of_meet) R->L }
% 10.89/1.88 meet(meet(X, join(X, Z)), Y)
% 10.89/1.88 = { by axiom 5 (absorption1) }
% 10.89/1.88 meet(X, Y)
% 10.89/1.88
% 10.89/1.88 Lemma 19: meet(X, meet(Y, join(Z, X))) = meet(X, Y).
% 10.89/1.88 Proof:
% 10.89/1.88 meet(X, meet(Y, join(Z, X)))
% 10.89/1.88 = { by lemma 15 R->L }
% 10.89/1.88 meet(Y, meet(X, join(Z, X)))
% 10.89/1.88 = { by lemma 16 }
% 10.89/1.88 meet(Y, X)
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.88 meet(X, Y)
% 10.89/1.88
% 10.89/1.88 Lemma 20: join(X, join(Y, meet(X, Z))) = join(X, Y).
% 10.89/1.88 Proof:
% 10.89/1.88 join(X, join(Y, meet(X, Z)))
% 10.89/1.88 = { by axiom 3 (commutativity_of_join) R->L }
% 10.89/1.88 join(X, join(meet(X, Z), Y))
% 10.89/1.88 = { by axiom 12 (associativity_of_join) R->L }
% 10.89/1.88 join(join(X, meet(X, Z)), Y)
% 10.89/1.88 = { by axiom 9 (absorption2) }
% 10.89/1.88 join(X, Y)
% 10.89/1.88
% 10.89/1.88 Lemma 21: meet(a2, meet(X, join(b, r1))) = meet(X, a2).
% 10.89/1.88 Proof:
% 10.89/1.88 meet(a2, meet(X, join(b, r1)))
% 10.89/1.88 = { by lemma 20 R->L }
% 10.89/1.88 meet(a2, meet(X, join(b, join(r1, meet(b, r2)))))
% 10.89/1.88 = { by axiom 11 (define_a2) }
% 10.89/1.88 meet(a2, meet(X, join(b, a2)))
% 10.89/1.88 = { by lemma 19 }
% 10.89/1.88 meet(a2, X)
% 10.89/1.88 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.88 meet(X, a2)
% 10.89/1.88
% 10.89/1.88 Lemma 22: ifeq(meet(X, join(a, b)), X, meet(join(X, r1), join(a, b)), X) = X.
% 10.89/1.88 Proof:
% 10.89/1.88 ifeq(meet(X, join(a, b)), X, meet(join(X, r1), join(a, b)), X)
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 ifeq(meet(X, join(a, b)), X, meet(join(a, b), join(X, r1)), X)
% 10.89/1.89 = { by axiom 4 (x_join_0) R->L }
% 10.89/1.89 ifeq(meet(X, join(a, b)), X, meet(join(a, b), join(X, r1)), join(X, n0))
% 10.89/1.89 = { by axiom 6 (r1_complement_join_a_b_2) R->L }
% 10.89/1.89 ifeq(meet(X, join(a, b)), X, meet(join(a, b), join(X, r1)), join(X, meet(r1, join(a, b))))
% 10.89/1.89 = { by axiom 14 (modular) }
% 10.89/1.89 join(X, meet(r1, join(a, b)))
% 10.89/1.89 = { by axiom 6 (r1_complement_join_a_b_2) }
% 10.89/1.89 join(X, n0)
% 10.89/1.89 = { by axiom 4 (x_join_0) }
% 10.89/1.89 X
% 10.89/1.89
% 10.89/1.89 Lemma 23: meet(join(a, b), join(b, r1)) = b.
% 10.89/1.89 Proof:
% 10.89/1.89 meet(join(a, b), join(b, r1))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 meet(join(b, r1), join(a, b))
% 10.89/1.89 = { by axiom 13 (ifeq_axiom) R->L }
% 10.89/1.89 ifeq(b, b, meet(join(b, r1), join(a, b)), b)
% 10.89/1.89 = { by lemma 16 R->L }
% 10.89/1.89 ifeq(meet(b, join(a, b)), b, meet(join(b, r1), join(a, b)), b)
% 10.89/1.89 = { by lemma 22 }
% 10.89/1.89 b
% 10.89/1.89
% 10.89/1.89 Goal 1 (prove_SAMs_lemma): meet(a2, b2) = r1.
% 10.89/1.89 Proof:
% 10.89/1.89 meet(a2, b2)
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.89 meet(b2, a2)
% 10.89/1.89 = { by lemma 18 R->L }
% 10.89/1.89 meet(b2, meet(a2, join(b2, a)))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 meet(b2, meet(join(b2, a), a2))
% 10.89/1.89 = { by lemma 17 R->L }
% 10.89/1.89 meet(join(b2, a), meet(a2, b2))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.89 meet(meet(a2, b2), join(b2, a))
% 10.89/1.89 = { by axiom 3 (commutativity_of_join) }
% 10.89/1.89 meet(meet(a2, b2), join(a, b2))
% 10.89/1.89 = { by axiom 10 (define_b2) R->L }
% 10.89/1.89 meet(meet(a2, b2), join(a, join(r1, meet(a, r2))))
% 10.89/1.89 = { by lemma 20 }
% 10.89/1.89 meet(meet(a2, b2), join(a, r1))
% 10.89/1.89 = { by axiom 3 (commutativity_of_join) R->L }
% 10.89/1.89 meet(meet(a2, b2), join(r1, a))
% 10.89/1.89 = { by axiom 13 (ifeq_axiom) R->L }
% 10.89/1.89 ifeq(r1, r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 5 (absorption1) R->L }
% 10.89/1.89 ifeq(meet(r1, join(r1, meet(a, r2))), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 10 (define_b2) }
% 10.89/1.89 ifeq(meet(r1, b2), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 ifeq(meet(b2, r1), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 5 (absorption1) R->L }
% 10.89/1.89 ifeq(meet(b2, meet(r1, join(r1, meet(b, r2)))), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 11 (define_a2) }
% 10.89/1.89 ifeq(meet(b2, meet(r1, a2)), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by lemma 17 R->L }
% 10.89/1.89 ifeq(meet(r1, meet(a2, b2)), r1, meet(meet(a2, b2), join(r1, a)), join(r1, meet(a, meet(a2, b2))))
% 10.89/1.89 = { by axiom 14 (modular) }
% 10.89/1.89 join(r1, meet(a, meet(a2, b2)))
% 10.89/1.89 = { by lemma 17 }
% 10.89/1.89 join(r1, meet(b2, meet(a, a2)))
% 10.89/1.89 = { by lemma 21 R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a2, meet(a, join(b, r1)))))
% 10.89/1.89 = { by lemma 18 R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a2, meet(a, meet(join(b, r1), join(a, b))))))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) }
% 10.89/1.89 join(r1, meet(b2, meet(a2, meet(a, meet(join(a, b), join(b, r1))))))
% 10.89/1.89 = { by lemma 23 }
% 10.89/1.89 join(r1, meet(b2, meet(a2, meet(a, b))))
% 10.89/1.89 = { by lemma 15 }
% 10.89/1.89 join(r1, meet(b2, meet(a, meet(a2, b))))
% 10.89/1.89 = { by lemma 23 R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, meet(a2, meet(join(a, b), join(b, r1))))))
% 10.89/1.89 = { by lemma 21 }
% 10.89/1.89 join(r1, meet(b2, meet(a, meet(join(a, b), a2))))
% 10.89/1.89 = { by axiom 13 (ifeq_axiom) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(b, r2), meet(b, r2), meet(join(a, b), a2), meet(b, r2)))))
% 10.89/1.89 = { by lemma 19 R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(b, meet(r2, join(a, b))), meet(b, r2), meet(join(a, b), a2), meet(b, r2)))))
% 10.89/1.89 = { by axiom 8 (associativity_of_meet) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(meet(b, r2), join(a, b)), meet(b, r2), meet(join(a, b), a2), meet(b, r2)))))
% 10.89/1.89 = { by axiom 11 (define_a2) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(meet(b, r2), join(a, b)), meet(b, r2), meet(join(a, b), join(r1, meet(b, r2))), meet(b, r2)))))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(meet(b, r2), join(a, b)), meet(b, r2), meet(join(r1, meet(b, r2)), join(a, b)), meet(b, r2)))))
% 10.89/1.89 = { by axiom 3 (commutativity_of_join) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(a, ifeq(meet(meet(b, r2), join(a, b)), meet(b, r2), meet(join(meet(b, r2), r1), join(a, b)), meet(b, r2)))))
% 10.89/1.89 = { by lemma 22 }
% 10.89/1.89 join(r1, meet(b2, meet(a, meet(b, r2))))
% 10.89/1.89 = { by axiom 8 (associativity_of_meet) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(meet(a, b), r2)))
% 10.89/1.89 = { by axiom 1 (commutativity_of_meet) R->L }
% 10.89/1.89 join(r1, meet(b2, meet(r2, meet(a, b))))
% 10.89/1.89 = { by axiom 7 (r2_complement_meet_a_b_2) }
% 10.89/1.89 join(r1, meet(b2, n0))
% 10.89/1.89 = { by axiom 2 (x_meet_0) }
% 10.89/1.89 join(r1, n0)
% 10.89/1.89 = { by axiom 4 (x_join_0) }
% 10.89/1.89 r1
% 10.89/1.89 % SZS output end Proof
% 10.89/1.89
% 10.89/1.89 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------