Anne is furry. Charlie is not young. Erin is young. All rough people are round. If Erin is young then Erin is blue. If Anne is furry and Anne is blue then Anne is not round. If Erin is round then Erin is not rough. Furry people are big. If Erin is blue then Erin is round.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Erin is young.
("Erin" "is" "young" "+")
All rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If Erin is young then Erin is blue.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "blue" "+"))
If Anne is furry and Anne is blue then Anne is not round.
((("Anne" "is" "furry" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "round" "-"))
If Erin is round then Erin is not rough.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "rough" "-"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If Erin is blue then Erin is round.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "round" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Charlie is young.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "young" "+")
triple2
Erin is blue.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "big" "-")
((triple1) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is round.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("Erin" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("Erin" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "big" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is furry.[(triple1)] Charlie is not young.[(triple2)] Erin is young.[(triple3)] @1: Anne is big.[(((triple1) -> rule5))] Erin is blue.[(((triple3) -> rule2))] @2: Erin is round.[(((((triple3) -> rule2)) -> rule6))] @3: Erin is not rough.[(((((((triple3) -> rule2)) -> rule6)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is not young.
("Charlie" "is" "young" "-")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3