Anne is furry. Anne is rough. Bob is kind. Bob is nice. Bob is white. Gary is furry. Gary is green. Gary is kind. Gary is nice. Gary is rough. Gary is white. Gary is young. If something is rough and young then it is nice. If Anne is young then Anne is white. If Gary is white then Gary is furry. If something is kind and rough then it is white. If something is white and kind then it is rough. All green things are young. If something is nice then it is young. If Anne is young and Anne is green then Anne is kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is rough and young then it is nice.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Anne is young then Anne is white.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "white" "+"))
If Gary is white then Gary is furry.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "furry" "+"))
If something is kind and rough then it is white.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is white and kind then it is rough.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Anne is young and Anne is green then Anne is kind.
((("Anne" "is" "young" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "kind" "+"))
Gary is nice.
True
1
proof
[(triple9 OR ((triple10 triple12) -> rule1) OR ((triple10 ((triple7) -> rule6)) -> rule1) OR ((((triple11 triple8) -> rule5) triple12) -> rule1) OR ((((triple11 triple8) -> rule5) ((triple7) -> rule6)) -> rule1))]
("Gary" "is" "nice" "+")
triple9
((triple10 triple12) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple10 ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple11 triple8) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple11 triple8) -> (rule5 % int3)) ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Bob is not nice.
False
1
inv-proof
[(triple4)]
("Bob" "is" "nice" "-")
triple4
Bob is young.
True
2
proof
[(((triple4) -> rule7))]
("Bob" "is" "young" "+")
((triple4) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not rough.
False
3
inv-proof
[(((triple5 triple3) -> rule5))]
("Bob" "is" "rough" "-")
((triple5 triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "kind" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is rough.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is white.[(triple5)] Gary is furry.[(triple6 OR ((triple11) -> rule3) OR ((((triple8 triple10) -> rule4)) -> rule3))] Gary is green.[(triple7)] Gary is kind.[(triple8)] Gary is nice.[(triple9 OR ((triple10 triple12) -> rule1) OR ((triple10 ((triple7) -> rule6)) -> rule1) OR ((((triple11 triple8) -> rule5) triple12) -> rule1) OR ((((triple11 triple8) -> rule5) ((triple7) -> rule6)) -> rule1))] Gary is rough.[(triple10 OR ((triple11 triple8) -> rule5))] Gary is white.[(triple11 OR ((triple8 triple10) -> rule4))] Gary is young.[(triple12 OR ((triple7) -> rule6) OR ((triple9) -> rule7))] @1: Bob is rough.[(((triple5 triple3) -> rule5))] Bob is young.[(((triple4) -> rule7))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8 triple10) -> (rule4 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple10 triple12) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple10 ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple11 triple8) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple11 triple8) -> (rule5 % int3)) ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple10
((triple11 triple8) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple11
((triple8 triple10) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple7) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple9) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple5 triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple4) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1