Anne is kind. Anne is quiet. Anne is white. Anne is young. Bob is rough. Bob is smart. Bob is white. Dave is quiet. Dave is young. Gary is white. If someone is quiet then they are green. All young, kind people are white. All quiet people are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All young, kind people are white.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple9)]
("Dave" "is" "young" "-")
triple9
Dave is kind.
True
2
proof
[(((triple8) -> rule3))]
("Dave" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "green" "-")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is white.
True
4
proof
[(((triple9 ((triple8) -> rule3)) -> rule2))]
("Dave" "is" "white" "+")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not white.
False
4
inv-proof
[(((triple9 ((triple8) -> rule3)) -> rule2))]
("Dave" "is" "white" "-")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is kind.[(triple1 OR ((triple2) -> rule3))] Anne is quiet.[(triple2)] Anne is white.[(triple3 OR ((triple4 triple1) -> rule2) OR ((triple4 ((triple2) -> rule3)) -> rule2))] Anne is young.[(triple4)] Bob is rough.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7)] Dave is quiet.[(triple8)] Dave is young.[(triple9)] Gary is white.[(triple10)] @1: Anne is green.[(((triple2) -> rule1))] Dave is green.[(((triple8) -> rule1))] Dave is kind.[(((triple8) -> rule3))] @2: Dave is white.[(((triple9 ((triple8) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple4 triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2