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