%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ018-1 : TPTP v8.2.0. Bugfixed v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n009.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:04 EDT 2024 % Result : Unsatisfiable 58.66s 59.37s % Output : CNFRefutation 58.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ018-1 : TPTP v8.2.0. Bugfixed v1.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 10:33:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 58.60/59.35 %------------------------------------------- % 58.60/59.35 % File :CSE---1.7 % 58.60/59.35 % Problem :theBenchmark % 58.60/59.35 % Transform :cnf % 58.60/59.35 % Format :tptp:raw % 58.60/59.35 % Command :java -jar mcs_scs.jar %d %s % 58.60/59.35 % 58.60/59.35 % Result :Theorem 58.060000s % 58.60/59.35 % Output :CNFRefutation 58.060000s % 58.60/59.35 %------------------------------------------- % 58.66/59.36 %-------------------------------------------------------------------------- % 58.66/59.36 % File : PUZ018-1 : TPTP v8.2.0. Bugfixed v1.2.0. % 58.66/59.36 % Domain : Puzzles % 58.66/59.36 % Problem : The Interns % 58.66/59.36 % Version : Especial. % 58.66/59.36 % English : Three interns are residents of the same hospital. On only one % 58.66/59.36 % day of the week are all three interns on call. No intern % 58.66/59.36 % is on call on three consecutiveutive days. No two interns are % 58.66/59.36 % off on the same day more than once a week. The first intern % 58.66/59.36 % is off on Sunday, Tuesday, and Thursday. The second intern % 58.66/59.36 % is off on Thursday and Saturday. The third intern is off % 58.66/59.36 % on Sunday. Which day of the week are all three interns % 58.66/59.36 % on call? % 58.66/59.36 % 58.66/59.36 % Refs : [Rap95] Raptis (1995), Email to G. Sutcliffe % 58.66/59.36 % Source : [ANL] % 58.66/59.37 % Names : interns.ver1.in [ANL] % 58.66/59.37 % 58.66/59.37 % Status : Unsatisfiable % 58.66/59.37 % Rating : 0.00 v6.2.0, 0.12 v6.1.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.25 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0 % 58.66/59.37 % Syntax : Number of clauses : 48 ( 40 unt; 2 nHn; 45 RR) % 58.66/59.37 % Number of literals : 72 ( 0 equ; 45 neg) % 58.66/59.37 % Maximal clause size : 7 ( 1 avg) % 58.66/59.37 % Maximal term depth : 1 ( 1 avg) % 58.66/59.37 % Number of predicates : 5 ( 5 usr; 0 prp; 1-2 aty) % 58.66/59.37 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 58.66/59.37 % Number of variables : 17 ( 1 sgn) % 58.66/59.37 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.66/59.37 % 58.66/59.37 % Comments : Dimitris Raptis pointed out [Rap95] that this was trivially % 58.66/59.37 % unsatisfiable, by resolving prove_all_on_one_day % 58.66/59.37 % [--all_on(Day)] with all_on_one_day. % 58.66/59.37 % Bugfixes : v1.2.0 - Theorem clause prove_all_on_one_day grounded. % 58.66/59.37 %-------------------------------------------------------------------------- % 58.66/59.37 cnf(all_on_a_on,axiom, % 58.66/59.37 ( ~ all_on(X) % 58.66/59.37 | on(a,X) ) ). % 58.66/59.37 % 58.66/59.37 cnf(all_on_b_on,axiom, % 58.66/59.37 ( ~ all_on(X) % 58.66/59.37 | on(b,X) ) ). % 58.66/59.37 % 58.66/59.37 cnf(all_on_c_on,axiom, % 58.66/59.37 ( ~ all_on(X) % 58.66/59.37 | on(c,X) ) ). % 58.66/59.37 % 58.66/59.37 cnf(all_on,axiom, % 58.66/59.37 ( all_on(X) % 58.66/59.37 | ~ on(a,X) % 58.66/59.37 | ~ on(b,X) % 58.66/59.37 | ~ on(c,X) ) ). % 58.66/59.37 % 58.66/59.37 cnf(all_on_well_defined,axiom, % 58.66/59.37 ( ~ all_on(X) % 58.66/59.37 | ~ all_on(Y) % 58.66/59.37 | same_day(X,Y) ) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_follows_sunday,axiom, % 58.66/59.37 consecutive(sunday,monday) ). % 58.66/59.37 % 58.66/59.37 cnf(tuesday_follows_monday,axiom, % 58.66/59.37 consecutive(monday,tuesday) ). % 58.66/59.37 % 58.66/59.37 cnf(wednesday_follows_tuesday,axiom, % 58.66/59.37 consecutive(tuesday,wednesday) ). % 58.66/59.37 % 58.66/59.37 cnf(thursday_follows_wednesday,axiom, % 58.66/59.37 consecutive(wednesday,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(friday_follows_thursday,axiom, % 58.66/59.37 consecutive(thursday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(staurday_follows_friday,axiom, % 58.66/59.37 consecutive(friday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_follows_saturday,axiom, % 58.66/59.37 consecutive(saturday,sunday) ). % 58.66/59.37 % 58.66/59.37 cnf(reflexivity_for_same_person,axiom, % 58.66/59.37 same_person(X,X) ). % 58.66/59.37 % 58.66/59.37 cnf(a_not_b,axiom, % 58.66/59.37 ~ same_person(a,b) ). % 58.66/59.37 % 58.66/59.37 cnf(a_not_c,axiom, % 58.66/59.37 ~ same_person(a,c) ). % 58.66/59.37 % 58.66/59.37 cnf(b_not_c,axiom, % 58.66/59.37 ~ same_person(b,c) ). % 58.66/59.37 % 58.66/59.37 cnf(reflexivity_for_same_day,axiom, % 58.66/59.37 same_day(X,X) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_monday,axiom, % 58.66/59.37 ~ same_day(sunday,monday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_tuesday,axiom, % 58.66/59.37 ~ same_day(sunday,tuesday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_wednesday,axiom, % 58.66/59.37 ~ same_day(sunday,wednesday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_thursday,axiom, % 58.66/59.37 ~ same_day(sunday,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_friday,axiom, % 58.66/59.37 ~ same_day(sunday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(sunday_not_saturday,axiom, % 58.66/59.37 ~ same_day(sunday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_not_tuesday,axiom, % 58.66/59.37 ~ same_day(monday,tuesday) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_not_wednesday,axiom, % 58.66/59.37 ~ same_day(monday,wednesday) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_not_thursday,axiom, % 58.66/59.37 ~ same_day(monday,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_not_friday,axiom, % 58.66/59.37 ~ same_day(monday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(monday_not_saturday,axiom, % 58.66/59.37 ~ same_day(monday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(tuesday_not_wednesday,axiom, % 58.66/59.37 ~ same_day(tuesday,wednesday) ). % 58.66/59.37 % 58.66/59.37 cnf(tuesday_not_thursday,axiom, % 58.66/59.37 ~ same_day(tuesday,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(tuesday_not_friday,axiom, % 58.66/59.37 ~ same_day(tuesday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(tuesday_not_saturday,axiom, % 58.66/59.37 ~ same_day(tuesday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(wednesday_not_thursday,axiom, % 58.66/59.37 ~ same_day(wednesday,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(wednesday_not_friday,axiom, % 58.66/59.37 ~ same_day(wednesday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(wednesday_not_saturday,axiom, % 58.66/59.37 ~ same_day(wednesday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(thursday_not_friday,axiom, % 58.66/59.37 ~ same_day(thursday,friday) ). % 58.66/59.37 % 58.66/59.37 cnf(thursday_not_saturday,axiom, % 58.66/59.37 ~ same_day(thursday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(friday_not_saturday,axiom, % 58.66/59.37 ~ same_day(friday,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(all_on_one_day,hypothesis, % 58.66/59.37 ( all_on(sunday) % 58.66/59.37 | all_on(monday) % 58.66/59.37 | all_on(tuesday) % 58.66/59.37 | all_on(wednesday) % 58.66/59.37 | all_on(thursday) % 58.66/59.37 | all_on(friday) % 58.66/59.37 | all_on(saturday) ) ). % 58.66/59.37 % 58.66/59.37 cnf(not_on_for_3_days,hypothesis, % 58.66/59.37 ( ~ consecutive(X,Y) % 58.66/59.37 | ~ consecutive(Y,Z) % 58.66/59.37 | ~ consecutive(Z,W) % 58.66/59.37 | ~ on(U,X) % 58.66/59.37 | ~ on(U,Y) % 58.66/59.37 | ~ on(U,Z) ) ). % 58.66/59.37 % 58.66/59.37 cnf(no_two_off_twice_together,hypothesis, % 58.66/59.37 ( on(X,Y) % 58.66/59.37 | on(X,Z) % 58.66/59.37 | on(W,Y) % 58.66/59.37 | on(W,Z) % 58.66/59.37 | same_person(X,W) % 58.66/59.37 | same_day(Y,Z) ) ). % 58.66/59.37 % 58.66/59.37 cnf(a_off_sunday,hypothesis, % 58.66/59.37 ~ on(a,sunday) ). % 58.66/59.37 % 58.66/59.37 cnf(a_off_tuesday,hypothesis, % 58.66/59.37 ~ on(a,tuesday) ). % 58.66/59.37 % 58.66/59.37 cnf(a_off_thursday,hypothesis, % 58.66/59.37 ~ on(a,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(b_off_thursday,hypothesis, % 58.66/59.37 ~ on(b,thursday) ). % 58.66/59.37 % 58.66/59.37 cnf(b_off_saturday,hypothesis, % 58.66/59.37 ~ on(b,saturday) ). % 58.66/59.37 % 58.66/59.37 cnf(c_off_sunday,hypothesis, % 58.66/59.37 ~ on(c,sunday) ). % 58.66/59.37 % 58.66/59.37 cnf(prove_all_on_friday,negated_conjecture, % 58.66/59.37 ~ all_on(friday) ). % 58.66/59.37 % 58.66/59.37 %-------------------------------------------------------------------------- % 58.66/59.37 %------------------------------------------- % 58.66/59.37 % Proof found % 58.66/59.37 % SZS status Theorem for theBenchmark % 58.66/59.37 % SZS output start Proof % 58.66/59.38 %ClaNum:48(EqnAxiom:0) % 58.66/59.38 %VarNum:42(SingletonVarNum:17) % 58.66/59.38 %MaxLitNum:7 % 58.66/59.38 %MaxfuncDepth:0 % 58.66/59.38 %SharedTerms:55 % 58.66/59.38 %goalClause: 10 % 58.66/59.38 %singleGoalClaCount:1 % 58.66/59.38 [1]P1(a1,a2) % 58.66/59.38 [2]P1(a2,a8) % 58.66/59.38 [3]P1(a8,a10) % 58.66/59.38 [4]P1(a10,a9) % 58.66/59.38 [5]P1(a9,a3) % 58.66/59.38 [6]P1(a3,a7) % 58.66/59.38 [7]P1(a7,a1) % 58.66/59.38 [10]~P2(a3) % 58.66/59.38 [11]~P4(a4,a1) % 58.66/59.38 [12]~P4(a4,a8) % 58.66/59.38 [13]~P4(a4,a9) % 58.66/59.38 [14]~P4(a5,a9) % 58.66/59.38 [15]~P4(a5,a7) % 58.66/59.38 [16]~P4(a6,a1) % 58.66/59.38 [17]~P3(a1,a2) % 58.66/59.38 [18]~P3(a1,a8) % 58.66/59.38 [19]~P3(a1,a10) % 58.66/59.38 [20]~P3(a1,a9) % 58.66/59.38 [21]~P3(a1,a3) % 58.66/59.38 [22]~P3(a1,a7) % 58.66/59.38 [23]~P3(a2,a8) % 58.66/59.38 [24]~P3(a2,a10) % 58.66/59.38 [25]~P3(a2,a9) % 58.66/59.38 [26]~P3(a2,a3) % 58.66/59.38 [27]~P3(a2,a7) % 58.66/59.38 [28]~P3(a8,a10) % 58.66/59.38 [29]~P3(a8,a9) % 58.66/59.38 [30]~P3(a8,a3) % 58.66/59.38 [31]~P3(a8,a7) % 58.66/59.38 [32]~P3(a10,a9) % 58.66/59.38 [33]~P3(a10,a3) % 58.66/59.38 [34]~P3(a10,a7) % 58.66/59.38 [35]~P3(a9,a3) % 58.66/59.38 [36]~P3(a9,a7) % 58.66/59.38 [37]~P3(a3,a7) % 58.66/59.38 [38]~P5(a4,a5) % 58.66/59.38 [39]~P5(a4,a6) % 58.66/59.38 [40]~P5(a5,a6) % 58.66/59.38 [8]P3(x81,x81) % 58.66/59.38 [9]P5(x91,x91) % 58.66/59.38 [41]~P2(x411)+P4(a4,x411) % 58.66/59.38 [42]~P2(x421)+P4(a5,x421) % 58.66/59.38 [43]~P2(x431)+P4(a6,x431) % 58.66/59.38 [45]~P2(x452)+~P2(x451)+P3(x451,x452) % 58.66/59.38 [46]P2(x461)+~P4(a4,x461)+~P4(a5,x461)+~P4(a6,x461) % 58.66/59.38 [47]P4(x474,x473)+P3(x473,x472)+P5(x474,x471)+P4(x471,x472)+P4(x471,x473)+P4(x474,x472) % 58.66/59.38 [48]~P1(x483,x482)+~P1(x484,x483)+~P4(x481,x482)+~P4(x481,x483)+~P4(x481,x484)+~P1(x482,x485) % 58.66/59.38 [44]P2(a1)+P2(a2)+P2(a8)+P2(a10)+P2(a9)+P2(a3)+P2(a7) % 58.66/59.38 %EqnAxiom % 58.66/59.38 % 58.66/59.38 %------------------------------------------- % 58.77/59.46 cnf(49,plain, % 58.77/59.46 (~P2(a1)), % 58.77/59.46 inference(scs_inference,[],[11,41])). % 58.77/59.46 cnf(51,plain, % 58.77/59.46 (~P2(a9)), % 58.77/59.46 inference(scs_inference,[],[11,14,41,42])). % 58.77/59.46 cnf(58,plain, % 58.77/59.46 (P2(a2)+P2(a8)+P2(a10)+P2(a7)), % 58.77/59.46 inference(scs_inference,[],[49,51,10,44])). % 58.77/59.46 cnf(59,plain, % 58.77/59.46 (~P2(a7)), % 58.77/59.46 inference(scs_inference,[],[15,42])). % 58.77/59.46 cnf(61,plain, % 58.77/59.46 (~P2(a8)), % 58.77/59.46 inference(scs_inference,[],[12,15,42,41])). % 58.77/59.46 cnf(70,plain, % 58.77/59.46 (P2(a2)+P2(a10)), % 58.77/59.46 inference(scs_inference,[],[61,59,58])). % 58.77/59.46 cnf(429,plain, % 58.77/59.46 (P4(a5,a2)+P2(a10)), % 58.77/59.46 inference(scs_inference,[],[70,42])). % 58.77/59.46 cnf(491,plain, % 58.77/59.46 (P4(a6,a10)+P2(a2)), % 58.77/59.46 inference(scs_inference,[],[70,43])). % 58.77/59.46 cnf(893,plain, % 58.77/59.46 (P4(a4,a2)+P4(a6,a10)), % 58.77/59.46 inference(scs_inference,[],[41,491])). % 58.77/59.46 cnf(1109,plain, % 58.77/59.46 (P4(a5,a2)+P4(a6,a10)), % 58.77/59.46 inference(scs_inference,[],[42,491])). % 58.77/59.46 cnf(1201,plain, % 58.77/59.46 (~P4(a6,a8)+~P2(a10)+~P4(a6,a9)), % 58.77/59.46 inference(scs_inference,[],[4,3,5,43,48])). % 58.77/59.46 cnf(58018,plain, % 58.77/59.46 (P4(a6,a8)), % 58.77/59.46 inference(scs_inference,[],[18,39,16,12,11,47])). % 58.77/59.46 cnf(58022,plain, % 58.77/59.46 (~P4(a6,a9)+~P2(a10)), % 58.77/59.46 inference(scs_inference,[],[18,39,3,16,12,11,47,48,1201])). % 58.77/59.46 cnf(58028,plain, % 58.77/59.46 (~P4(a6,a2)+P4(a5,a2)), % 58.77/59.46 inference(scs_inference,[],[58018,3,4,2,48,491,893,1109])). % 58.77/59.46 cnf(58039,plain, % 58.77/59.46 (~P4(a6,a10)+~P4(a6,a9)), % 58.77/59.46 inference(scs_inference,[],[38,5,58018,3,4,14,13,47,48])). % 58.77/59.46 cnf(58050,plain, % 58.77/59.46 (P4(a6,a7)+~P2(a10)), % 58.77/59.46 inference(scs_inference,[],[40,36,15,14,47,58022])). % 58.77/59.46 cnf(58066,plain, % 58.77/59.46 (P4(a5,a1)), % 58.77/59.46 inference(scs_inference,[],[20,38,13,14,11,47])). % 58.77/59.46 cnf(58093,plain, % 58.77/59.46 (P4(a5,a8)), % 58.77/59.46 inference(scs_inference,[],[29,38,12,13,14,47])). % 58.77/59.46 cnf(58110,plain, % 58.77/59.46 (~P4(a5,a2)), % 58.77/59.46 inference(scs_inference,[],[58093,1,58066,3,2,48])). % 58.77/59.46 cnf(58112,plain, % 58.77/59.46 (P2(a10)), % 58.77/59.46 inference(scs_inference,[],[58093,1,58066,3,2,48,429])). % 58.77/59.46 cnf(58124,plain, % 58.77/59.46 (~P4(a6,a9)), % 58.77/59.46 inference(scs_inference,[],[35,58093,1,58066,38,3,13,14,2,48,429,41,43,42,45,47,58050,58039])). % 58.77/59.46 cnf(58125,plain, % 58.77/59.46 (~P4(a6,a2)), % 58.77/59.46 inference(scs_inference,[],[35,58093,1,58066,38,3,13,14,2,48,429,41,43,42,45,47,58050,58039,58028])). % 58.77/59.46 cnf(58131,plain, % 58.77/59.46 ($false), % 58.77/59.46 inference(scs_inference,[],[58125,58124,58110,58112,25,40,14,45,47]), % 58.77/59.46 ['proof']). % 58.88/59.54 % SZS output end Proof % 58.88/59.54 % Total time :58.060000s %------------------------------------------------------------------------------