%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ029-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:07 EDT 2024 % Result : Unsatisfiable 0.13s 0.48s % Output : CNFRefutation 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.08 % Problem : PUZ029-1 : TPTP v8.2.0. Released v1.0.0. % 0.02/0.08 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.27 % Computer : n032.cluster.edu % 0.09/0.27 % Model : x86_64 x86_64 % 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.27 % Memory : 8042.1875MB % 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.27 % CPULimit : 300 % 0.09/0.27 % WCLimit : 300 % 0.09/0.27 % DateTime : Tue Jun 18 09:53:54 EDT 2024 % 0.09/0.27 % CPUTime : % 0.13/0.45 start to proof:theBenchmark % 0.13/0.47 %------------------------------------------- % 0.13/0.47 % File :CSE---1.7 % 0.13/0.47 % Problem :theBenchmark % 0.13/0.47 % Transform :cnf % 0.13/0.47 % Format :tptp:raw % 0.13/0.47 % Command :java -jar mcs_scs.jar %d %s % 0.13/0.47 % 0.13/0.47 % Result :Theorem 0.000000s % 0.13/0.47 % Output :CNFRefutation 0.000000s % 0.13/0.47 %------------------------------------------- % 0.13/0.48 %-------------------------------------------------------------------------- % 0.13/0.48 % File : PUZ029-1 : TPTP v8.2.0. Released v1.0.0. % 0.13/0.48 % Domain : Puzzles % 0.13/0.48 % Problem : The pigs and balloons puzzle % 0.13/0.48 % Version : Especial. % 0.13/0.48 % English : 1) All, who neither dance on tight ropes nor eat penny-buns, % 0.13/0.48 % are old. % 0.13/0.48 % 2) Pigs, that are liable to giddiness, are treated with respect. % 0.13/0.48 % 3) A wise balloonist takes an umbrella with him. % 0.13/0.48 % 4) No one ought to lunch in public who looks ridiculous and eats % 0.13/0.48 % penny-buns. % 0.13/0.48 % 5) Young creatures, who go up in balloons, are liable to % 0.13/0.48 % giddiness. % 0.13/0.48 % 6) Fat creatures, who look ridiculous, may lunch in public, % 0.13/0.48 % provided that they do not dance on tight ropes. % 0.13/0.48 % 7) No wise creatures dance on tight ropes, if liable to % 0.13/0.48 % giddiness. % 0.13/0.48 % 8) A pig looks ridiculous, carrying an umbrella. % 0.13/0.48 % 9) All, who do not dance on tight ropes, and who are treated % 0.13/0.48 % with respect are fat. % 0.13/0.48 % Show that no wise young pigs go up in balloons. % 0.13/0.48 % 0.13/0.48 % Refs : [Car86] Carroll (1986), Lewis Carroll's Symbolic Logic % 0.13/0.48 % Source : [ANL] % 0.13/0.48 % Names : pigs.ver1.in [ANL] % 0.13/0.48 % 0.13/0.48 % Status : Unsatisfiable % 0.13/0.48 % Rating : 0.00 v2.0.0 % 0.13/0.48 % Syntax : Number of clauses : 15 ( 4 unt; 4 nHn; 13 RR) % 0.13/0.48 % Number of literals : 36 ( 0 equ; 19 neg) % 0.13/0.48 % Maximal clause size : 4 ( 2 avg) % 0.13/0.48 % Maximal term depth : 1 ( 1 avg) % 0.13/0.48 % Number of predicates : 13 ( 13 usr; 0 prp; 1-1 aty) % 0.13/0.48 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.13/0.48 % Number of variables : 11 ( 0 sgn) % 0.13/0.48 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.13/0.48 % 0.13/0.48 % Comments : % 0.13/0.48 %-------------------------------------------------------------------------- % 0.13/0.48 cnf(boring_old_people,axiom, % 0.13/0.48 ( dances_on_tightropes(X) % 0.13/0.48 | eats_pennybuns(X) % 0.13/0.48 | old(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(giddy_pigs_reated_with_respect,axiom, % 0.13/0.48 ( ~ pig(X) % 0.13/0.48 | ~ liable_to_giddiness(X) % 0.13/0.48 | treated_with_respect(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(wise_ballonists_have_umbrellas,axiom, % 0.13/0.48 ( ~ wise(X) % 0.13/0.48 | ~ balloonist(X) % 0.13/0.48 | has_umbrella(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(dont_look_ridiculous_eating_buns_in_public,axiom, % 0.13/0.48 ( ~ looks_ridiculous(X) % 0.13/0.48 | ~ eats_pennybuns(X) % 0.13/0.48 | ~ eats_lunch_in_public(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(young_balloonists_get_giddy,axiom, % 0.13/0.48 ( ~ balloonist(X) % 0.13/0.48 | ~ young(X) % 0.13/0.48 | liable_to_giddiness(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(fat_ridiculous_off_tightrope_eat_in_public,axiom, % 0.13/0.48 ( ~ fat(X) % 0.13/0.48 | ~ looks_ridiculous(X) % 0.13/0.48 | dances_on_tightropes(X) % 0.13/0.48 | eats_lunch_in_public(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(wise_giddy_dont_dance_on_tightrope,axiom, % 0.13/0.48 ( ~ liable_to_giddiness(X) % 0.13/0.48 | ~ wise(X) % 0.13/0.48 | ~ dances_on_tightropes(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(pigs_look_ridiculous_with_umbrellas,axiom, % 0.13/0.48 ( ~ pig(X) % 0.13/0.48 | ~ has_umbrella(X) % 0.13/0.48 | looks_ridiculous(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(non_dancers_who_are_respected_are_fat,axiom, % 0.13/0.48 ( dances_on_tightropes(X) % 0.13/0.48 | ~ treated_with_respect(X) % 0.13/0.48 | fat(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(young_or_old,axiom, % 0.13/0.48 ( young(X) % 0.13/0.48 | old(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(not_young_and_old,axiom, % 0.13/0.48 ( ~ young(X) % 0.13/0.48 | ~ old(X) ) ). % 0.13/0.48 % 0.13/0.48 cnf(piggy_is_wise,hypothesis, % 0.13/0.48 wise(piggy) ). % 0.13/0.48 % 0.13/0.48 cnf(piggy_is_young,hypothesis, % 0.13/0.48 young(piggy) ). % 0.13/0.48 % 0.13/0.48 cnf(piggy_is_a_pig,hypothesis, % 0.13/0.48 pig(piggy) ). % 0.13/0.48 % 0.13/0.48 cnf(prove_piggy_is_no_balloonist,negated_conjecture, % 0.13/0.48 balloonist(piggy) ). % 0.13/0.48 % 0.13/0.48 %-------------------------------------------------------------------------- % 0.13/0.48 %------------------------------------------- % 0.13/0.48 % Proof found % 0.13/0.48 % SZS status Theorem for theBenchmark % 0.13/0.48 % SZS output start Proof % 0.13/0.48 %ClaNum:15(EqnAxiom:0) % 0.13/0.48 %VarNum:32(SingletonVarNum:11) % 0.13/0.48 %MaxLitNum:4 % 0.13/0.48 %MaxfuncDepth:0 % 0.13/0.48 %SharedTerms:5 % 0.13/0.48 %goalClause: 3 % 0.13/0.48 %singleGoalClaCount:1 % 0.13/0.48 [1]P1(a1) % 0.13/0.48 [2]P11(a1) % 0.13/0.48 [3]P2(a1) % 0.13/0.48 [4]P13(a1) % 0.13/0.48 [5]P13(x51)+P3(x51) % 0.13/0.48 [7]~P13(x71)+~P3(x71) % 0.13/0.48 [6]P5(x61)+P3(x61)+P4(x61) % 0.13/0.48 [8]P7(x81)+~P12(x81)+P4(x81) % 0.13/0.48 [9]~P2(x91)+~P13(x91)+P8(x91) % 0.13/0.48 [10]~P1(x101)+~P8(x101)+P12(x101) % 0.13/0.48 [11]~P11(x111)+~P2(x111)+P9(x111) % 0.13/0.48 [12]~P1(x121)+~P9(x121)+P10(x121) % 0.13/0.48 [13]~P8(x131)+~P11(x131)+~P4(x131) % 0.13/0.48 [14]~P10(x141)+~P6(x141)+~P5(x141) % 0.13/0.48 [15]P6(x151)+~P10(x151)+~P7(x151)+P4(x151) % 0.13/0.48 %EqnAxiom % 0.13/0.48 % 0.13/0.48 %------------------------------------------- % 0.13/0.48 cnf(24,plain, % 0.13/0.48 (~P4(a1)), % 0.13/0.48 inference(scs_inference,[],[3,4,2,1,9,11,10,12,13])). % 0.13/0.48 cnf(30,plain, % 0.13/0.48 (~P5(a1)), % 0.13/0.48 inference(scs_inference,[],[3,4,2,1,9,11,10,12,13,8,15,14])). % 0.13/0.48 cnf(33,plain, % 0.13/0.48 ($false), % 0.13/0.48 inference(scs_inference,[],[24,30,4,6,7]), % 0.13/0.48 ['proof']). % 0.13/0.48 % SZS output end Proof % 0.13/0.48 % Total time :0.000000s %------------------------------------------------------------------------------