Bob is blue. Bob is not green. Bob is kind. Bob is round. Bob is white. Dave is furry. Gary is furry. Gary is green. Gary is round. Gary is not white. All furry people are quiet. If someone is white and not furry then they are blue. All quiet people are blue. If someone is quiet and not furry then they are not green. If someone is kind and not quiet then they are not green. Quiet, white people are green. All blue people are kind. If someone is round and not quiet then they are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and not furry then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "blue" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and not furry then they are not green.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "-"))
If someone is kind and not quiet then they are not green.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "green" "-"))
Quiet, white people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and not quiet then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "kind" "+"))
Bob is not green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Bob is not white.
False
1
inv-proof
[(triple5)]
("Bob" "is" "white" "-")
triple5
Gary is quiet.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple7) -> rule1))]
("Gary" "is" "quiet" "-")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple3 OR ((triple1) -> rule7))] Bob is not green.[(triple2)] Bob is round.[(triple4)] Bob is white.[(triple5)] Dave is furry.[(triple6)] Gary is furry.[(triple7)] Gary is green.[(triple8)] Gary is not white.[(triple10)] Gary is round.[(triple9)] @1: Dave is quiet.[(((triple6) -> rule1))] Gary is quiet.[(((triple7) -> rule1))] @2: Dave is blue.[(((((triple6) -> rule1)) -> rule3))] Gary is blue.[(((((triple7) -> rule1)) -> rule3))] @3: Dave is kind.[(((((((triple6) -> rule1)) -> rule3)) -> rule7))] Gary is kind.[(((((((triple7) -> rule1)) -> rule3)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is not white.
("Gary" "is" "white" "-")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3