Charlie is quiet. Charlie is rough. Harry is big. Harry is blue. Harry is kind. Harry is nice. Harry is quiet. If someone is rough and quiet then they are nice. All nice people are big. If Charlie is big then Charlie is kind.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is rough and quiet then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Charlie is big then Charlie is kind.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "kind" "+"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Charlie is nice.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Charlie" "is" "nice" "+")
((triple2 triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("Charlie" "is" "nice" "-")
((triple2 triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
True
4
proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
True
5
proof
[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "+")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "-")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is quiet.[(triple1)] Charlie is rough.[(triple2)] Harry is big.[(triple3 OR ((triple6) -> rule2))] Harry is blue.[(triple4)] Harry is kind.[(triple5)] Harry is nice.[(triple6)] Harry is quiet.[(triple7)] @1: Charlie is nice.[(((triple2 triple1) -> rule1))] @2: Charlie is big.[(((((triple2 triple1) -> rule1)) -> rule2))] @3: Charlie is kind.[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
((triple6) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2 triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3