Dave is red. Harry is young. If Dave is red then Dave is furry. Big, round things are cold. Big, cold things are round. All cold things are furry. Red, kind things are big. All big, red things are young. All round, young things are red. If something is red then it is cold.
Dave is red.
("Dave" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is red then Dave is furry.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "+"))
Big, round things are cold.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Big, cold things are round.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Red, kind things are big.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All big, red things are young.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All round, young things are red.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Harry is young.
True
1
proof
[(triple2)]
("Harry" "is" "young" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple2)]
("Harry" "is" "young" "-")
triple2
Dave is furry.
True
2
proof
[(((triple1) -> rule1) OR ((((triple1) -> rule8)) -> rule4))]
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("Dave" "is" "cold" "-")
((triple1) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@4: Harry is cold.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule3 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is red.
Unknown
rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is red.[(triple1)] Harry is young.[(triple2)] @1: Dave is cold.[(((triple1) -> rule8))] Dave is furry.[(((triple1) -> rule1) OR ((((triple1) -> rule8)) -> rule4))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2