Dave is cold. Dave is furry. Dave is nice. Dave is smart. Erin is blue. Erin is cold. Erin is not green. Erin is nice. Erin is round. Erin is smart. All nice, smart things are furry. If something is cold then it is smart. If Dave is blue then Dave is round.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All nice, smart things are furry.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Dave is blue then Dave is round.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
Erin is cold.
True
1
proof
[(triple6)]
("Erin" "is" "cold" "+")
triple6
Erin is not cold.
False
1
inv-proof
[(triple6)]
("Erin" "is" "cold" "-")
triple6
Erin is furry.
True
3
proof
[(((triple8 triple10) -> rule1) OR ((triple8 ((triple6) -> rule2)) -> rule1))]
("Erin" "is" "furry" "+")
((triple8 triple10) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((triple8 triple10) -> rule1) OR ((triple8 ((triple6) -> rule2)) -> rule1))]
("Erin" "is" "furry" "-")
((triple8 triple10) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2 OR ((triple3 triple4) -> rule1) OR ((triple3 ((triple1) -> rule2)) -> rule1))] Dave is nice.[(triple3)] Dave is smart.[(triple4 OR ((triple1) -> rule2))] Erin is blue.[(triple5)] Erin is cold.[(triple6)] Erin is nice.[(triple8)] Erin is not green.[(triple7)] Erin is round.[(triple9)] Erin is smart.[(triple10 OR ((triple6) -> rule2))] @1: Erin is furry.[(((triple8 triple10) -> rule1) OR ((triple8 ((triple6) -> rule2)) -> rule1))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple3 triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is not green.
("Erin" "is" "green" "-")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
((triple6) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple8 triple10) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple8 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2