Anne is not blue. Anne is quiet. Dave is big. Dave is nice. Dave is quiet. Dave is white. Dave is young. Rough, young people are not white. All rough people are white. If someone is nice and not quiet then they are white. If Dave is big then Dave is white. If someone is white and big then they are blue. Rough people are nice. Rough, big people are nice. If someone is young then they are big.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Rough, young people are not white.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "-"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and not quiet then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "white" "+"))
If Dave is big then Dave is white.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "+"))
If someone is white and big then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Rough, big people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple4)]
("Dave" "is" "nice" "-")
triple4
Dave is blue.
True
3
proof
[(((triple6 triple3) -> rule5) OR ((triple6 ((triple7) -> rule8)) -> rule5) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple7) -> rule8)) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) ((triple7) -> rule8)) -> rule5))]
("Dave" "is" "blue" "+")
((triple6 triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) ((triple7) -> (rule8 % int3))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not blue.
False
3
inv-proof
[(((triple6 triple3) -> rule5) OR ((triple6 ((triple7) -> rule8)) -> rule5) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple7) -> rule8)) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) ((triple7) -> rule8)) -> rule5))]
("Dave" "is" "blue" "-")
((triple6 triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) ((triple7) -> (rule8 % int3))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "nice" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is not blue.[(triple1)] Anne is quiet.[(triple2)] Dave is big.[(triple3 OR ((triple7) -> rule8))] Dave is nice.[(triple4)] Dave is quiet.[(triple5)] Dave is white.[(triple6 OR ((triple3) -> rule4) OR ((((triple7) -> rule8)) -> rule4))] Dave is young.[(triple7)] @1: Dave is blue.[(((triple6 triple3) -> rule5) OR ((triple6 ((triple7) -> rule8)) -> rule5) OR ((((triple3) -> rule4) triple3) -> rule5) OR ((((triple3) -> rule4) ((triple7) -> rule8)) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) triple3) -> rule5) OR ((((((triple7) -> rule8)) -> rule4) ((triple7) -> rule8)) -> rule5))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
((triple7) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple3) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple6 triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple7) -> (rule8 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) ((triple7) -> (rule8 % int3))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3