Charlie is kind. Charlie is round. Charlie is smart. Charlie is white. Dave is blue. Dave is cold. Dave is kind. Dave is smart. Dave is white. Harry is blue. Harry is kind. Harry is rough. Harry is round. Harry is smart. Harry is white. Cold, smart people are white. Smart, round people are cold. If Charlie is cold and Charlie is kind then Charlie is rough.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Cold, smart people are white.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Smart, round people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is kind then Charlie is rough.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "rough" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple12)]
("Harry" "is" "rough" "-")
triple12
Harry is cold.
True
3
proof
[(((triple14 triple13) -> rule2))]
("Harry" "is" "cold" "+")
((triple14 triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
3
inv-proof
[(((triple14 triple13) -> rule2))]
("Harry" "is" "cold" "-")
((triple14 triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is rough.
True
5
proof
[(((((triple3 triple2) -> rule2) triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple3 triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not rough.
False
5
inv-proof
[(((((triple3 triple2) -> rule2) triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((((triple3 triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is kind.[(triple1)] Charlie is round.[(triple2)] Charlie is smart.[(triple3)] Charlie is white.[(triple4 OR ((((triple3 triple2) -> rule2) triple3) -> rule1))] Dave is blue.[(triple5)] Dave is cold.[(triple6)] Dave is kind.[(triple7)] Dave is smart.[(triple8)] Dave is white.[(triple9 OR ((triple6 triple8) -> rule1))] Harry is blue.[(triple10)] Harry is kind.[(triple11)] Harry is rough.[(triple12)] Harry is round.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15 OR ((((triple14 triple13) -> rule2) triple14) -> rule1))] @1: Charlie is cold.[(((triple3 triple2) -> rule2))] Harry is cold.[(((triple14 triple13) -> rule2))] @2: Charlie is rough.[(((((triple3 triple2) -> rule2) triple1) -> rule3))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((((triple3 triple2) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
((triple6 triple8) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((((triple14 triple13) -> (rule2 % int2)) triple14) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3 triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple14 triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3 triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2