Anne is blue. Charlie is blue. Dave is furry. Fiona is furry. All kind, rough people are not big. Rough people are big. All kind, red people are blue. Rough people are not quiet. Big people are rough. All furry people are red. If someone is furry and red then they are kind. If Dave is quiet and Dave is red then Dave is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All kind, rough people are not big.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "-"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All kind, red people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Rough people are not quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and red then they are kind.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Dave is quiet and Dave is red then Dave is furry.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Dave is red.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "red" "+")
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "red" "-")
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is kind.
True
4
proof
[(((triple4 ((triple4) -> rule6)) -> rule7))]
("Fiona" "is" "kind" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule6)) -> rule7))]
("Dave" "is" "kind" "-")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is blue.
True
7
proof
[(((((triple4 ((triple4) -> rule6)) -> rule7) ((triple4) -> rule6)) -> rule3))]
("Fiona" "is" "blue" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Dave is not blue.
False
7
inv-proof
[(((((triple3 ((triple3) -> rule6)) -> rule7) ((triple3) -> rule6)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule7 % int2)) ((triple3) -> (rule6 % int3))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "kind" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Charlie is blue.[(triple2)] Dave is furry.[(triple3)] Fiona is furry.[(triple4)] @1: Dave is red.[(((triple3) -> rule6))] Fiona is red.[(((triple4) -> rule6))] @2: Dave is kind.[(((triple3 ((triple3) -> rule6)) -> rule7))] Fiona is kind.[(((triple4 ((triple4) -> rule6)) -> rule7))] @3: Dave is blue.[(((((triple3 ((triple3) -> rule6)) -> rule7) ((triple3) -> rule6)) -> rule3))] Fiona is blue.[(((((triple4 ((triple4) -> rule6)) -> rule7) ((triple4) -> rule6)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple4) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule7 % int2)) ((triple3) -> (rule6 % int3))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3