Charlie is nice. Charlie is quiet. Dave is white. Dave is young. Fiona is young. Gary is quiet. Gary is round. If something is nice then it is white. Round things are nice.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is white.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "white" "+")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "white" "-")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is white.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Gary" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("Gary" "is" "white" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is nice.[(triple1)] Charlie is quiet.[(triple2)] Dave is white.[(triple3)] Dave is young.[(triple4)] Fiona is young.[(triple5)] Gary is quiet.[(triple6)] Gary is round.[(triple7)] @1: Charlie is white.[(((triple1) -> rule1))] Gary is nice.[(((triple7) -> rule2))] @2: Gary is white.[(((((triple7) -> rule2)) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2