Dave is nice. Erin is kind. Fiona is furry. If Erin is furry and Erin is round then Erin is red. If something is round then it is blue. If something is nice then it is round.
Dave is nice.
("Dave" "is" "nice" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
If Erin is furry and Erin is round then Erin is red.
((("Erin" "is" "furry" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "red" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Dave is round.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "round" "+")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "round" "-")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is nice.[(triple1)] Erin is kind.[(triple2)] Fiona is furry.[(triple3)] @1: Dave is round.[(((triple1) -> rule3))] @2: Dave is blue.[(((((triple1) -> rule3)) -> rule2))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2