Bob is cold. Bob is furry. Bob is kind. Bob is red. Bob is smart. Dave is furry. Harry is red. If something is rough then it is green. All red things are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple3)]
("Bob" "is" "kind" "-")
triple3
Bob is rough.
True
2
proof
[(((triple4) -> rule2))]
("Bob" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple4) -> rule2))]
("Bob" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is green.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("Harry" "is" "green" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is smart.[(triple5)] Dave is furry.[(triple6)] Harry is red.[(triple7)] @1: Bob is rough.[(((triple4) -> rule2))] Harry is rough.[(((triple7) -> rule2))] @2: Bob is green.[(((((triple4) -> rule2)) -> rule1))] Harry is green.[(((((triple7) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2