Dave is cold. Dave is rough. Erin is blue. Erin is cold. Erin is furry. Erin is rough. Erin is round. If Dave is rough then Dave is cold. All blue people are smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
If Dave is rough then Dave is cold.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "cold" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Erin is rough.
True
1
proof
[(triple6)]
("Erin" "is" "rough" "+")
triple6
Erin is not round.
False
1
inv-proof
[(triple7)]
("Erin" "is" "round" "-")
triple7
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is cold.[(triple1 OR ((triple2) -> rule1))] Dave is rough.[(triple2)] Erin is blue.[(triple3)] Erin is cold.[(triple4)] Erin is furry.[(triple5)] Erin is rough.[(triple6)] Erin is round.[(triple7)] @1: Erin is smart.[(((triple3) -> rule2))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1