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