Charlie is not kind. Charlie is nice. Charlie is smart. Harry is big. Harry is kind. Harry is not red. Harry is rough. If Charlie is kind and Charlie is rough then Charlie is not nice. Big, kind people are nice. All blue people are not smart. Nice people are smart. If Harry is big and Harry is blue then Harry is rough. If Harry is kind and Harry is not red then Harry is big.
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
If Charlie is kind and Charlie is rough then Charlie is not nice.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "nice" "-"))
Big, kind people are nice.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All blue people are not smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "-"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Harry is big and Harry is blue then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is kind and Harry is not red then Harry is big.
((("Harry" "is" "kind" "+") ("Harry" "is" "red" "~")) -> ("Harry" "is" "big" "+"))
Charlie is smart.
True
1
proof
[(triple3 OR ((triple2) -> rule4))]
("Charlie" "is" "smart" "+")
triple3
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is not big.
False
1
inv-proof
[(triple4 OR ((triple5 triple6) -> rule6))]
("Harry" "is" "big" "-")
triple4
((triple5 triple6) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
True
3
proof
[(((triple4 triple5) -> rule2) OR ((((triple5 triple6) -> rule6) triple5) -> rule2))]
("Harry" "is" "nice" "+")
((triple4 triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule6 % int2)) triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((triple4 triple5) -> rule2) OR ((((triple5 triple6) -> rule6) triple5) -> rule2))]
("Harry" "is" "nice" "-")
((triple4 triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule6 % int2)) triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is nice.[(triple2)] Charlie is not kind.[(triple1)] Charlie is smart.[(triple3 OR ((triple2) -> rule4))] Harry is big.[(triple4 OR ((triple5 triple6) -> rule6))] Harry is kind.[(triple5)] Harry is not red.[(triple6)] Harry is rough.[(triple7)] @1: Harry is nice.[(((triple4 triple5) -> rule2) OR ((((triple5 triple6) -> rule6) triple5) -> rule2))] @2: Harry is smart.[(((((triple4 triple5) -> rule2)) -> rule4) OR ((((((triple5 triple6) -> rule6) triple5) -> rule2)) -> rule4))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple4
((triple5 triple6) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is not red.
("Harry" "is" "red" "-")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
((triple4 triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5 triple6) -> (rule6 % int2)) triple5) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple5 triple6) -> (rule6 % int3)) triple5) -> (rule2 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3