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