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