Anne is blue. Anne is cold. Anne is green. Anne is kind. Anne is red. Anne is young. Charlie is cold. Charlie is kind. Charlie is red. Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is nice. Harry is red. Harry is young. Cold, red things are young. All green, young things are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold, red things are young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All green, young things are kind.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Anne is green.
True
1
proof
[(triple3)]
("Anne" "is" "green" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "kind" "-")
triple8
Charlie is young.
True
3
proof
[(((triple7 triple9) -> rule1))]
("Charlie" "is" "young" "+")
((triple7 triple9) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple7 triple9) -> rule1))]
("Charlie" "is" "young" "-")
((triple7 triple9) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4 OR ((triple3 triple6) -> rule2) OR ((triple3 ((triple2 triple5) -> rule1)) -> rule2))] Anne is red.[(triple5)] Anne is young.[(triple6 OR ((triple2 triple5) -> rule1))] Charlie is cold.[(triple7)] Charlie is kind.[(triple8)] Charlie is red.[(triple9)] Harry is blue.[(triple10)] Harry is cold.[(triple11)] Harry is green.[(triple12)] Harry is kind.[(triple13 OR ((triple12 triple16) -> rule2) OR ((triple12 ((triple11 triple15) -> rule1)) -> rule2))] Harry is nice.[(triple14)] Harry is red.[(triple15)] Harry is young.[(triple16 OR ((triple11 triple15) -> rule1))] @1: Charlie is young.[(((triple7 triple9) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple3 triple6) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple3 ((triple2 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple2 triple5) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
((triple12 triple16) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple12 ((triple11 triple15) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple11 triple15) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple7 triple9) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1