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