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