Anne is red. Bob is rough. Dave is nice. Harry is kind. Smart people are nice. If Anne is smart then Anne is rough. All red people are nice. If Anne is red and Anne is nice then Anne is kind. If Anne is big and Anne is quiet then Anne is red. If someone is big then they are red.
Anne is red.
("Anne" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Anne is smart then Anne is rough.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "rough" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Anne is red and Anne is nice then Anne is kind.
((("Anne" "is" "red" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
If Anne is big and Anne is quiet then Anne is red.
((("Anne" "is" "big" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "red" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Anne is nice.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("Anne" "is" "kind" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "red" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is red.[(triple1)] Bob is rough.[(triple2)] Dave is nice.[(triple3)] Harry is kind.[(triple4)] @1: Anne is nice.[(((triple1) -> rule3))] @2: Anne is kind.[(((triple1 ((triple1) -> rule3)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2