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