%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ003-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 : n004.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:00 EDT 2024 % Result : Unsatisfiable 58.48s 59.02s % Output : CNFRefutation 58.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : PUZ003-1 : TPTP v8.2.0. Released v1.0.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.16/0.31 % Computer : n004.cluster.edu % 0.16/0.31 % Model : x86_64 x86_64 % 0.16/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.31 % Memory : 8042.1875MB % 0.16/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.31 % CPULimit : 300 % 0.16/0.31 % WCLimit : 300 % 0.16/0.31 % DateTime : Tue Jun 18 10:31:39 EDT 2024 % 0.16/0.31 % CPUTime : % 0.16/0.52 start to proof:theBenchmark % 58.48/59.00 %------------------------------------------- % 58.48/59.00 % File :CSE---1.7 % 58.48/59.00 % Problem :theBenchmark % 58.48/59.00 % Transform :cnf % 58.48/59.00 % Format :tptp:raw % 58.48/59.00 % Command :java -jar mcs_scs.jar %d %s % 58.48/59.00 % 58.48/59.00 % Result :Theorem 58.000000s % 58.48/59.00 % Output :CNFRefutation 58.000000s % 58.48/59.00 %------------------------------------------- % 58.48/59.02 %-------------------------------------------------------------------------- % 58.48/59.02 % File : PUZ003-1 : TPTP v8.2.0. Released v1.0.0. % 58.48/59.02 % Domain : Puzzles % 58.48/59.02 % Problem : The Barber Puzzle % 58.48/59.02 % Version : Especial. % 58.48/59.02 % English : There is a barbers' club that obeys the following three % 58.48/59.02 % conditions: % 58.48/59.02 % (1) If any member A has shaved any other member B - whether % 58.48/59.02 % himself or another - then all members have shaved A, % 58.48/59.02 % though not necessarily at the same time. % 58.48/59.02 % (2) Four of the members are named Guido, Lorenzo, Petrucio, % 58.48/59.02 % and Cesare. % 58.48/59.02 % (3) Guido has shaved Cesare. % 58.48/59.02 % Prove Petrucio has shaved Lorenzo % 58.48/59.02 % 58.48/59.02 % Refs : % 58.48/59.02 % Source : [ANL] % 58.48/59.02 % Names : barber.ver1.in [ANL] % 58.48/59.02 % 58.48/59.02 % Status : Unsatisfiable % 58.48/59.02 % Rating : 0.00 v2.0.0 % 58.48/59.02 % Syntax : Number of clauses : 8 ( 6 unt; 0 nHn; 8 RR) % 58.48/59.02 % Number of literals : 13 ( 0 equ; 6 neg) % 58.48/59.02 % Maximal clause size : 4 ( 1 avg) % 58.48/59.02 % Maximal term depth : 1 ( 1 avg) % 58.48/59.02 % Number of predicates : 2 ( 2 usr; 0 prp; 1-2 aty) % 58.48/59.02 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 58.48/59.02 % Number of variables : 4 ( 0 sgn) % 58.48/59.02 % SPC : CNF_UNS_EPR_NEQ_HRN % 58.48/59.02 % 58.48/59.02 % Comments : % 58.48/59.02 %-------------------------------------------------------------------------- % 58.48/59.02 cnf(one_shaved_then_all_shaved,axiom, % 58.48/59.02 ( ~ member(X) % 58.48/59.02 | ~ member(Y) % 58.48/59.02 | ~ shaved(X,Y) % 58.48/59.02 | shaved(members,X) ) ). % 58.48/59.02 % 58.48/59.02 cnf(all_shaved_then_one_shaved,axiom, % 58.48/59.02 ( ~ shaved(members,X) % 58.48/59.02 | ~ member(Y) % 58.48/59.02 | shaved(Y,X) ) ). % 58.48/59.02 % 58.48/59.02 cnf(guido,hypothesis, % 58.48/59.02 member(guido) ). % 58.48/59.02 % 58.48/59.02 cnf(lorenzo,hypothesis, % 58.48/59.02 member(lorenzo) ). % 58.48/59.02 % 58.48/59.02 cnf(petruchio,hypothesis, % 58.48/59.02 member(petruchio) ). % 58.48/59.02 % 58.48/59.02 cnf(cesare,hypothesis, % 58.48/59.02 member(cesare) ). % 58.48/59.02 % 58.48/59.02 cnf(guido_has_shaved_cesare,hypothesis, % 58.48/59.02 shaved(guido,cesare) ). % 58.48/59.02 % 58.48/59.02 cnf(prove_petruchio_has_shaved_lorenzo,negated_conjecture, % 58.48/59.02 ~ shaved(petruchio,lorenzo) ). % 58.48/59.02 % 58.48/59.02 %-------------------------------------------------------------------------- % 58.48/59.02 %------------------------------------------- % 58.48/59.02 % Proof found % 58.48/59.02 % SZS status Theorem for theBenchmark % 58.48/59.02 % SZS output start Proof % 58.48/59.03 %ClaNum:8(EqnAxiom:0) % 58.48/59.03 %VarNum:9(SingletonVarNum:4) % 58.48/59.03 %MaxLitNum:4 % 58.48/59.03 %MaxfuncDepth:0 % 58.48/59.03 %SharedTerms:11 % 58.48/59.03 %goalClause: 6 % 58.48/59.03 %singleGoalClaCount:1 % 58.48/59.03 [1]P1(a1) % 58.48/59.03 [2]P1(a3) % 58.48/59.03 [3]P1(a4) % 58.48/59.03 [4]P1(a2) % 58.48/59.03 [5]P2(a1,a2) % 58.48/59.03 [6]~P2(a4,a3) % 58.48/59.03 [7]~P1(x71)+P2(x71,x72)+~P2(a5,x72) % 58.48/59.03 [8]~P1(x81)+~P2(x81,x82)+~P1(x82)+P2(a5,x81) % 58.48/59.03 %EqnAxiom % 58.48/59.03 % 58.48/59.03 %------------------------------------------- % 58.48/59.04 cnf(10,plain, % 58.48/59.04 (~P2(a3,a4)), % 58.48/59.04 inference(scs_inference,[],[3,6,2,7,8])). % 58.48/59.04 cnf(12,plain, % 58.48/59.04 (P2(a1,a1)), % 58.48/59.04 inference(scs_inference,[],[1,5,4,7,8])). % 58.48/59.04 cnf(19,plain, % 58.48/59.04 (P2(a5,a1)), % 58.48/59.04 inference(scs_inference,[],[1,10,12,2,7,8])). % 58.48/59.04 cnf(21,plain, % 58.48/59.04 (~P2(a5,a3)), % 58.48/59.04 inference(scs_inference,[],[6,3,7])). % 58.48/59.04 cnf(29,plain, % 58.48/59.04 ($false), % 58.48/59.04 inference(scs_inference,[],[2,19,1,21,7,8]), % 58.48/59.04 ['proof']). % 58.48/59.04 % SZS output end Proof % 58.48/59.04 % Total time :58.000000s %------------------------------------------------------------------------------