Dave is cold. Dave is furry. Dave is young. Harry is big. Harry is blue. Harry is cold. Harry is young. Kind, smart people are cold. If someone is smart then they are young. If Dave is smart then Dave is big. Furry people are blue. If someone is cold then they are young. If someone is kind and smart then they are furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind, smart people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If Dave is smart then Dave is big.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "big" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and smart then they are furry.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Dave is young.
True
1
proof
[(triple3 OR ((triple1) -> rule5))]
("Dave" "is" "young" "+")
triple3
((triple1) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5))]
("Dave" "is" "young" "-")
triple3
((triple1) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2)] Dave is young.[(triple3 OR ((triple1) -> rule5))] Harry is big.[(triple4)] Harry is blue.[(triple5)] Harry is cold.[(triple6)] Harry is young.[(triple7 OR ((triple6) -> rule5))] @1: Dave is blue.[(((triple2) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
((triple1) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
((triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1