Anne is furry. Anne is quiet. Anne is white. Charlie is furry. Charlie is nice. Charlie is white. Charlie is young. Erin is young. Gary is nice. Gary is young. All big, quiet things are young. If Charlie is red and Charlie is furry then Charlie is quiet. Big, red things are furry. Young, big things are white. Quiet, furry things are white. If something is quiet then it is big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
All big, quiet things are young.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Charlie is red and Charlie is furry then Charlie is quiet.
((("Charlie" "is" "red" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "quiet" "+"))
Big, red things are furry.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Young, big things are white.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Quiet, furry things are white.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Gary is nice.
True
1
proof
[(triple9)]
("Gary" "is" "nice" "+")
triple9
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3 OR ((triple2 triple1) -> rule5) OR ((((((triple2) -> rule6) triple2) -> rule1) ((triple2) -> rule6)) -> rule4))] Charlie is furry.[(triple4)] Charlie is nice.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7)] Erin is young.[(triple8)] Gary is nice.[(triple9)] Gary is young.[(triple10)] @1: Anne is big.[(((triple2) -> rule6))] @2: Anne is young.[(((((triple2) -> rule6) triple2) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple2 triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2)) ((triple2) -> (rule6 % int3))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2