Charlie is big. Charlie is cold. Charlie is kind. Charlie is white. Dave is big. Dave is cold. Dave is kind. Dave is nice. Dave is red. Dave is round. Dave is white. Gary is not big. Gary is kind. Gary is nice. Gary is red. Gary is round. If Gary is cold then Gary is nice. Kind people are red. Red people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Gary is cold then Gary is nice.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "nice" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Charlie is white.
True
1
proof
[(triple4)]
("Charlie" "is" "white" "+")
triple4
Charlie is not white.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "white" "-")
triple4
Charlie is red.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "red" "+")
((triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "red" "-")
((triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is kind.[(triple3)] Charlie is white.[(triple4)] Dave is big.[(triple5)] Dave is cold.[(triple6)] Dave is kind.[(triple7)] Dave is nice.[(triple8 OR ((triple9) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] Dave is red.[(triple9 OR ((triple7) -> rule2))] Dave is round.[(triple10)] Dave is white.[(triple11)] Gary is kind.[(triple13)] Gary is nice.[(triple14 OR ((triple15) -> rule3) OR ((((triple13) -> rule2)) -> rule3))] Gary is not big.[(triple12)] Gary is red.[(triple15 OR ((triple13) -> rule2))] Gary is round.[(triple16)] @1: Charlie is red.[(((triple3) -> rule2))] @2: Charlie is nice.[(((((triple3) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple9) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is nice.
("Gary" "is" "nice" "+")
triple14
((triple15) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not big.
("Gary" "is" "big" "-")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple15
((triple13) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple16
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2