Anne is big. Anne is round. Dave is furry. Dave is kind. Gary is cold. Harry is furry. Harry is round. If Anne is cold then Anne is round. All furry people are cold. All cold, furry people are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If Anne is cold then Anne is round.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All cold, furry people are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Dave is not furry.
False
1
inv-proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Dave is cold.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "cold" "-")
((triple6) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is young.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule3))]
("Dave" "is" "young" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule3))]
("Dave" "is" "young" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "cold" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "young" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Gary is cold.[(triple5)] Harry is furry.[(triple6)] Harry is round.[(triple7)] @1: Dave is cold.[(((triple3) -> rule2))] Harry is cold.[(((triple6) -> rule2))] @2: Dave is young.[(((((triple3) -> rule2) triple3) -> rule3))] Harry is young.[(((((triple6) -> rule2) triple6) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2