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