Bob is green. Bob is nice. Bob is quiet. Bob is not smart. Bob is not young. Charlie is green. Charlie is smart. Charlie is young. Dave is green. Dave is red. If someone is white and quiet then they are not nice. All red people are nice. If someone is green and nice then they are not young. If Bob is red and Bob is white then Bob is nice. All quiet people are red. If someone is quiet then they are green. If someone is quiet and not white then they are not green. If Charlie is not quiet and Charlie is not white then Charlie is not young.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
If someone is white and quiet then they are not nice.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is green and nice then they are not young.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
If Bob is red and Bob is white then Bob is nice.
((("Bob" "is" "red" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "nice" "+"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and not white then they are not green.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "-"))
If Charlie is not quiet and Charlie is not white then Charlie is not young.
((("Charlie" "is" "quiet" "~") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "young" "-"))
Bob is nice.
True
1
proof
[(triple2 OR ((((triple3) -> rule5)) -> rule2))]
("Bob" "is" "nice" "+")
triple2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
False
1
inv-proof
[(triple5 OR ((triple1 triple2) -> rule3) OR ((((triple3) -> rule6) triple2) -> rule3) OR ((triple1 ((((triple3) -> rule5)) -> rule2)) -> rule3) OR ((((triple3) -> rule6) ((((triple3) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "young" "+")
triple5
((triple1 triple2) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
((((triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is green.[(triple1 OR ((triple3) -> rule6))] Bob is nice.[(triple2 OR ((((triple3) -> rule5)) -> rule2))] Bob is not smart.[(triple4)] Bob is not young.[(triple5 OR ((triple1 triple2) -> rule3) OR ((((triple3) -> rule6) triple2) -> rule3) OR ((triple1 ((((triple3) -> rule5)) -> rule2)) -> rule3) OR ((((triple3) -> rule6) ((((triple3) -> rule5)) -> rule2)) -> rule3))] Bob is quiet.[(triple3)] Charlie is green.[(triple6)] Charlie is smart.[(triple7)] Charlie is young.[(triple8)] Dave is green.[(triple9)] Dave is red.[(triple10)] @1: Bob is red.[(((triple3) -> rule5))] Dave is nice.[(((triple10) -> rule2))] @2: Dave is not young.[(((triple9 ((triple10) -> rule2)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple3) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
((triple1 triple2) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
((((triple3) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple10) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple9 ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2