Anne is nice. Anne is white. Erin is quiet. If something is smart then it is white. All smart, cold things are not quiet. If something is smart then it is quiet. If Anne is nice and Anne is white then Anne is smart. Quiet things are rough. Rough things are smart. If Anne is rough and Anne is not nice then Anne is not cold. If Anne is not quiet then Anne is young.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All smart, cold things are not quiet.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "-"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Anne is nice and Anne is white then Anne is smart.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "smart" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Anne is rough and Anne is not nice then Anne is not cold.
((("Anne" "is" "rough" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "cold" "-"))
If Anne is not quiet then Anne is young.
((("Anne" "is" "quiet" "~")) -> ("Anne" "is" "young" "+"))
Anne is white.
True
1
proof
[(triple2)]
("Anne" "is" "white" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Erin is rough.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "rough" "-")
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Anne is quiet.
True
4
proof
[(((((triple1 triple2) -> rule4)) -> rule3))]
("Anne" "is" "quiet" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6))]
("Erin" "is" "smart" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is white.
True
4
proof
[(((((((triple3) -> rule5)) -> rule6)) -> rule1))]
("Erin" "is" "white" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((((((triple1 triple2) -> rule4)) -> rule3)) -> rule5))]
("Anne" "is" "rough" "-")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Anne is white.[(triple2)] Erin is quiet.[(triple3)] @1: Anne is smart.[(((triple1 triple2) -> rule4))] Erin is rough.[(((triple3) -> rule5))] @2: Anne is quiet.[(((((triple1 triple2) -> rule4)) -> rule3))] Erin is smart.[(((((triple3) -> rule5)) -> rule6))] @3: Anne is rough.[(((((((triple1 triple2) -> rule4)) -> rule3)) -> rule5))] Erin is white.[(((((((triple3) -> rule5)) -> rule6)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3