Anne is big. Anne is furry. Anne is not quiet. Anne is red. Anne is round. Charlie is big. Charlie is not furry. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is not round. Gary is big. Gary is furry. Gary is kind. Gary is red. Gary is round. If Charlie is big then Charlie is red. Red, round things are cold. If Anne is cold then Anne is round. If Anne is kind then Anne is big. If Anne is cold then Anne is kind. If Charlie is not big and Charlie is not red then Charlie is kind. If something is big and not red then it is round. Quiet, red things are not round.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Charlie is big then Charlie is red.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
Red, round things are cold.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If Anne is cold then Anne is round.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
If Anne is kind then Anne is big.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "big" "+"))
If Anne is cold then Anne is kind.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "kind" "+"))
If Charlie is not big and Charlie is not red then Charlie is kind.
((("Charlie" "is" "big" "~") ("Charlie" "is" "red" "~")) -> ("Charlie" "is" "kind" "+"))
If something is big and not red then it is round.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "+"))
Quiet, red things are not round.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
Charlie is kind.
True
1
proof
[(triple8)]
("Charlie" "is" "kind" "+")
triple8
Gary is not big.
False
1
inv-proof
[(triple12)]
("Gary" "is" "big" "-")
triple12
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is big.[(triple1 OR ((((((triple4 triple5) -> rule2)) -> rule5)) -> rule4))] Anne is furry.[(triple2)] Anne is not quiet.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5)] Charlie is big.[(triple6)] Charlie is kind.[(triple8)] Charlie is not furry.[(triple7)] Charlie is not round.[(triple11 OR ((triple9 triple10) -> rule8) OR ((triple9 ((triple6) -> rule1)) -> rule8))] Charlie is quiet.[(triple9)] Charlie is red.[(triple10 OR ((triple6) -> rule1))] Gary is big.[(triple12)] Gary is furry.[(triple13)] Gary is kind.[(triple14)] Gary is red.[(triple15)] Gary is round.[(triple16)] @1: Anne is cold.[(((triple4 triple5) -> rule2))] Gary is cold.[(((triple15 triple16) -> rule2))] @2: Anne is kind.[(((((triple4 triple5) -> rule2)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((((triple4 triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple7
Charlie is not round.
("Charlie" "is" "round" "-")
triple11
((triple9 triple10) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
((triple9 ((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple6) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is red.
("Gary" "is" "red" "+")
triple15
Gary is round.
("Gary" "is" "round" "+")
triple16
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple5) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple15 triple16) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2