Anne is green. Anne is nice. Charlie is furry. Gary is kind. Gary is nice. Harry is big. Harry is round. If someone is kind then they are red. Green people are round. If someone is kind then they are green. All kind people are green. Big people are nice. All big, nice people are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All big, nice people are kind.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple7 OR ((((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3)) -> rule2) OR ((((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule4)) -> rule2))]
("Harry" "is" "round" "-")
triple7
((((((triple6 ((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple6 ((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is nice.
True
2
proof
[(((triple6) -> rule5))]
("Harry" "is" "nice" "+")
((triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple4) -> rule4))]
("Gary" "is" "green" "-")
((triple4) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple4) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is kind.
True
4
proof
[(((triple6 ((triple6) -> rule5)) -> rule6))]
("Harry" "is" "kind" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))]
("Gary" "is" "round" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Harry is green.
True
5
proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3) OR ((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule4))]
("Harry" "is" "green" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule1))]
("Harry" "is" "red" "-")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "round" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Charlie is furry.[(triple3)] Gary is kind.[(triple4)] Gary is nice.[(triple5)] Harry is big.[(triple6)] Harry is round.[(triple7 OR ((((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3)) -> rule2) OR ((((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule4)) -> rule2))] @1: Anne is round.[(((triple1) -> rule2))] Gary is green.[(((triple4) -> rule3) OR ((triple4) -> rule4))] Gary is red.[(((triple4) -> rule1))] Harry is nice.[(((triple6) -> rule5))] @2: Gary is round.[(((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))] Harry is kind.[(((triple6 ((triple6) -> rule5)) -> rule6))] @3: Harry is green.[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule3) OR ((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule4))] Harry is red.[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
((((((triple6 ((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple6 ((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple4) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3