Anne is rough. Charlie is nice. Dave is white. Fiona is blue. White things are red. Red things are rough. If something is rough then it is smart.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Dave" "is" "smart" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Dave" "is" "smart" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is rough.[(triple1)] Charlie is nice.[(triple2)] Dave is white.[(triple3)] Fiona is blue.[(triple4)] @1: Anne is smart.[(((triple1) -> rule3))] Dave is red.[(((triple3) -> rule1))] @2: Dave is rough.[(((((triple3) -> rule1)) -> rule2))] @3: Dave is smart.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3