Charlie is red. Fiona is red. If Charlie is young and Charlie is smart then Charlie is red. If someone is quiet then they are young. All furry, big people are red. If Charlie is red then Charlie is quiet. All round people are big. If someone is big and round then they are quiet.
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Charlie is young and Charlie is smart then Charlie is red.
((("Charlie" "is" "young" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "red" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All furry, big people are red.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red then Charlie is quiet.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is big and round then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Fiona is red.
True
1
proof
[(triple2)]
("Fiona" "is" "red" "+")
triple2
Fiona is not red.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "red" "-")
triple2
Charlie is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is red.[(triple1)] Fiona is red.[(triple2)] @1: Charlie is quiet.[(((triple1) -> rule4))] @2: Charlie is young.[(((((triple1) -> rule4)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2