Anne is round. Bob is big. Charlie is nice. Harry is cold. All furry people are nice. If someone is red and big then they are cold. If someone is round then they are blue. If Anne is cold then Anne is big. If someone is nice and round then they are red. Red, big people are nice. If someone is cold then they are round. If someone is big then they are blue.
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and big then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Anne is cold then Anne is big.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "big" "+"))
If someone is nice and round then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red, big people are nice.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is blue.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "blue" "-")
((triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Charlie is red.
Unknown
rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is round.[(triple1)] Bob is big.[(triple2)] Charlie is nice.[(triple3)] Harry is cold.[(triple4)] @1: Anne is blue.[(((triple1) -> rule3))] Bob is blue.[(((triple2) -> rule8))] Harry is round.[(((triple4) -> rule7))] @2: Harry is blue.[(((((triple4) -> rule7)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2