Anne is not nice. Anne is quiet. Anne is red. Anne is round. Erin is kind. Gary is nice. Gary is round. All kind things are rough. Round things are rough. If Erin is not nice then Erin is kind. All rough, round things are red. Big things are not red. All red things are quiet.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Erin is not nice then Erin is kind.
((("Erin" "is" "nice" "~")) -> ("Erin" "is" "kind" "+"))
All rough, round things are red.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Big things are not red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Anne is not nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Gary is not round.
False
1
inv-proof
[(triple7)]
("Gary" "is" "round" "-")
triple7
Erin is rough.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is red.
True
4
proof
[(((((triple7) -> rule2) triple7) -> rule4))]
("Gary" "is" "red" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple7) -> rule2) triple7) -> rule4))]
("Gary" "is" "red" "-")
((((triple7) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
True
5
proof
[(((((((triple7) -> rule2) triple7) -> rule4)) -> rule6))]
("Gary" "is" "quiet" "+")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not quiet.
False
5
inv-proof
[(((((((triple7) -> rule2) triple7) -> rule4)) -> rule6))]
("Gary" "is" "quiet" "-")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "quiet" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is not nice.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule6) OR ((((((triple4) -> rule2) triple4) -> rule4)) -> rule6))] Anne is red.[(triple3 OR ((((triple4) -> rule2) triple4) -> rule4))] Anne is round.[(triple4)] Erin is kind.[(triple5)] Gary is nice.[(triple6)] Gary is round.[(triple7)] @1: Anne is rough.[(((triple4) -> rule2))] Erin is rough.[(((triple5) -> rule1))] Gary is rough.[(((triple7) -> rule2))] @2: Gary is red.[(((((triple7) -> rule2) triple7) -> rule4))] @3: Gary is quiet.[(((((((triple7) -> rule2) triple7) -> rule4)) -> rule6))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((((triple4) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
((((triple4) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple7) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3