Anne is not big. Anne is furry. Anne is green. Anne is not nice. Anne is rough. Anne is not smart. Anne is white. Gary is nice. Gary is rough. Gary is smart. Harry is big. Harry is not green. If Harry is white and Harry is big then Harry is not rough. If something is big then it is white. All furry, nice things are big.
Anne is not big.
("Anne" "is" "big" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not green.
("Harry" "is" "green" "-")
If Harry is white and Harry is big then Harry is not rough.
((("Harry" "is" "white" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "rough" "-"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All furry, nice things are big.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple11)]
("Harry" "is" "big" "+")
triple11
Anne is not rough.
False
1
inv-proof
[(triple5)]
("Anne" "is" "rough" "-")
triple5
Harry is white.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "white" "+")
((triple11) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "white" "-")
((triple11) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not rough.
True
4
proof
[(((((triple11) -> rule2) triple11) -> rule1))]
("Harry" "is" "rough" "-")
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
False
4
inv-proof
[(((((triple11) -> rule2) triple11) -> rule1))]
("Harry" "is" "rough" "+")
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Gary" "is" "white" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is not big.[(triple1)] Anne is not nice.[(triple4)] Anne is not smart.[(triple6)] Anne is rough.[(triple5)] Anne is white.[(triple7)] Gary is nice.[(triple8)] Gary is rough.[(triple9)] Gary is smart.[(triple10)] Harry is big.[(triple11)] Harry is not green.[(triple12)] @1: Harry is white.[(((triple11) -> rule2))] @2: Harry is not rough.[(((((triple11) -> rule2) triple11) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple4
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is not green.
("Harry" "is" "green" "-")
triple12
Harry is white.
("Harry" "is" "white" "+")
((triple11) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2