Anne is nice. Anne is quiet. Anne is rough. Anne is round. Anne is smart. Anne is white. Erin is nice. Erin is quiet. Erin is round. Fiona is big. Fiona is nice. Fiona is rough. Fiona is round. Fiona is white. Gary is white. If someone is big and not quiet then they are not nice. If someone is smart and not quiet then they are nice. Smart people are rough. If Gary is quiet and Gary is not white then Gary is round. Round people are big. If someone is big then they are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is big and not quiet then they are not nice.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "nice" "-"))
If someone is smart and not quiet then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "nice" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Gary is quiet and Gary is not white then Gary is round.
((("Gary" "is" "quiet" "+") ("Gary" "is" "white" "~")) -> ("Gary" "is" "round" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Erin is round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "+")
triple9
Anne is not smart.
False
1
inv-proof
[(triple5 OR ((((triple4) -> rule5)) -> rule6))]
("Anne" "is" "smart" "-")
triple5
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is smart.
True
2
proof
[(((triple10) -> rule6) OR ((((triple13) -> rule5)) -> rule6))]
("Fiona" "is" "smart" "+")
((triple10) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple13) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is not big.
False
2
inv-proof
[(((triple4) -> rule5))]
("Anne" "is" "big" "-")
((triple4) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is smart.
True
3
proof
[(((((triple9) -> rule5)) -> rule6))]
("Erin" "is" "smart" "+")
((((triple9) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule6))]
("Erin" "is" "smart" "-")
((((triple9) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
True
4
proof
[(((((((triple9) -> rule5)) -> rule6)) -> rule3))]
("Erin" "is" "rough" "+")
((((((triple9) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not rough.
False
4
inv-proof
[(((((((triple9) -> rule5)) -> rule6)) -> rule3))]
("Erin" "is" "rough" "-")
((((((triple9) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not rough.
Unknown
inv-rconc
[@4: Gary is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- rule4 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is big.
Unknown
rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Anne is rough.[(triple3 OR ((triple5) -> rule3) OR ((((((triple4) -> rule5)) -> rule6)) -> rule3))] Anne is round.[(triple4)] Anne is smart.[(triple5 OR ((((triple4) -> rule5)) -> rule6))] Anne is white.[(triple6)] Erin is nice.[(triple7)] Erin is quiet.[(triple8)] Erin is round.[(triple9)] Fiona is big.[(triple10 OR ((triple13) -> rule5))] Fiona is nice.[(triple11)] Fiona is rough.[(triple12 OR ((((triple10) -> rule6)) -> rule3) OR ((((((triple13) -> rule5)) -> rule6)) -> rule3))] Fiona is round.[(triple13)] Fiona is white.[(triple14)] Gary is white.[(triple15)] @1: Anne is big.[(((triple4) -> rule5))] Erin is big.[(((triple9) -> rule5))] Fiona is smart.[(((triple10) -> rule6) OR ((((triple13) -> rule5)) -> rule6))] @2: Erin is smart.[(((((triple9) -> rule5)) -> rule6))] @3: Erin is rough.[(((((((triple9) -> rule5)) -> rule6)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple5) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
((triple13) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple13) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
triple13
Fiona is white.
("Fiona" "is" "white" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Anne is big.
("Anne" "is" "big" "+")
((triple4) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple9) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple10) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple13) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple9) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple9) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3