Bob is nice. Gary is red. Gary is smart. All furry people are kind. All red people are kind. All blue people are nice. Furry people are red. All smart, kind people are blue. All kind people are round.
Bob is nice.
("Bob" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All smart, kind people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Gary is red.
True
1
proof
[(triple2)]
("Gary" "is" "red" "+")
triple2
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Gary is kind.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
True
4
proof
[(((triple3 ((triple2) -> rule2)) -> rule5))]
("Gary" "is" "blue" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not blue.
False
4
inv-proof
[(((triple3 ((triple2) -> rule2)) -> rule5))]
("Gary" "is" "blue" "-")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
True
5
proof
[(((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule3))]
("Gary" "is" "nice" "+")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not nice.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule3))]
("Gary" "is" "nice" "-")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is nice.[(triple1)] Gary is red.[(triple2)] Gary is smart.[(triple3)] @1: Gary is kind.[(((triple2) -> rule2))] @2: Gary is blue.[(((triple3 ((triple2) -> rule2)) -> rule5))] Gary is round.[(((((triple2) -> rule2)) -> rule6))] @3: Gary is nice.[(((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3