Anne is furry. Charlie is smart. Dave is green. Furry people are green. All green people are not young. If Charlie is smart then Charlie is blue. All green people are blue. If someone is blue then they are quiet. If someone is green and not furry then they are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All green people are not young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "-"))
If Charlie is smart then Charlie is blue.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "blue" "+"))
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and not furry then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "+"))
Charlie is smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple3)]
("Dave" "is" "green" "-")
triple3
Dave is not young.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "young" "-")
((triple3) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "young" "+")
((triple3) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Charlie" "is" "quiet" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "smart" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is furry.[(triple1)] Charlie is smart.[(triple2)] Dave is green.[(triple3)] @1: Anne is green.[(((triple1) -> rule1))] Charlie is blue.[(((triple2) -> rule3))] Dave is blue.[(((triple3) -> rule4))] Dave is not young.[(((triple3) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule1)) -> rule4))] Anne is not young.[(((((triple1) -> rule1)) -> rule2))] Charlie is quiet.[(((((triple2) -> rule3)) -> rule5))] Dave is quiet.[(((((triple3) -> rule4)) -> rule5))] @3: Anne is quiet.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple3) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not young.
("Anne" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3