%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ131+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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 : 300s
% DateTime : Thu May 9 17:37:49 EDT 2024
% Result : Theorem 3.58s 3.82s
% Output : Refutation 3.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : PUZ131+1 : TPTP v8.1.2. Released v4.1.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 20:43:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 3.58/3.82 % Version: 1.5
% 3.58/3.82 % SZS status Theorem
% 3.58/3.82 % SZS output start CNFRefutation
% 3.58/3.82 fof(teaching_conjecture,conjecture,taughtby(michael,victor),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', teaching_conjecture)).
% 3.58/3.82 fof(c7,negated_conjecture,(~taughtby(michael,victor)),inference(assume_negation,[status(cth)],[teaching_conjecture])).
% 3.58/3.82 fof(c8,negated_conjecture,~taughtby(michael,victor),inference(fof_simplification,[status(thm)],[c7])).
% 3.58/3.82 cnf(c9,negated_conjecture,~taughtby(michael,victor),inference(split_conjunct,[status(thm)],[c8])).
% 3.58/3.82 cnf(reflexivity,axiom,X18=X18,theory(equality)).
% 3.58/3.82 fof(victor_coordinator_csc410_axiom,axiom,coordinatorof(csc410)=victor,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', victor_coordinator_csc410_axiom)).
% 3.58/3.82 cnf(c10,plain,coordinatorof(csc410)=victor,inference(split_conjunct,[status(thm)],[victor_coordinator_csc410_axiom])).
% 3.58/3.82 cnf(c6,axiom,X56!=X55|X54!=X53|~taughtby(X56,X54)|taughtby(X55,X53),theory(equality)).
% 3.58/3.82 fof(michael_type,axiom,student(michael),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', michael_type)).
% 3.58/3.82 cnf(c48,plain,student(michael),inference(split_conjunct,[status(thm)],[michael_type])).
% 3.58/3.82 fof(csc410_type,axiom,course(csc410),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', csc410_type)).
% 3.58/3.82 cnf(c46,plain,course(csc410),inference(split_conjunct,[status(thm)],[csc410_type])).
% 3.58/3.82 fof(michael_enrolled_csc410_axiom,axiom,enrolled(michael,csc410),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', michael_enrolled_csc410_axiom)).
% 3.58/3.82 cnf(c11,plain,enrolled(michael,csc410),inference(split_conjunct,[status(thm)],[michael_enrolled_csc410_axiom])).
% 3.58/3.82 fof(coordinator_of_type,axiom,(![A]:(course(A)=>professor(coordinatorof(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', coordinator_of_type)).
% 3.58/3.82 fof(c43,plain,(![A]:(~course(A)|professor(coordinatorof(A)))),inference(fof_nnf,[status(thm)],[coordinator_of_type])).
% 3.58/3.82 fof(c44,plain,(![X14]:(~course(X14)|professor(coordinatorof(X14)))),inference(variable_rename,[status(thm)],[c43])).
% 3.58/3.82 cnf(c45,plain,~course(X34)|professor(coordinatorof(X34)),inference(split_conjunct,[status(thm)],[c44])).
% 3.58/3.82 cnf(c92,plain,professor(coordinatorof(csc410)),inference(resolution,[status(thm)],[c45, c46])).
% 3.58/3.82 fof(student_enrolled_taught,axiom,(![X]:(![Y]:((student(X)&course(Y))=>(enrolled(X,Y)=>(![Z]:(professor(Z)=>(teaches(Z,Y)=>taughtby(X,Z)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', student_enrolled_taught)).
% 3.58/3.82 fof(c12,plain,(![X]:(![Y]:((~student(X)|~course(Y))|(~enrolled(X,Y)|(![Z]:(~professor(Z)|(~teaches(Z,Y)|taughtby(X,Z)))))))),inference(fof_nnf,[status(thm)],[student_enrolled_taught])).
% 3.58/3.82 fof(c14,plain,(![X2]:(![X3]:(![X4]:((~student(X2)|~course(X3))|(~enrolled(X2,X3)|(~professor(X4)|(~teaches(X4,X3)|taughtby(X2,X4)))))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,(![X2]:(![X3]:((~student(X2)|~course(X3))|(~enrolled(X2,X3)|(![X4]:(~professor(X4)|(~teaches(X4,X3)|taughtby(X2,X4)))))))),inference(variable_rename,[status(thm)],[c12])).])).
% 3.58/3.82 cnf(c15,plain,~student(X58)|~course(X59)|~enrolled(X58,X59)|~professor(X57)|~teaches(X57,X59)|taughtby(X58,X57),inference(split_conjunct,[status(thm)],[c14])).
% 3.58/3.82 fof(coordinator_teaches,axiom,(![X]:(course(X)=>teaches(coordinatorof(X),X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', coordinator_teaches)).
% 3.58/3.82 fof(c16,plain,(![X]:(~course(X)|teaches(coordinatorof(X),X))),inference(fof_nnf,[status(thm)],[coordinator_teaches])).
% 3.58/3.82 fof(c17,plain,(![X5]:(~course(X5)|teaches(coordinatorof(X5),X5))),inference(variable_rename,[status(thm)],[c16])).
% 3.58/3.82 cnf(c18,plain,~course(X60)|teaches(coordinatorof(X60),X60),inference(split_conjunct,[status(thm)],[c17])).
% 3.58/3.82 cnf(c146,plain,teaches(coordinatorof(csc410),csc410),inference(resolution,[status(thm)],[c18, c46])).
% 3.58/3.82 cnf(c150,plain,~student(X73)|~course(csc410)|~enrolled(X73,csc410)|~professor(coordinatorof(csc410))|taughtby(X73,coordinatorof(csc410)),inference(resolution,[status(thm)],[c146, c15])).
% 3.58/3.82 cnf(c458,plain,~student(X198)|~course(csc410)|~enrolled(X198,csc410)|taughtby(X198,coordinatorof(csc410)),inference(resolution,[status(thm)],[c150, c92])).
% 3.58/3.82 cnf(c2651,plain,~student(michael)|~course(csc410)|taughtby(michael,coordinatorof(csc410)),inference(resolution,[status(thm)],[c458, c11])).
% 3.58/3.82 cnf(c2653,plain,~student(michael)|taughtby(michael,coordinatorof(csc410)),inference(resolution,[status(thm)],[c2651, c46])).
% 3.58/3.82 cnf(c2654,plain,taughtby(michael,coordinatorof(csc410)),inference(resolution,[status(thm)],[c2653, c48])).
% 3.58/3.82 cnf(c2655,plain,michael!=X200|coordinatorof(csc410)!=X199|taughtby(X200,X199),inference(resolution,[status(thm)],[c2654, c6])).
% 3.58/3.82 cnf(c2657,plain,michael!=X203|taughtby(X203,victor),inference(resolution,[status(thm)],[c2655, c10])).
% 3.58/3.82 cnf(c2659,plain,taughtby(michael,victor),inference(resolution,[status(thm)],[c2657, reflexivity])).
% 3.58/3.82 cnf(c2660,plain,$false,inference(resolution,[status(thm)],[c2659, c9])).
% 3.58/3.82 % SZS output end CNFRefutation
% 3.58/3.82
% 3.58/3.82 % Initial clauses : 30
% 3.58/3.82 % Processed clauses : 911
% 3.58/3.82 % Factors computed : 1
% 3.58/3.82 % Resolvents computed: 2603
% 3.58/3.82 % Tautologies deleted: 5
% 3.58/3.82 % Forward subsumed : 52
% 3.58/3.82 % Backward subsumed : 4
% 3.58/3.82 % -------- CPU Time ---------
% 3.58/3.82 % User time : 3.434 s
% 3.58/3.82 % System time : 0.014 s
% 3.58/3.82 % Total time : 3.448 s
%------------------------------------------------------------------------------