Anne is green. Dave is big. Dave is quiet. If Dave is green and Dave is big then Dave is kind. If someone is kind and big then they are rough. If someone is furry then they are big. If someone is furry then they are kind. Big people are green. All green, rough people are kind.
Anne is green.
("Anne" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If Dave is green and Dave is big then Dave is kind.
((("Dave" "is" "green" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If someone is kind and big then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All green, rough people are kind.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Dave is green.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "green" "+")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "green" "-")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule1))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule1))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
True
6
proof
[(((((((triple2) -> rule5) triple2) -> rule1) triple2) -> rule2))]
("Dave" "is" "rough" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((((((triple2) -> rule5) triple2) -> rule1) triple2) -> rule2))]
("Dave" "is" "rough" "-")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@3: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not rough.
Unknown
inv-rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is green.[(triple1)] Dave is big.[(triple2)] Dave is quiet.[(triple3)] @1: Dave is green.[(((triple2) -> rule5))] @2: Dave is kind.[(((((triple2) -> rule5) triple2) -> rule1))] @3: Dave is rough.[(((((((triple2) -> rule5) triple2) -> rule1) triple2) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3