Anne is furry. Bob is nice. Charlie is blue. Gary is round. Round people are nice. Round, furry people are rough. Kind, blue people are round. If someone is furry then they are white. Furry people are kind. If someone is furry then they are blue. If Charlie is kind and Charlie is nice then Charlie is round. Kind people are round.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Round, furry people are rough.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Kind, blue people are round.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is kind and Charlie is nice then Charlie is round.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "round" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Anne is blue.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "blue" "-")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule5)) -> rule8) OR ((((triple1) -> rule5) ((triple1) -> rule6)) -> rule3))]
("Anne" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8) OR ((((triple1) -> rule5) ((triple1) -> rule6)) -> rule3))]
("Anne" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Bob is nice.[(triple2)] Charlie is blue.[(triple3)] Gary is round.[(triple4)] @1: Anne is blue.[(((triple1) -> rule6))] Anne is kind.[(((triple1) -> rule5))] Anne is white.[(((triple1) -> rule4))] Gary is nice.[(((triple4) -> rule1))] @2: Anne is round.[(((((triple1) -> rule5)) -> rule8) OR ((((triple1) -> rule5) ((triple1) -> rule6)) -> rule3))] @3: Anne is nice.[(((((((triple1) -> rule5)) -> rule8)) -> rule1) OR ((((((triple1) -> rule5) ((triple1) -> rule6)) -> rule3)) -> rule1))] Anne is rough.[(((((((triple1) -> rule5)) -> rule8) triple1) -> rule2) OR ((((((triple1) -> rule5) ((triple1) -> rule6)) -> rule3) triple1) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4