Anne is quiet. Charlie is red. Gary is red. Harry is nice. All blue people are smart. Red people are blue. Smart people are rough. Quiet, blue people are rough. White, red people are quiet. If Gary is red and Gary is white then Gary is blue.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Quiet, blue people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
White, red people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is red and Gary is white then Gary is blue.
((("Gary" "is" "red" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "blue" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is rough.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Charlie is red.[(triple2)] Gary is red.[(triple3)] Harry is nice.[(triple4)] @1: Charlie is blue.[(((triple2) -> rule2))] Gary is blue.[(((triple3) -> rule2))] @2: Charlie is smart.[(((((triple2) -> rule2)) -> rule1))] Gary is smart.[(((((triple3) -> rule2)) -> rule1))] @3: Charlie is rough.[(((((((triple2) -> rule2)) -> rule1)) -> rule3))] Gary is rough.[(((((((triple3) -> rule2)) -> rule1)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3