Harry is red. If someone is green and red then they are cold. If Harry is red then Harry is cold. If someone is furry and red then they are green. If someone is cold then they are green. If Harry is cold then Harry is quiet. Quiet, nice people are blue.
Harry is red.
("Harry" "is" "red" "+")
If someone is green and red then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Harry is red then Harry is cold.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "cold" "+"))
If someone is furry and red then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If Harry is cold then Harry is quiet.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "quiet" "+"))
Quiet, nice people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Harry is red.
True
1
proof
[(triple1)]
("Harry" "is" "red" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple1)]
("Harry" "is" "red" "-")
triple1
Harry is cold.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Harry" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Harry" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Harry is red.[(triple1)] @1: Harry is cold.[(((triple1) -> rule2))] @2: Harry is green.[(((((triple1) -> rule2)) -> rule4))] Harry is quiet.[(((((triple1) -> rule2)) -> rule5))]
Harry is red.
("Harry" "is" "red" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2