Anne is big. Anne is furry. Anne is nice. Anne is red. Anne is young. Charlie is blue. Charlie is furry. Charlie is kind. Gary is big. Gary is red. Young, blue people are furry. If Gary is furry and Gary is young then Gary is red. Red people are young. All young people are big. Nice people are big. If someone is young then they are red. Young, big people are kind. Red people are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
Young, blue people are furry.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Gary is furry and Gary is young then Gary is red.
((("Gary" "is" "furry" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "red" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Young, big people are kind.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3) -> rule5) OR ((triple5) -> rule4) OR ((((triple4) -> rule3)) -> rule4))]
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule8) OR ((((triple5) -> rule6)) -> rule8))]
("Anne" "is" "furry" "-")
triple2
((triple4) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
True
3
proof
[(((triple5 triple1) -> rule7) OR ((triple5 ((triple3) -> rule5)) -> rule7) OR ((triple5 ((triple5) -> rule4)) -> rule7) OR ((((triple4) -> rule3) triple1) -> rule7) OR ((((triple4) -> rule3) ((triple3) -> rule5)) -> rule7) OR ((((triple4) -> rule3) ((triple5) -> rule4)) -> rule7) OR ((triple5 ((((triple4) -> rule3)) -> rule4)) -> rule7) OR ((((triple4) -> rule3) ((((triple4) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "kind" "+")
((triple5 triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple4) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple5 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not furry.
False
2
inv-proof
[(((triple10) -> rule8))]
("Gary" "is" "furry" "-")
((triple10) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
True
4
proof
[(((((triple10) -> rule3) triple9) -> rule7) OR ((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule4)) -> rule7))]
("Gary" "is" "kind" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not kind.
False
4
inv-proof
[(((((triple10) -> rule3) triple9) -> rule7) OR ((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule4)) -> rule7))]
("Gary" "is" "kind" "-")
((((triple10) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not big.
Unknown
inv-rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule5) OR ((triple5) -> rule4) OR ((((triple4) -> rule3)) -> rule4))] Anne is furry.[(triple2 OR ((triple4) -> rule8) OR ((((triple5) -> rule6)) -> rule8))] Anne is nice.[(triple3)] Anne is red.[(triple4 OR ((triple5) -> rule6))] Anne is young.[(triple5 OR ((triple4) -> rule3))] Charlie is blue.[(triple6)] Charlie is furry.[(triple7)] Charlie is kind.[(triple8)] Gary is big.[(triple9 OR ((((triple10) -> rule3)) -> rule4))] Gary is red.[(triple10)] @1: Anne is kind.[(((triple5 triple1) -> rule7) OR ((triple5 ((triple3) -> rule5)) -> rule7) OR ((triple5 ((triple5) -> rule4)) -> rule7) OR ((((triple4) -> rule3) triple1) -> rule7) OR ((((triple4) -> rule3) ((triple3) -> rule5)) -> rule7) OR ((((triple4) -> rule3) ((triple5) -> rule4)) -> rule7) OR ((triple5 ((((triple4) -> rule3)) -> rule4)) -> rule7) OR ((((triple4) -> rule3) ((((triple4) -> rule3)) -> rule4)) -> rule7))] Gary is furry.[(((triple10) -> rule8))] Gary is young.[(((triple10) -> rule3))] @2: Gary is kind.[(((((triple10) -> rule3) triple9) -> rule7) OR ((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule4)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple4) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple10
Anne is kind.
("Anne" "is" "kind" "+")
((triple5 triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple4) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple5 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((triple10) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple10) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3