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