Dave is big. Dave is cold. Dave is furry. Dave is green. Dave is kind. Erin is green. Harry is big. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is round. If something is kind and big then it is round. If Harry is furry then Harry is cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is kind and big then it is round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Harry is furry then Harry is cold.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "cold" "+"))
Harry is kind.
True
1
proof
[(triple11)]
("Harry" "is" "kind" "+")
triple11
Harry is not round.
False
1
inv-proof
[(triple12 OR ((triple11 triple7) -> rule1))]
("Harry" "is" "round" "-")
triple12
((triple11 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is round.
True
3
proof
[(((triple5 triple1) -> rule1))]
("Dave" "is" "round" "+")
((triple5 triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple5 triple1) -> rule1))]
("Dave" "is" "round" "-")
((triple5 triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is green.[(triple4)] Dave is kind.[(triple5)] Erin is green.[(triple6)] Harry is big.[(triple7)] Harry is cold.[(triple8 OR ((triple9) -> rule2))] Harry is furry.[(triple9)] Harry is green.[(triple10)] Harry is kind.[(triple11)] Harry is round.[(triple12 OR ((triple11 triple7) -> rule1))] @1: Dave is round.[(((triple5 triple1) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple9) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple11 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5 triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1