Charlie is cold. Charlie is green. Charlie is quiet. Charlie is white. Harry is big. Harry is cold. Harry is kind. Harry is nice. Harry is quiet. Harry is white. White people are nice. If someone is kind then they are white. If Charlie is cold then Charlie is white. If someone is green then they are white. If Charlie is kind then Charlie is white. If Charlie is kind then Charlie is quiet.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Charlie is kind then Charlie is white.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is kind then Charlie is quiet.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Harry is not nice.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule1) OR ((((triple7) -> rule2)) -> rule1))]
("Harry" "is" "nice" "-")
triple8
((triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is nice.
True
2
proof
[(((triple4) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not nice.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("Charlie" "is" "nice" "-")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Charlie is quiet.[(triple3)] Charlie is white.[(triple4 OR ((triple1) -> rule3) OR ((triple2) -> rule4))] Harry is big.[(triple5)] Harry is cold.[(triple6)] Harry is kind.[(triple7)] Harry is nice.[(triple8 OR ((triple10) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Harry is quiet.[(triple9)] Harry is white.[(triple10 OR ((triple7) -> rule2))] @1: Charlie is nice.[(((triple4) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2