Dave is kind. Erin is red. Fiona is not red. Kind people are round. Blue people are round. If Erin is kind and Erin is round then Erin is not quiet. If someone is cold and not big then they are blue. If someone is red then they are not blue. Round people are quiet. If someone is big and not red then they are not quiet. If Fiona is not blue and Fiona is not round then Fiona is quiet.
Dave is kind.
("Dave" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Erin is kind and Erin is round then Erin is not quiet.
((("Erin" "is" "kind" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "quiet" "-"))
If someone is cold and not big then they are blue.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "blue" "+"))
If someone is red then they are not blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "-"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and not red then they are not quiet.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "quiet" "-"))
If Fiona is not blue and Fiona is not round then Fiona is quiet.
((("Fiona" "is" "blue" "~") ("Fiona" "is" "round" "~")) -> ("Fiona" "is" "quiet" "+"))
Fiona is not red.
True
1
proof
[(triple3)]
("Fiona" "is" "red" "-")
triple3
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Dave is round.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("Erin" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "blue" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Dave is kind.[(triple1)] Erin is red.[(triple2)] Fiona is not red.[(triple3)] @1: Dave is round.[(((triple1) -> rule1))] Erin is not blue.[(((triple2) -> rule5))] @2: Dave is quiet.[(((((triple1) -> rule1)) -> rule6))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is not red.
("Fiona" "is" "red" "-")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
((triple2) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2