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