Anne is red. Bob is nice. Dave is nice. Harry is smart. Nice people are red. If Dave is nice and Dave is red then Dave is smart.
Anne is red.
("Anne" "is" "red" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Dave is nice and Dave is red then Dave is smart.
((("Dave" "is" "nice" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "smart" "+"))
Bob is nice.
True
1
proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Dave is red.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "red" "+")
((triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "red" "-")
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is smart.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Dave" "is" "smart" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Dave" "is" "smart" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is red.[(triple1)] Bob is nice.[(triple2)] Dave is nice.[(triple3)] Harry is smart.[(triple4)] @1: Bob is red.[(((triple2) -> rule1))] Dave is red.[(((triple3) -> rule1))] @2: Dave is smart.[(((triple3 ((triple3) -> rule1)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2