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