Anne is nice. Dave is big. Erin is blue. Gary is nice. All red people are blue. If someone is blue then they are red. All blue, nice people are furry. Red, blue people are rough. If someone is red and not blue then they are not big. If someone is rough then they are big.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All blue, nice people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Red, blue people are rough.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and not blue then they are not big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "big" "-"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Erin is not blue.
False
1
inv-proof
[(triple3)]
("Erin" "is" "blue" "-")
triple3
Erin is red.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "red" "+")
((triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "red" "-")
((triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule4))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule4))]
("Erin" "is" "rough" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
True
5
proof
[(((((((triple3) -> rule2) triple3) -> rule4)) -> rule6))]
("Erin" "is" "big" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not big.
False
5
inv-proof
[(((((((triple3) -> rule2) triple3) -> rule4)) -> rule6))]
("Erin" "is" "big" "-")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "+")
Gary is not rough.
Unknown
inv-rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Dave is big.[(triple2)] Erin is blue.[(triple3)] Gary is nice.[(triple4)] @1: Erin is red.[(((triple3) -> rule2))] @2: Erin is rough.[(((((triple3) -> rule2) triple3) -> rule4))] @3: Erin is big.[(((((((triple3) -> rule2) triple3) -> rule4)) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3