%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : PUZ131+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 12:30:58 PM UTC 2026
% Result : Theorem 0.59s 0.53s
% Output : Proof 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ131+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:45:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.53 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
% 0.59/0.53
% 0.59/0.53 % SZS status Theorem
% 0.59/0.53
% 0.59/0.54 % SZS output start Proof
% 0.59/0.54 Axiom 1 (csc410_type): course(csc410) = true.
% 0.59/0.54 Axiom 2 (victor_type): professor(victor) = true.
% 0.59/0.54 Axiom 3 (michael_type): student(michael) = true.
% 0.59/0.54 Axiom 4 (victor_coordinator_csc410_axiom): coordinatorof(csc410) = victor.
% 0.59/0.54 Axiom 5 (michael_enrolled_csc410_axiom): enrolled(michael, csc410) = true.
% 0.59/0.54 Axiom 6 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 0.59/0.54 Axiom 7 (coordinator_teaches): ifeq(course(X), true, teaches(coordinatorof(X), X), true) = true.
% 0.59/0.54 Axiom 8 (student_enrolled_taught): ifeq(teaches(X, Y), true, ifeq(enrolled(Z, Y), true, ifeq(course(Y), true, ifeq(professor(X), true, ifeq(student(Z), true, taughtby(Z, X), true), true), true), true), true) = true.
% 0.59/0.54
% 0.59/0.54 Goal 1 (teaching_conjecture): taughtby(michael, victor) = true.
% 0.59/0.54 Proof:
% 0.59/0.54 taughtby(michael, victor)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) R->L }
% 0.59/0.54 ifeq(true, true, taughtby(michael, victor), true)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) R->L }
% 0.59/0.54 ifeq(true, true, ifeq(true, true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 7 (coordinator_teaches) R->L }
% 0.59/0.54 ifeq(ifeq(course(csc410), true, teaches(coordinatorof(csc410), csc410), true), true, ifeq(true, true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 1 (csc410_type) }
% 0.59/0.54 ifeq(ifeq(true, true, teaches(coordinatorof(csc410), csc410), true), true, ifeq(true, true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) }
% 0.59/0.54 ifeq(teaches(coordinatorof(csc410), csc410), true, ifeq(true, true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 4 (victor_coordinator_csc410_axiom) }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(true, true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 2 (victor_type) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(professor(victor), true, taughtby(michael, victor), true), true)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(professor(victor), true, ifeq(true, true, taughtby(michael, victor), true), true), true)
% 0.59/0.54 = { by axiom 3 (michael_type) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(professor(victor), true, ifeq(student(michael), true, taughtby(michael, victor), true), true), true)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(true, true, ifeq(professor(victor), true, ifeq(student(michael), true, taughtby(michael, victor), true), true), true), true)
% 0.59/0.54 = { by axiom 1 (csc410_type) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(course(csc410), true, ifeq(professor(victor), true, ifeq(student(michael), true, taughtby(michael, victor), true), true), true), true)
% 0.59/0.54 = { by axiom 6 (ifeq_axiom) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(true, true, ifeq(course(csc410), true, ifeq(professor(victor), true, ifeq(student(michael), true, taughtby(michael, victor), true), true), true), true), true)
% 0.59/0.54 = { by axiom 5 (michael_enrolled_csc410_axiom) R->L }
% 0.59/0.54 ifeq(teaches(victor, csc410), true, ifeq(enrolled(michael, csc410), true, ifeq(course(csc410), true, ifeq(professor(victor), true, ifeq(student(michael), true, taughtby(michael, victor), true), true), true), true), true)
% 0.59/0.54 = { by axiom 8 (student_enrolled_taught) }
% 0.59/0.54 true
% 0.59/0.54 % SZS output end Proof
% 0.59/0.54
% 0.59/0.54 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------