Bob is cold. Bob is furry. Bob is not nice. Bob is red. Bob is not round. Dave is not cold. Dave is furry. Erin is blue. Erin is red. Harry is not big. Harry is blue. Harry is cold. Harry is furry. Harry is red. Harry is round. If someone is big then they are round. If someone is nice and blue then they are not red. If Dave is not furry then Dave is red. All blue people are cold. If someone is cold and not furry then they are big. If someone is blue and not furry then they are nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is not round.
("Bob" "is" "round" "-")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and blue then they are not red.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If Dave is not furry then Dave is red.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "red" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and not furry then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "big" "+"))
If someone is blue and not furry then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "+"))
Dave is not cold.
True
1
proof
[(triple6)]
("Dave" "is" "cold" "-")
triple6
Harry is not cold.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule4))]
("Harry" "is" "cold" "-")
triple12
((triple11) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is cold.
True
2
proof
[(((triple8) -> rule4))]
("Erin" "is" "cold" "+")
((triple8) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple8) -> rule4))]
("Erin" "is" "cold" "-")
((triple8) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is not nice.[(triple3)] Bob is not round.[(triple5)] Bob is red.[(triple4)] Dave is furry.[(triple7)] Dave is not cold.[(triple6)] Erin is blue.[(triple8)] Erin is red.[(triple9)] Harry is blue.[(triple11)] Harry is cold.[(triple12 OR ((triple11) -> rule4))] Harry is furry.[(triple13)] Harry is not big.[(triple10)] Harry is red.[(triple14)] Harry is round.[(triple15)] @1: Erin is cold.[(((triple8) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is not round.
("Bob" "is" "round" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is not cold.
("Dave" "is" "cold" "-")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple11) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is not big.
("Harry" "is" "big" "-")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Erin is cold.
("Erin" "is" "cold" "+")
((triple8) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1