Anne is big. Anne is green. Anne is red. Anne is rough. Anne is smart. Dave is red. Dave is rough. If someone is red and big then they are young. All red people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If someone is red and big then they are young.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Anne is smart.
True
1
proof
[(triple5)]
("Anne" "is" "smart" "+")
triple5
Dave is not red.
False
1
inv-proof
[(triple6)]
("Dave" "is" "red" "-")
triple6
Dave is big.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "big" "+")
((triple6) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "big" "-")
((triple6) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
True
4
proof
[(((triple6 ((triple6) -> rule2)) -> rule1))]
("Dave" "is" "young" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not young.
False
4
inv-proof
[(((triple6 ((triple6) -> rule2)) -> rule1))]
("Dave" "is" "young" "-")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule2))] Anne is green.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5)] Dave is red.[(triple6)] Dave is rough.[(triple7)] @1: Anne is young.[(((triple3 triple1) -> rule1) OR ((triple3 ((triple3) -> rule2)) -> rule1))] Dave is big.[(((triple6) -> rule2))] @2: Dave is young.[(((triple6 ((triple6) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple6) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2