Bob is quiet. Dave is big. Dave is cold. Dave is nice. Dave is quiet. Dave is smart. Gary is big. Gary is furry. Gary is quiet. Gary is smart. Harry is furry. Harry is quiet. All smart people are round. Big, quiet people are cold. Round people are big. If someone is big then they are furry. If someone is round then they are smart. All cold, smart people are quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Big, quiet people are cold.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All cold, smart people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Dave is cold.
True
1
proof
[(triple3 OR ((triple2 triple5) -> rule2) OR ((((((triple6) -> rule1)) -> rule3) triple5) -> rule2))]
("Dave" "is" "cold" "+")
triple3
((triple2 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is not quiet.
False
1
inv-proof
[(triple9)]
("Gary" "is" "quiet" "-")
triple9
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Bob is quiet.[(triple1)] Dave is big.[(triple2 OR ((((triple6) -> rule1)) -> rule3))] Dave is cold.[(triple3 OR ((triple2 triple5) -> rule2) OR ((((((triple6) -> rule1)) -> rule3) triple5) -> rule2))] Dave is nice.[(triple4)] Dave is quiet.[(triple5 OR ((triple3 triple6) -> rule6))] Dave is smart.[(triple6)] Gary is big.[(triple7 OR ((((triple10) -> rule1)) -> rule3))] Gary is furry.[(triple8 OR ((triple7) -> rule4) OR ((((((triple10) -> rule1)) -> rule3)) -> rule4))] Gary is quiet.[(triple9)] Gary is smart.[(triple10)] Harry is furry.[(triple11)] Harry is quiet.[(triple12)] @1: Dave is furry.[(((triple2) -> rule4) OR ((((((triple6) -> rule1)) -> rule3)) -> rule4))] Dave is round.[(((triple6) -> rule1))] Gary is cold.[(((triple7 triple9) -> rule2) OR ((((((triple10) -> rule1)) -> rule3) triple9) -> rule2))] Gary is round.[(((triple10) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple2 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple3 triple6) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple7) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple7 triple9) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((triple10) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1