Anne is red. Charlie is smart. Dave is nice. All nice things are red. All smart things are kind. Round things are kind. All nice things are rough. All nice, round things are not rough. If something is smart and not round then it is not quiet. Round, smart things are not nice. All rough, red things are smart.
Anne is red.
("Anne" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All nice, round things are not rough.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "-"))
If something is smart and not round then it is not quiet.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "quiet" "-"))
Round, smart things are not nice.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
All rough, red things are smart.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Dave is rough.
True
2
proof
[(((triple3) -> rule4))]
("Dave" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is smart.
True
5
proof
[(((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8))]
("Dave" "is" "smart" "+")
((((triple3) -> (rule4 % int3)) ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8))]
("Dave" "is" "smart" "-")
((((triple3) -> (rule4 % int3)) ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
True
6
proof
[(((((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8)) -> rule2))]
("Dave" "is" "kind" "+")
((((((triple3) -> (rule4 % int4)) ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is not kind.
False
6
inv-proof
[(((((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8)) -> rule2))]
("Dave" "is" "kind" "-")
((((((triple3) -> (rule4 % int4)) ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is red.[(triple1)] Charlie is smart.[(triple2)] Dave is nice.[(triple3)] @1: Charlie is kind.[(((triple2) -> rule2))] Dave is red.[(((triple3) -> rule1))] Dave is rough.[(((triple3) -> rule4))] @2: Dave is smart.[(((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8))] @3: Dave is kind.[(((((((triple3) -> rule4) ((triple3) -> rule1)) -> rule8)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3) -> (rule4 % int3)) ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple3) -> (rule4 % int4)) ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4