Erin is green. Harry is cold. Harry is red. Cold, red things are furry. If something is furry then it is young. If Harry is cold then Harry is furry.
Erin is green.
("Erin" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Cold, red things are furry.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If Harry is cold then Harry is furry.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
Harry is furry.
True
2
proof
[(((triple2) -> rule3) OR ((triple2 triple3) -> rule1))]
("Harry" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2 triple3) -> rule1))]
("Harry" "is" "furry" "-")
((triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
True
3
proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2))]
("Harry" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2))]
("Harry" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Erin is green.[(triple1)] Harry is cold.[(triple2)] Harry is red.[(triple3)] @1: Harry is furry.[(((triple2) -> rule3) OR ((triple2 triple3) -> rule1))] @2: Harry is young.[(((((triple2) -> rule3)) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2