Bob is red. Dave is nice. All quiet, red people are kind. All nice, green people are kind. If someone is red and not big then they are not green. If someone is nice then they are green. If Bob is quiet then Bob is nice. If Dave is kind then Dave is not quiet.
Bob is red.
("Bob" "is" "red" "+")
Dave is nice.
("Dave" "is" "nice" "+")
All quiet, red people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All nice, green people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not big then they are not green.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "-"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Bob is quiet then Bob is nice.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "nice" "+"))
If Dave is kind then Dave is not quiet.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "quiet" "-"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "-")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule2))]
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule2))]
("Dave" "is" "kind" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
True
5
proof
[(((((triple2 ((triple2) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "quiet" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is quiet.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "quiet" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is red.[(triple1)] Dave is nice.[(triple2)] @1: Dave is green.[(((triple2) -> rule4))] @2: Dave is kind.[(((triple2 ((triple2) -> rule4)) -> rule2))] @3: Dave is not quiet.[(((((triple2 ((triple2) -> rule4)) -> rule2)) -> rule6))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3