Erin is smart. Fiona is kind. Gary is round. Big things are not furry. White things are kind. If something is round then it is big. If something is white then it is quiet. All white, quiet things are not smart. If something is kind then it is white. If Gary is round then Gary is quiet. If Gary is not big and Gary is not kind then Gary is smart.
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Big things are not furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is white then it is quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All white, quiet things are not smart.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "-"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Gary is round then Gary is quiet.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "quiet" "+"))
If Gary is not big and Gary is not kind then Gary is smart.
((("Gary" "is" "big" "~") ("Gary" "is" "kind" "~")) -> ("Gary" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Fiona is white.
True
2
proof
[(((triple2) -> rule6))]
("Fiona" "is" "white" "+")
((triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule7))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Fiona" "is" "quiet" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not smart.
True
6
proof
[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule4)) -> rule5))]
("Fiona" "is" "smart" "-")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is smart.
False
6
inv-proof
[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule4)) -> rule5))]
("Fiona" "is" "smart" "+")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Erin is smart.[(triple1)] Fiona is kind.[(triple2)] Gary is round.[(triple3)] @1: Fiona is white.[(((triple2) -> rule6))] Gary is big.[(((triple3) -> rule3))] Gary is quiet.[(((triple3) -> rule7))] @2: Fiona is quiet.[(((((triple2) -> rule6)) -> rule4))] Gary is not furry.[(((((triple3) -> rule3)) -> rule1))] @3: Fiona is not smart.[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule4)) -> rule5))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Fiona is not smart.
("Fiona" "is" "smart" "-")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3