Anne is cold. Anne is quiet. Anne is rough. Anne is young. Bob is green. Bob is kind. Bob is not red. Bob is not young. Dave is cold. Dave is kind. Dave is not rough. Dave is young. Gary is not cold. Gary is kind. Gary is quiet. Gary is not young. If someone is cold then they are not green. If someone is kind and not green then they are not red. Quiet, cold people are not red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is not young.
("Bob" "is" "young" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is young.
("Dave" "is" "young" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not young.
("Gary" "is" "young" "-")
If someone is cold then they are not green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "-"))
If someone is kind and not green then they are not red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "-"))
Quiet, cold people are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "-"))
Bob is green.
True
1
proof
[(triple5)]
("Bob" "is" "green" "+")
triple5
Gary is cold.
False
1
inv-proof
[(triple13)]
("Gary" "is" "cold" "+")
triple13
Anne is not red.
True
3
proof
[(((triple2 triple1) -> rule3))]
("Anne" "is" "red" "-")
((triple2 triple1) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Dave is not red.
True
4
proof
[(((triple10 ((triple9) -> rule1)) -> rule2))]
("Dave" "is" "red" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
int2
Dave is red.
False
4
inv-proof
[(((triple10 ((triple9) -> rule1)) -> rule2))]
("Dave" "is" "red" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
int2
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2)] Anne is rough.[(triple3)] Anne is young.[(triple4)] Bob is green.[(triple5)] Bob is kind.[(triple6)] Bob is not red.[(triple7)] Bob is not young.[(triple8)] Dave is cold.[(triple9)] Dave is kind.[(triple10)] Dave is not rough.[(triple11)] Dave is young.[(triple12)] Gary is kind.[(triple14)] Gary is not cold.[(triple13)] Gary is not young.[(triple16)] Gary is quiet.[(triple15)] @1: Anne is not green.[(((triple1) -> rule1))] Anne is not red.[(((triple2 triple1) -> rule3))] Dave is not green.[(((triple9) -> rule1))] @2: Dave is not red.[(((triple10 ((triple9) -> rule1)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is not red.
("Bob" "is" "red" "-")
triple7
Bob is not young.
("Bob" "is" "young" "-")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is not rough.
("Dave" "is" "rough" "-")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is not cold.
("Gary" "is" "cold" "-")
triple13
Gary is not young.
("Gary" "is" "young" "-")
triple16
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Anne is not green.
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is not red.
("Anne" "is" "red" "-")
((triple2 triple1) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple9) -> (rule1 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
int2