Harry is furry. Harry is nice. Harry is not rough. If someone is green and blue then they are rough. All nice people are not green. If Harry is nice and Harry is not green then Harry is not big.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
If someone is green and blue then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All nice people are not green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
If Harry is nice and Harry is not green then Harry is not big.
((("Harry" "is" "nice" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "big" "-"))
Harry is furry.
True
1
proof
[(triple1)]
("Harry" "is" "furry" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple1)]
("Harry" "is" "furry" "-")
triple1
Harry is not green.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "green" "-")
((triple2) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is not big.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Harry" "is" "big" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Harry" "is" "big" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Harry is furry.[(triple1)] Harry is nice.[(triple2)] Harry is not rough.[(triple3)] @1: Harry is not green.[(((triple2) -> rule2))] @2: Harry is not big.[(((triple2 ((triple2) -> rule2)) -> rule3))]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is not rough.
("Harry" "is" "rough" "-")
triple3
Harry is not green.
("Harry" "is" "green" "-")
((triple2) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is not big.
("Harry" "is" "big" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2