Gary is big. Gary is furry. Gary is kind. Gary is not round. Gary is white. Harry is big. Harry is white. All white things are big. Big things are green. If Harry is green and Harry is not white then Harry is not kind. If something is big and furry then it is kind. If something is green and not white then it is not kind. If something is round and white then it is not furry. If something is green then it is furry. If Gary is green then Gary is kind.
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Harry is green and Harry is not white then Harry is not kind.
((("Harry" "is" "green" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "kind" "-"))
If something is big and furry then it is kind.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is green and not white then it is not kind.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "kind" "-"))
If something is round and white then it is not furry.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "-"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Gary is green then Gary is kind.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "kind" "+"))
Gary is big.
True
1
proof
[(triple1 OR ((triple5) -> rule1))]
("Gary" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple5)]
("Gary" "is" "white" "-")
triple5
Gary is green.
True
2
proof
[(((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))]
("Gary" "is" "green" "+")
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Harry is not green.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((triple7) -> rule1)) -> rule2))]
("Harry" "is" "green" "-")
((triple6) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
True
3
proof
[(((((triple6) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))]
("Harry" "is" "furry" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not furry.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))]
("Harry" "is" "furry" "-")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is kind.
True
5
proof
[(((triple6 ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((triple6 ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4))]
("Harry" "is" "kind" "+")
((triple6 ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple7) -> (rule1 % int4)) ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((triple6 ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple7) -> (rule1 % int4)) ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not kind.
False
5
inv-proof
[(((triple6 ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((triple6 ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4))]
("Harry" "is" "kind" "-")
((triple6 ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple7) -> (rule1 % int4)) ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((triple6 ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple7) -> (rule1 % int4)) ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Gary is big.[(triple1 OR ((triple5) -> rule1))] Gary is furry.[(triple2 OR ((((triple1) -> rule2)) -> rule7) OR ((((((triple5) -> rule1)) -> rule2)) -> rule7))] Gary is kind.[(triple3 OR ((triple1 triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule8) OR ((((triple5) -> rule1) triple2) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule8) OR ((triple1 ((((triple1) -> rule2)) -> rule7)) -> rule4) OR ((((triple5) -> rule1) ((((triple1) -> rule2)) -> rule7)) -> rule4) OR ((triple1 ((((((triple5) -> rule1)) -> rule2)) -> rule7)) -> rule4) OR ((((triple5) -> rule1) ((((((triple5) -> rule1)) -> rule2)) -> rule7)) -> rule4))] Gary is not round.[(triple4)] Gary is white.[(triple5)] Harry is big.[(triple6 OR ((triple7) -> rule1))] Harry is white.[(triple7)] @1: Gary is green.[(((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] Harry is green.[(((triple6) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] @2: Harry is furry.[(((((triple6) -> rule2)) -> rule7) OR ((((((triple7) -> rule1)) -> rule2)) -> rule7))] @3: Harry is kind.[(((triple6 ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((triple6) -> rule2)) -> rule7)) -> rule4) OR ((triple6 ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4) OR ((((triple7) -> rule1) ((((((triple7) -> rule1)) -> rule2)) -> rule7)) -> rule4))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple1 triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple5) -> (rule1 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((triple1 ((((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is not round.
("Gary" "is" "round" "-")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple6) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((triple6 ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple7) -> (rule1 % int4)) ((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((triple6 ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple7) -> (rule1 % int4)) ((((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4