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