Anne is blue. Anne is green. Anne is nice. Anne is red. Anne is smart. Charlie is blue. Charlie is green. Charlie is nice. Charlie is quiet. Gary is blue. Gary is green. Gary is nice. Gary is quiet. Gary is red. Gary is smart. Gary is young. If something is young and red then it is nice. If something is blue then it is green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young and red then it is nice.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Gary is green.
True
1
proof
[(triple11 OR ((triple10) -> rule2))]
("Gary" "is" "green" "+")
triple11
((triple10) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple15)]
("Gary" "is" "smart" "-")
triple15
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule2))] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is smart.[(triple5)] Charlie is blue.[(triple6)] Charlie is green.[(triple7 OR ((triple6) -> rule2))] Charlie is nice.[(triple8)] Charlie is quiet.[(triple9)] Gary is blue.[(triple10)] Gary is green.[(triple11 OR ((triple10) -> rule2))] Gary is nice.[(triple12 OR ((triple16 triple14) -> rule1))] Gary is quiet.[(triple13)] Gary is red.[(triple14)] Gary is smart.[(triple15)] Gary is young.[(triple16)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
((triple6) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
((triple10) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple12
((triple16 triple14) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16