Anne is red. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Gary is quiet. Gary is rough. If someone is smart then they are rough. If Anne is kind then Anne is big. Red, big people are nice. Nice people are rough. All smart, kind people are nice. If Gary is smart and Gary is quiet then Gary is nice. Rough people are nice. Nice, rough people are red.
Anne is red.
("Anne" "is" "red" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Anne is kind then Anne is big.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "big" "+"))
Red, big people are nice.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All smart, kind people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Gary is smart and Gary is quiet then Gary is nice.
((("Gary" "is" "smart" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Nice, rough people are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Gary is nice.
True
2
proof
[(((triple7) -> rule7))]
("Gary" "is" "nice" "+")
((triple7) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple7) -> rule7))]
("Gary" "is" "nice" "-")
((triple7) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is nice.
Unknown
rconc
[@4: Anne is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is red.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple3 ((triple3) -> rule4)) -> rule8))] Gary is quiet.[(triple6)] Gary is rough.[(triple7)] @1: Bob is rough.[(((triple3) -> rule4))] Gary is nice.[(((triple7) -> rule7))] @2: Gary is red.[(((((triple7) -> rule7) triple7) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple7) -> (rule7 % int2)) triple7) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2