Charlie is round. Erin is young. Fiona is kind. If something is quiet and kind then it is red. If something is kind then it is red. Red things are quiet.
Charlie is round.
("Charlie" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If something is quiet and kind then it is red.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Erin is young.
True
1
proof
[(triple2)]
("Erin" "is" "young" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple2)]
("Erin" "is" "young" "-")
triple2
Fiona is red.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "red" "+")
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Fiona" "is" "red" "-")
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule2 % 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
[(((((triple3) -> rule2)) -> rule3))]
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is round.[(triple1)] Erin is young.[(triple2)] Fiona is kind.[(triple3)] @1: Fiona is red.[(((triple3) -> rule2))] @2: Fiona is quiet.[(((((triple3) -> rule2)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2