%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ131+1 : TPTP v8.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n006.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 : Mon Jun 24 13:42:26 EDT 2024 % Result : Theorem 30.84s 30.94s % Output : CNFRefutation 30.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : PUZ131+1 : TPTP v8.2.0. Released v4.1.0. % 0.00/0.07 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.25 % Computer : n006.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Tue Jun 18 10:45:39 EDT 2024 % 0.07/0.25 % CPUTime : % 0.12/0.47 start to proof:theBenchmark % 30.84/30.93 %------------------------------------------- % 30.84/30.93 % File :CSE---1.7 % 30.84/30.93 % Problem :theBenchmark % 30.84/30.93 % Transform :cnf % 30.84/30.93 % Format :tptp:raw % 30.84/30.93 % Command :java -jar mcs_scs.jar %d %s % 30.84/30.93 % 30.84/30.93 % Result :Theorem 30.430000s % 30.84/30.93 % Output :CNFRefutation 30.430000s % 30.84/30.93 %------------------------------------------- % 30.84/30.94 %------------------------------------------------------------------------------ % 30.84/30.94 % File : PUZ131+1 : TPTP v8.2.0. Released v4.1.0. % 30.84/30.94 % Domain : Puzzles % 30.84/30.94 % Problem : Victor teaches Michael % 30.84/30.94 % Version : Especial. % 30.84/30.94 % English : Every student is enrolled in at least one course. Every professor % 30.84/30.94 % teaches at least one course. Every course has at least one student % 30.84/30.94 % enrolled. Every course has at least one professor teaching. The % 30.84/30.94 % coordinator of a course teaches the course. If a student is % 30.84/30.94 % enroled in a course then the student is taught by every professor % 30.84/30.94 % who teaches the course. Michael is enrolled in CSC410. Victor is % 30.84/30.94 % the coordinator of CSC410. Therefore, Michael is taught by Victor. % 30.84/30.94 % 30.84/30.94 % Refs : % 30.84/30.94 % Source : [TPTP] % 30.84/30.94 % Names : % 30.84/30.94 % 30.84/30.94 % Status : Theorem % 30.84/30.94 % Rating : 0.06 v7.4.0, 0.07 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.05 v5.0.0, 0.04 v4.1.0 % 30.84/30.94 % Syntax : Number of formulae : 16 ( 9 unt; 0 def) % 30.84/30.94 % Number of atoms : 31 ( 1 equ) % 30.84/30.94 % Maximal formula atoms : 6 ( 1 avg) % 30.84/30.94 % Number of connectives : 15 ( 0 ~; 0 |; 5 &) % 30.84/30.94 % ( 0 <=>; 10 =>; 0 <=; 0 <~>) % 30.84/30.94 % Maximal formula depth : 8 ( 3 avg) % 30.84/30.94 % Maximal term depth : 2 ( 1 avg) % 30.84/30.94 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 30.84/30.94 % Number of functors : 4 ( 4 usr; 3 con; 0-1 aty) % 30.84/30.94 % Number of variables : 16 ( 9 !; 7 ?) % 30.84/30.94 % SPC : FOF_THM_RFO_SEQ % 30.84/30.94 % 30.84/30.94 % Comments : % 30.84/30.94 %------------------------------------------------------------------------------ % 30.84/30.94 fof(student_type,axiom, % 30.84/30.94 ? [A] : student(A) ). % 30.84/30.94 % 30.84/30.94 fof(professor_type,axiom, % 30.84/30.94 ? [A] : professor(A) ). % 30.84/30.94 % 30.84/30.94 fof(course_type,axiom, % 30.84/30.94 ? [A] : course(A) ). % 30.84/30.94 % 30.84/30.94 fof(michael_type,axiom, % 30.84/30.94 student(michael) ). % 30.84/30.94 % 30.84/30.94 fof(victor_type,axiom, % 30.84/30.94 professor(victor) ). % 30.84/30.94 % 30.84/30.94 fof(csc410_type,axiom, % 30.84/30.94 course(csc410) ). % 30.84/30.94 % 30.84/30.94 fof(coordinator_of_type,axiom, % 30.84/30.94 ! [A] : % 30.84/30.94 ( course(A) % 30.84/30.94 => professor(coordinatorof(A)) ) ). % 30.84/30.94 % 30.84/30.94 fof(student_enrolled_axiom,axiom, % 30.84/30.94 ! [X] : % 30.84/30.94 ( student(X) % 30.84/30.94 => ? [Y] : % 30.84/30.94 ( course(Y) % 30.84/30.94 & enrolled(X,Y) ) ) ). % 30.84/30.94 % 30.84/30.94 fof(professor_teaches,axiom, % 30.84/30.94 ! [X] : % 30.84/30.94 ( professor(X) % 30.84/30.94 => ? [Y] : % 30.84/30.94 ( course(Y) % 30.84/30.94 & teaches(X,Y) ) ) ). % 30.84/30.94 % 30.84/30.94 fof(course_enrolled,axiom, % 30.84/30.94 ! [X] : % 30.84/30.94 ( course(X) % 30.84/30.94 => ? [Y] : % 30.84/30.94 ( student(Y) % 30.84/30.94 & enrolled(Y,X) ) ) ). % 30.84/30.94 % 30.84/30.94 fof(course_teaches,axiom, % 30.84/30.94 ! [X] : % 30.84/30.94 ( course(X) % 30.84/30.94 => ? [Y] : % 30.84/30.94 ( professor(Y) % 30.84/30.94 & teaches(Y,X) ) ) ). % 30.84/30.94 % 30.84/30.94 fof(coordinator_teaches,axiom, % 30.84/30.94 ! [X] : % 30.84/30.94 ( course(X) % 30.84/30.94 => teaches(coordinatorof(X),X) ) ). % 30.84/30.94 % 30.84/30.94 fof(student_enrolled_taught,axiom, % 30.84/30.94 ! [X,Y] : % 30.84/30.94 ( ( student(X) % 30.84/30.94 & course(Y) ) % 30.84/30.94 => ( enrolled(X,Y) % 30.84/30.94 => ! [Z] : % 30.84/30.94 ( professor(Z) % 30.84/30.94 => ( teaches(Z,Y) % 30.84/30.94 => taughtby(X,Z) ) ) ) ) ). % 30.84/30.94 % 30.84/30.94 fof(michael_enrolled_csc410_axiom,axiom, % 30.84/30.94 enrolled(michael,csc410) ). % 30.84/30.94 % 30.84/30.94 fof(victor_coordinator_csc410_axiom,axiom, % 30.84/30.94 coordinatorof(csc410) = victor ). % 30.84/30.94 % 30.84/30.94 fof(teaching_conjecture,conjecture, % 30.84/30.94 taughtby(michael,victor) ). % 30.84/30.94 % 30.84/30.94 %------------------------------------------------------------------------------ % 30.84/30.94 %------------------------------------------- % 30.84/30.94 % Proof found % 30.84/30.94 % SZS status Theorem for theBenchmark % 30.84/30.94 % SZS output start Proof % 30.84/30.94 %ClaNum:37(EqnAxiom:17) % 30.84/30.94 %VarNum:34(SingletonVarNum:13) % 30.84/30.94 %MaxLitNum:6 % 30.84/30.94 %MaxfuncDepth:1 % 30.84/30.94 %SharedTerms:16 % 30.84/30.94 %goalClause: 26 % 30.84/30.94 %singleGoalClaCount:1 % 30.84/30.94 [19]P1(a4) % 30.84/30.94 [20]P1(a5) % 30.84/30.94 [21]P2(a3) % 30.84/30.94 [22]P2(a6) % 30.84/30.94 [23]P3(a1) % 30.84/30.94 [24]P3(a7) % 30.84/30.94 [25]P4(a4,a1) % 30.84/30.94 [26]~P5(a4,a3) % 30.84/30.94 [18]E(f2(a1),a3) % 30.84/30.94 [27]~P3(x271)+P1(f8(x271)) % 30.84/30.94 [28]~P3(x281)+P2(f2(x281)) % 30.84/30.94 [29]~P3(x291)+P2(f11(x291)) % 30.84/30.94 [30]~P1(x301)+P3(f9(x301)) % 30.84/30.94 [31]~P2(x311)+P3(f10(x311)) % 30.84/30.94 [32]~P1(x321)+P4(x321,f9(x321)) % 30.84/30.94 [33]~P2(x331)+P6(x331,f10(x331)) % 30.84/30.94 [34]~P3(x341)+P4(f8(x341),x341) % 30.84/30.94 [35]~P3(x351)+P6(f2(x351),x351) % 30.84/30.94 [36]~P3(x361)+P6(f11(x361),x361) % 30.84/30.94 [37]~P1(x371)+~P2(x372)+~P4(x371,x373)+~P6(x372,x373)+P5(x371,x372)+~P3(x373) % 30.84/30.94 %EqnAxiom % 30.84/30.94 [1]E(x11,x11) % 30.84/30.94 [2]E(x22,x21)+~E(x21,x22) % 30.84/30.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 30.84/30.94 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 30.84/30.94 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 30.84/30.94 [6]~E(x61,x62)+E(f11(x61),f11(x62)) % 30.84/30.94 [7]~E(x71,x72)+E(f10(x71),f10(x72)) % 30.84/30.94 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 30.84/30.94 [9]~P1(x91)+P1(x92)+~E(x91,x92) % 30.84/30.94 [10]P6(x102,x103)+~E(x101,x102)+~P6(x101,x103) % 30.84/30.94 [11]P6(x113,x112)+~E(x111,x112)+~P6(x113,x111) % 30.84/30.94 [12]~P2(x121)+P2(x122)+~E(x121,x122) % 30.84/30.94 [13]~P3(x131)+P3(x132)+~E(x131,x132) % 30.84/30.94 [14]P5(x142,x143)+~E(x141,x142)+~P5(x141,x143) % 30.84/30.94 [15]P5(x153,x152)+~E(x151,x152)+~P5(x153,x151) % 30.84/30.94 [16]P4(x162,x163)+~E(x161,x162)+~P4(x161,x163) % 30.84/30.94 [17]P4(x173,x172)+~E(x171,x172)+~P4(x173,x171) % 30.84/30.94 % 30.84/30.94 %------------------------------------------- % 30.84/30.95 cnf(39,plain, % 30.84/30.95 (P2(f2(a1))), % 30.84/30.95 inference(scs_inference,[],[21,18,2,12])). % 30.84/30.95 cnf(792,plain, % 30.84/30.95 (~P5(x7921,f2(a1))+P5(a4,a3)+~E(x7921,a4)), % 30.84/30.95 inference(scs_inference,[],[26,18,14,15])). % 30.84/30.95 cnf(793,plain, % 30.84/30.95 (~P5(a4,f2(a1))+P5(a4,a3)), % 30.84/30.95 inference(equality_inference,[],[792])). % 30.84/30.95 cnf(794,plain, % 30.84/30.95 (~P5(a4,f2(a1))), % 30.84/30.95 inference(scs_inference,[],[26,793])). % 30.84/30.95 cnf(7204,plain, % 30.84/30.95 (~E(a1,x72041)+P3(x72041)), % 30.84/30.95 inference(scs_inference,[],[23,13])). % 30.84/30.95 cnf(7935,plain, % 30.84/30.95 (P6(f2(x79351),x79351)+~E(a1,x79351)), % 30.84/30.95 inference(scs_inference,[],[7204,35])). % 30.84/30.95 cnf(7936,plain, % 30.84/30.95 (P6(f2(a1),a1)), % 30.84/30.95 inference(equality_inference,[],[7935])). % 30.84/30.95 cnf(7984,plain, % 30.84/30.95 ($false), % 30.84/30.95 inference(scs_inference,[],[19,25,23,7936,794,39,37]), % 30.84/30.95 ['proof']). % 30.84/30.95 % SZS output end Proof % 30.84/30.95 % Total time :30.430000s %------------------------------------------------------------------------------