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