Anne is furry. Anne is kind. Bob is nice. Charlie is green. Charlie is rough. Gary is furry. Gary is nice. Nice, kind people are big. If Bob is big then Bob is kind. If someone is green then they are kind. If Gary is nice then Gary is green. If Charlie is nice and Charlie is kind then Charlie is rough. Rough people are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Nice, kind people are big.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Bob is big then Bob is kind.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "kind" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Gary is nice then Gary is green.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "green" "+"))
If Charlie is nice and Charlie is kind then Charlie is rough.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "rough" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "green" "-")
triple4
Charlie is kind.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "kind" "-")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "nice" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Bob is nice.[(triple3)] Charlie is green.[(triple4)] Charlie is rough.[(triple5)] Gary is furry.[(triple6)] Gary is nice.[(triple7)] @1: Charlie is kind.[(((triple4) -> rule3))] Charlie is nice.[(((triple5) -> rule6))] Gary is green.[(((triple7) -> rule4))] @2: Charlie is big.[(((((triple5) -> rule6) ((triple4) -> rule3)) -> rule1))] Gary is kind.[(((((triple7) -> rule4)) -> rule3))] @3: Gary is big.[(((triple7 ((((triple7) -> rule4)) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple5) -> (rule6 % int3)) ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple7 ((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3