Anne is not furry. Anne is green. Anne is kind. Dave is big. Dave is furry. Dave is not green. Dave is kind. Dave is not quiet. Gary is big. Gary is green. Gary is nice. Harry is not big. All kind, big people are white. If Dave is furry and Dave is not big then Dave is not green. All green people are nice. Green people are kind. Green people are quiet. If Dave is nice then Dave is not furry.
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is not big.
("Harry" "is" "big" "-")
All kind, big people are white.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Dave is furry and Dave is not big then Dave is not green.
((("Dave" "is" "furry" "+") ("Dave" "is" "big" "~")) -> ("Dave" "is" "green" "-"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is nice then Dave is not furry.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "furry" "-"))
Dave is not quiet.
True
1
proof
[(triple8)]
("Dave" "is" "quiet" "-")
triple8
Dave is not kind.
False
1
inv-proof
[(triple7)]
("Dave" "is" "kind" "-")
triple7
Anne is quiet.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Gary is white.
True
4
proof
[(((((triple10) -> rule4) triple9) -> rule1))]
("Gary" "is" "white" "+")
((((triple10) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not white.
False
4
inv-proof
[(((((triple10) -> rule4) triple9) -> rule1))]
("Gary" "is" "white" "-")
((((triple10) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple2) -> rule4))] Anne is not furry.[(triple1)] Dave is big.[(triple4)] Dave is furry.[(triple5)] Dave is kind.[(triple7)] Dave is not green.[(triple6)] Dave is not quiet.[(triple8)] Gary is big.[(triple9)] Gary is green.[(triple10)] Gary is nice.[(triple11 OR ((triple10) -> rule3))] Harry is not big.[(triple12)] @1: Anne is nice.[(((triple2) -> rule3))] Anne is quiet.[(((triple2) -> rule5))] Dave is white.[(((triple7 triple4) -> rule1))] Gary is kind.[(((triple10) -> rule4))] Gary is quiet.[(((triple10) -> rule5))] @2: Gary is white.[(((((triple10) -> rule4) triple9) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple11
((triple10) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
triple12
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple7 triple4) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple10) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2