Anne is rough. Anne is round. Dave is red. Smart people are blue. If someone is blue and smart then they are rough. If someone is red then they are smart.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and smart then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is smart.
True
2
proof
[(((triple3) -> rule3))]
("Dave" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
True
6
proof
[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
("Dave" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
("Dave" "is" "rough" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Dave is red.[(triple3)] @1: Dave is smart.[(((triple3) -> rule3))] @2: Dave is blue.[(((((triple3) -> rule3)) -> rule1))] @3: Dave is rough.[(((((((triple3) -> rule3)) -> rule1) ((triple3) -> rule3)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3