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