Charlie is white. Dave is quiet. Fiona is rough. If someone is rough then they are nice. White people are red. Quiet people are rough.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Dave is rough.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "-")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is nice.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Dave" "is" "nice" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is white.[(triple1)] Dave is quiet.[(triple2)] Fiona is rough.[(triple3)] @1: Charlie is red.[(((triple1) -> rule2))] Dave is rough.[(((triple2) -> rule3))] Fiona is nice.[(((triple3) -> rule1))] @2: Dave is nice.[(((((triple2) -> rule3)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2