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