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