Anne is kind. Bob is big. Charlie is not smart. Red, smart people are green. Big people are nice. Kind, big people are nice. Cold, kind people are not nice. If Charlie is not big then Charlie is green. If someone is kind and green then they are not red. Big people are red. Green people are cold.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is big.
("Bob" "is" "big" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Red, smart people are green.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Kind, big people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Cold, kind people are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If Charlie is not big then Charlie is green.
((("Charlie" "is" "big" "~")) -> ("Charlie" "is" "green" "+"))
If someone is kind and green then they are not red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "-"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Charlie is not smart.
True
1
proof
[(triple3)]
("Charlie" "is" "smart" "-")
triple3
Bob is not big.
False
1
inv-proof
[(triple2)]
("Bob" "is" "big" "-")
triple2
Bob is red.
True
2
proof
[(((triple2) -> rule7))]
("Bob" "is" "red" "+")
((triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule7))]
("Bob" "is" "red" "-")
((triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is kind.[(triple1)] Bob is big.[(triple2)] Charlie is not smart.[(triple3)] @1: Bob is nice.[(((triple2) -> rule2))] Bob is red.[(((triple2) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1