Bob is furry. Erin is furry. Gary is white. All white things are blue. If Erin is furry then Erin is smart. Green, red things are kind. Blue things are white. If Erin is kind then Erin is furry. All furry things are blue.
Bob is furry.
("Bob" "is" "furry" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is white.
("Gary" "is" "white" "+")
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Erin is furry then Erin is smart.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "smart" "+"))
Green, red things are kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Erin is kind then Erin is furry.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "furry" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Erin is smart.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "blue" "-")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Erin" "is" "white" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Erin is furry.[(triple2)] Gary is white.[(triple3)] @1: Bob is blue.[(((triple1) -> rule6))] Erin is blue.[(((triple2) -> rule6))] Erin is smart.[(((triple2) -> rule2))] Gary is blue.[(((triple3) -> rule1))] @2: Bob is white.[(((((triple1) -> rule6)) -> rule4))] Erin is white.[(((((triple2) -> rule6)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2