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