%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PUZ078+1 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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 : 600s % DateTime : Mon Jul 18 18:27:29 EDT 2022 % Result : Theorem 0.19s 0.48s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : PUZ078+1 : TPTP v8.1.0. Released v3.5.0. % 0.08/0.13 % Command : run_spass %d %s % 0.12/0.33 % Computer : n020.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.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat May 28 21:38:54 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.48 % 0.19/0.48 SPASS V 3.9 % 0.19/0.48 SPASS beiseite: Proof found. % 0.19/0.48 % SZS status Theorem % 0.19/0.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.48 SPASS derived 626 clauses, backtracked 374 clauses, performed 13 splits and kept 739 clauses. % 0.19/0.48 SPASS allocated 97967 KBytes. % 0.19/0.48 SPASS spent 0:00:00.14 on the problem. % 0.19/0.48 0:00:00.03 for the input. % 0.19/0.48 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.48 0:00:00.01 for inferences. % 0.19/0.48 0:00:00.00 for the backtracking. % 0.19/0.48 0:00:00.05 for the reduction. % 0.19/0.48 % 0.19/0.48 % 0.19/0.48 Here is a proof with depth 6, length 157 : % 0.19/0.48 % SZS output start Refutation % 0.19/0.48 1[0:Inp] || -> truthday(skc4)*. % 0.19/0.48 2[0:Inp] || -> day1(skc5)*. % 0.19/0.48 4[0:Inp] || -> day3(skc7)*. % 0.19/0.48 5[0:Inp] || truthday(tuesday)* -> . % 0.19/0.48 7[0:Inp] || equal(wednesday,monday)** -> . % 0.19/0.48 9[0:Inp] || equal(friday,monday)** -> . % 0.19/0.48 11[0:Inp] || equal(sunday,monday)** -> . % 0.19/0.48 17[0:Inp] || equal(thursday,wednesday)** -> . % 0.19/0.48 24[0:Inp] || equal(saturday,friday)** -> . % 0.19/0.48 27[0:Inp] || -> equal(consecutive(sunday),monday)**. % 0.19/0.48 28[0:Inp] || -> equal(consecutive(monday),tuesday)**. % 0.19/0.48 29[0:Inp] || -> equal(consecutive(tuesday),wednesday)**. % 0.19/0.48 30[0:Inp] || -> equal(consecutive(wednesday),thursday)**. % 0.19/0.48 32[0:Inp] || -> equal(consecutive(friday),saturday)**. % 0.19/0.48 33[0:Inp] || -> equal(consecutive(saturday),sunday)**. % 0.19/0.48 34[0:Inp] day1(u) || -> day2(consecutive(u))*. % 0.19/0.48 35[0:Inp] || day2(consecutive(u))* -> day1(u). % 0.19/0.48 36[0:Inp] day2(u) || -> day3(consecutive(u))*. % 0.19/0.48 37[0:Inp] || day3(consecutive(u))* -> day2(u). % 0.19/0.48 38[0:Inp] day2(u) || day2(thursday)*+ -> truthday(u)*. % 0.19/0.48 39[0:Inp] day2(u) || day2(saturday)*+ -> truthday(u)*. % 0.19/0.48 40[0:Inp] day2(u) || day2(sunday)*+ -> truthday(u)*. % 0.19/0.48 41[0:Inp] truthday(u) truthday(v) || -> equal(v,u)*. % 0.19/0.48 45[0:Inp] day1(u) truthday(u) || truthday(monday)* -> . % 0.19/0.48 47[0:Inp] day1(u) || -> truthday(monday) truthday(tuesday)* truthday(u)*. % 0.19/0.48 48[0:Inp] day3(u) truthday(u) || truthday(wednesday)* -> . % 0.19/0.48 49[0:Inp] day3(u) truthday(u) || truthday(friday)* -> . % 0.19/0.48 50[0:Inp] day3(u) || -> truthday(u)* truthday(friday)* truthday(wednesday). % 0.19/0.48 52[0:Inp] || -> equal(u,sunday)* equal(u,saturday) equal(u,friday) equal(u,thursday) equal(u,wednesday) equal(u,tuesday) equal(u,monday). % 0.19/0.48 53[0:MRR:47.2,5.0] day1(u) || -> truthday(u)* truthday(monday)*. % 0.19/0.48 54[0:Res:53.2,5.0] day1(tuesday) || -> truthday(monday)*. % 0.19/0.48 55[0:Res:50.3,5.0] day3(tuesday) || -> truthday(friday)* truthday(wednesday). % 0.19/0.48 59[0:Res:2.0,53.0] || -> truthday(skc5)* truthday(monday). % 0.19/0.48 62[1:Spt:53.0,53.1] day1(u) || -> truthday(u)*. % 0.19/0.48 63[1:MRR:45.1,62.1] day1(u) || truthday(monday)* -> . % 0.19/0.48 64[1:MRR:54.1,63.1] day1(tuesday) || -> . % 0.19/0.48 65[2:Spt:50.0,50.1] day3(u) || -> truthday(u)*. % 0.19/0.48 66[2:MRR:49.1,65.1] day3(u) || truthday(friday)* -> . % 0.19/0.48 67[2:MRR:48.1,65.1] day3(u) || truthday(wednesday)* -> . % 0.19/0.48 68[2:MRR:55.1,66.1] day3(tuesday) || -> truthday(wednesday)*. % 0.19/0.48 69[2:MRR:68.1,67.1] day3(tuesday) || -> . % 0.19/0.48 70[3:Spt:59.1] || -> truthday(monday)*. % 0.19/0.48 71[3:MRR:63.1,70.0] day1(u) || -> . % 0.19/0.48 72[3:UnC:71.0,2.0] || -> . % 0.19/0.48 73[3:Spt:72.0,59.1,70.0] || truthday(monday)* -> . % 0.19/0.48 74[3:Spt:72.0,59.0] || -> truthday(skc5)*. % 0.19/0.48 77[3:Res:65.1,73.0] day3(monday) || -> . % 0.19/0.48 86[2:EmS:66.0,4.0] || truthday(friday)* -> . % 0.19/0.48 89[2:EmS:67.0,4.0] || truthday(wednesday)* -> . % 0.19/0.48 97[0:SpR:28.0,36.1] day2(monday) || -> day3(tuesday)*. % 0.19/0.48 98[0:SpR:27.0,36.1] day2(sunday) || -> day3(monday)*. % 0.19/0.48 102[2:MRR:97.1,69.0] day2(monday) || -> . % 0.19/0.48 103[3:MRR:98.1,77.0] day2(sunday) || -> . % 0.19/0.48 105[0:SpR:33.0,34.1] day1(saturday) || -> day2(sunday)*. % 0.19/0.48 106[0:SpR:32.0,34.1] day1(friday) || -> day2(saturday)*. % 0.19/0.48 108[0:SpR:30.0,34.1] day1(wednesday) || -> day2(thursday)*. % 0.19/0.48 111[0:SpR:27.0,34.1] day1(sunday) || -> day2(monday)*. % 0.19/0.48 112[3:MRR:105.1,103.0] day1(saturday) || -> . % 0.19/0.48 113[2:MRR:111.1,102.0] day1(sunday) || -> . % 0.19/0.48 118[0:SpL:29.0,35.0] || day2(wednesday)* -> day1(tuesday). % 0.19/0.48 126[1:MRR:118.1,64.0] || day2(wednesday)* -> . % 0.19/0.48 132[0:SpL:30.0,37.0] || day3(thursday)* -> day2(wednesday). % 0.19/0.48 134[0:SpL:28.0,37.0] || day3(tuesday)* -> day2(monday). % 0.19/0.48 135[0:SpL:27.0,37.0] || day3(monday)* -> day2(sunday). % 0.19/0.48 140[1:MRR:132.1,126.0] || day3(thursday)* -> . % 0.19/0.48 143[2:MRR:134.1,102.0] || day3(tuesday)* -> . % 0.19/0.48 163[0:EmS:41.0,1.0] truthday(u) || -> equal(u,skc4)*. % 0.19/0.48 168[3:EmS:163.0,74.0] || -> equal(skc5,skc4)**. % 0.19/0.48 170[2:EmS:163.0,65.1] day3(u) || -> equal(u,skc4)*. % 0.19/0.48 171[3:Rew:168.0,2.0] || -> day1(skc4)*. % 0.19/0.48 188[3:SpR:52.0,171.0] || -> equal(skc4,saturday) equal(skc4,friday) equal(skc4,thursday) equal(skc4,wednesday) equal(skc4,tuesday) equal(skc4,monday) day1(sunday)*. % 0.19/0.48 219[3:MRR:188.6,113.0] || -> equal(skc4,saturday)** equal(skc4,friday) equal(skc4,thursday) equal(skc4,wednesday) equal(skc4,tuesday) equal(skc4,monday). % 0.19/0.48 223[2:EmS:170.0,4.0] || -> equal(skc7,skc4)**. % 0.19/0.48 224[2:Rew:223.0,4.0] || -> day3(skc4)*. % 0.19/0.48 244[4:Spt:219.0] || -> equal(skc4,saturday)**. % 0.19/0.48 249[4:Rew:244.0,171.0] || -> day1(saturday)*. % 0.19/0.48 254[4:MRR:249.0,112.0] || -> . % 0.19/0.48 262[4:Spt:254.0,219.0,244.0] || equal(skc4,saturday)** -> . % 0.19/0.48 263[4:Spt:254.0,219.1,219.2,219.3,219.4,219.5] || -> equal(skc4,friday)** equal(skc4,thursday) equal(skc4,wednesday) equal(skc4,tuesday) equal(skc4,monday). % 0.19/0.48 264[5:Spt:263.0] || -> equal(skc4,friday)**. % 0.19/0.48 267[5:Rew:264.0,1.0] || -> truthday(friday)*. % 0.19/0.48 277[5:MRR:267.0,86.0] || -> . % 0.19/0.48 278[5:Spt:277.0,263.0,264.0] || equal(skc4,friday)** -> . % 0.19/0.48 279[5:Spt:277.0,263.1,263.2,263.3,263.4] || -> equal(skc4,thursday)** equal(skc4,wednesday) equal(skc4,tuesday) equal(skc4,monday). % 0.19/0.48 280[6:Spt:279.0] || -> equal(skc4,thursday)**. % 0.19/0.48 283[6:Rew:280.0,224.0] || -> day3(thursday)*. % 0.19/0.48 294[6:MRR:283.0,140.0] || -> . % 0.19/0.48 300[6:Spt:294.0,279.0,280.0] || equal(skc4,thursday)** -> . % 0.19/0.48 301[6:Spt:294.0,279.1,279.2,279.3] || -> equal(skc4,wednesday)** equal(skc4,tuesday) equal(skc4,monday). % 0.19/0.48 302[7:Spt:301.0] || -> equal(skc4,wednesday)**. % 0.19/0.48 305[7:Rew:302.0,1.0] || -> truthday(wednesday)*. % 0.19/0.48 317[7:MRR:305.0,89.0] || -> . % 0.19/0.48 318[7:Spt:317.0,301.0,302.0] || equal(skc4,wednesday)** -> . % 0.19/0.48 319[7:Spt:317.0,301.1,301.2] || -> equal(skc4,tuesday)** equal(skc4,monday). % 0.19/0.48 320[8:Spt:319.0] || -> equal(skc4,tuesday)**. % 0.19/0.48 323[8:Rew:320.0,224.0] || -> day3(tuesday)*. % 0.19/0.48 336[8:MRR:323.0,143.0] || -> . % 0.19/0.48 337[8:Spt:336.0,319.0,320.0] || equal(skc4,tuesday)** -> . % 0.19/0.48 338[8:Spt:336.0,319.1] || -> equal(skc4,monday)**. % 0.19/0.48 341[8:Rew:338.0,1.0] || -> truthday(monday)*. % 0.19/0.48 346[8:MRR:341.0,73.0] || -> . % 0.19/0.48 356[2:Spt:346.0,50.2,50.3] || -> truthday(friday)* truthday(wednesday). % 0.19/0.48 357[3:Spt:356.0] || -> truthday(friday)*. % 0.19/0.48 361[4:Spt:59.1] || -> truthday(monday)*. % 0.19/0.48 362[4:MRR:63.1,361.0] day1(u) || -> . % 0.19/0.48 363[4:UnC:362.0,2.0] || -> . % 0.19/0.48 364[4:Spt:363.0,59.1,361.0] || truthday(monday)* -> . % 0.19/0.48 365[4:Spt:363.0,59.0] || -> truthday(skc5)*. % 0.19/0.48 407[4:EmS:163.0,365.0] || -> equal(skc5,skc4)**. % 0.19/0.48 408[3:EmS:163.0,357.0] || -> equal(skc4,friday)**. % 0.19/0.48 411[0:EmS:163.0,39.2] day2(u) || day2(saturday)* -> equal(u,skc4)*. % 0.19/0.48 414[4:Rew:407.0,2.0] || -> day1(skc4)*. % 0.19/0.48 423[4:Rew:408.0,414.0] || -> day1(friday)*. % 0.19/0.48 424[4:MRR:106.0,423.0] || -> day2(saturday)*. % 0.19/0.48 459[3:Rew:408.0,411.2] day2(u) || day2(saturday)* -> equal(u,friday)*. % 0.19/0.48 460[4:MRR:459.1,424.0] day2(u) || -> equal(u,friday)*. % 0.19/0.48 495[4:EmS:460.0,424.0] || -> equal(saturday,friday)**. % 0.19/0.48 496[4:MRR:495.0,24.0] || -> . % 0.19/0.48 497[3:Spt:496.0,356.0,357.0] || truthday(friday)* -> . % 0.19/0.48 498[3:Spt:496.0,356.1] || -> truthday(wednesday)*. % 0.19/0.48 502[4:Spt:59.1] || -> truthday(monday)*. % 0.19/0.48 503[4:MRR:63.1,502.0] day1(u) || -> . % 0.19/0.48 504[4:UnC:503.0,2.0] || -> . % 0.19/0.48 505[4:Spt:504.0,59.1,502.0] || truthday(monday)* -> . % 0.19/0.48 506[4:Spt:504.0,59.0] || -> truthday(skc5)*. % 0.19/0.48 554[4:EmS:163.0,506.0] || -> equal(skc5,skc4)**. % 0.19/0.48 555[3:EmS:163.0,498.0] || -> equal(skc4,wednesday)**. % 0.19/0.48 558[0:EmS:163.0,38.2] day2(u) || day2(thursday)* -> equal(u,skc4)*. % 0.19/0.48 560[4:Rew:554.0,2.0] || -> day1(skc4)*. % 0.19/0.48 571[4:Rew:555.0,560.0] || -> day1(wednesday)*. % 0.19/0.48 572[4:MRR:108.0,571.0] || -> day2(thursday)*. % 0.19/0.48 601[3:Rew:555.0,558.2] day2(u) || day2(thursday)* -> equal(u,wednesday)*. % 0.19/0.48 602[4:MRR:601.1,572.0] day2(u) || -> equal(u,wednesday)*. % 0.19/0.48 631[4:EmS:602.0,572.0] || -> equal(thursday,wednesday)**. % 0.19/0.48 632[4:MRR:631.0,17.0] || -> . % 0.19/0.48 633[1:Spt:632.0,53.2] || -> truthday(monday)*. % 0.19/0.48 635[1:EmS:41.0,633.0] truthday(u) || -> equal(u,monday)*. % 0.19/0.48 637[2:Spt:50.0,50.1] day3(u) || -> truthday(u)*. % 0.19/0.48 695[1:EmS:163.0,633.0] || -> equal(skc4,monday)**. % 0.19/0.48 696[2:EmS:163.0,637.1] day3(u) || -> equal(u,skc4)*. % 0.19/0.48 697[0:EmS:163.0,40.2] day2(u) || day2(sunday)* -> equal(u,skc4)*. % 0.19/0.48 703[2:Rew:695.0,696.1] day3(u) || -> equal(u,monday)*. % 0.19/0.49 704[1:Rew:695.0,697.2] day2(u) || day2(sunday)* -> equal(u,monday)*. % 0.19/0.49 711[2:EmS:703.0,4.0] || -> equal(skc7,monday)**. % 0.19/0.49 712[2:Rew:711.0,4.0] || -> day3(monday)*. % 0.19/0.49 715[2:MRR:135.0,712.0] || -> day2(sunday)*. % 0.19/0.49 721[2:MRR:704.1,715.0] day2(u) || -> equal(u,monday)*. % 0.19/0.49 769[2:EmS:721.0,715.0] || -> equal(sunday,monday)**. % 0.19/0.49 770[2:MRR:769.0,11.0] || -> . % 0.19/0.49 771[2:Spt:770.0,50.2,50.3] || -> truthday(friday)* truthday(wednesday). % 0.19/0.49 773[3:Spt:771.0] || -> truthday(friday)*. % 0.19/0.49 775[3:EmS:635.0,773.0] || -> equal(friday,monday)**. % 0.19/0.49 778[3:MRR:775.0,9.0] || -> . % 0.19/0.49 779[3:Spt:778.0,771.0,773.0] || truthday(friday)* -> . % 0.19/0.49 780[3:Spt:778.0,771.1] || -> truthday(wednesday)*. % 0.19/0.49 782[3:EmS:635.0,780.0] || -> equal(wednesday,monday)**. % 0.19/0.49 785[3:MRR:782.0,7.0] || -> . % 0.19/0.49 % SZS output end Refutation % 0.19/0.49 Formulae used in the proof : truth_once day1_once day3_once tuesday_leo_tells_truths uniquenames monday_follows_sunday tuesday_follows_monday wednesday_follows_tuesday thursday_follows_wednesday saturday_follows_friday sunday_follows_saturday day2_follows_day1 day3_follows_day2 statement2 truth_unique statement1 statement3 days_of_week % 0.19/0.49 %------------------------------------------------------------------------------