Anne is big. Anne is cold. Anne is nice. Anne is not red. Anne is not rough. Bob is big. Bob is cold. Bob is not furry. Bob is nice. Bob is rough. Charlie is rough. Charlie is round. Red people are cold. All nice, round people are not cold. Nice, rough people are cold. All cold people are nice. If someone is nice and not cold then they are not big. If someone is nice and not cold then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is not rough.
("Anne" "is" "rough" "-")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All nice, round people are not cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
Nice, rough people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and not cold then they are not big.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "-"))
If someone is nice and not cold then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "+"))
Anne is not rough.
True
1
proof
[(triple5)]
("Anne" "is" "rough" "-")
triple5
Charlie is not rough.
False
1
inv-proof
[(triple11)]
("Charlie" "is" "rough" "-")
triple11
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3 OR ((triple2) -> rule4))] Anne is not red.[(triple4)] Anne is not rough.[(triple5)] Bob is big.[(triple6)] Bob is cold.[(triple7 OR ((triple9 triple10) -> rule3))] Bob is nice.[(triple9 OR ((triple7) -> rule4))] Bob is not furry.[(triple8)] Bob is rough.[(triple10)] Charlie is rough.[(triple11)] Charlie is round.[(triple12)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not red.
("Anne" "is" "red" "-")
triple4
Anne is not rough.
("Anne" "is" "rough" "-")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
((triple9 triple10) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple9
((triple7) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
triple8
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12