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