Anne is big. Anne is cold. Anne is furry. Anne is red. Anne is smart. Dave is not blue. Dave is not furry. Gary is not big. Gary is cold. Gary is round. If someone is smart then they are round. If someone is smart and not round then they are cold. If Dave is not round and Dave is not blue then Dave is not cold. If Gary is big and Gary is smart then Gary is blue. If someone is big then they are red. Cold, big people are red. If someone is cold and smart then they are big. Blue people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Gary is not big.
("Gary" "is" "big" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and not round then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "+"))
If Dave is not round and Dave is not blue then Dave is not cold.
((("Dave" "is" "round" "~") ("Dave" "is" "blue" "~")) -> ("Dave" "is" "cold" "-"))
If Gary is big and Gary is smart then Gary is blue.
((("Gary" "is" "big" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "blue" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Cold, big people are red.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and smart then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Anne is furry.
True
1
proof
[(triple3)]
("Anne" "is" "furry" "+")
triple3
Gary is big.
False
1
inv-proof
[(triple8)]
("Gary" "is" "big" "+")
triple8
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Dave" "is" "red" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1 OR ((triple2 triple5) -> rule7))] Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is red.[(triple4 OR ((triple1) -> rule5) OR ((triple2 triple1) -> rule6) OR ((((triple2 triple5) -> rule7)) -> rule5) OR ((triple2 ((triple2 triple5) -> rule7)) -> rule6))] Anne is smart.[(triple5)] Dave is not blue.[(triple6)] Dave is not furry.[(triple7)] Gary is cold.[(triple9)] Gary is not big.[(triple8)] Gary is round.[(triple10)] @1: Anne is round.[(((triple5) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple5) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2 triple5) -> (rule7 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple2 ((triple2 triple5) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple6
Dave is not furry.
("Dave" "is" "furry" "-")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is not big.
("Gary" "is" "big" "-")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple5) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1