Erin is quiet. Fiona is not quiet. If someone is quiet then they are kind. Round people are blue. All kind people are blue. Kind people are blue. If Erin is quiet then Erin is not round. If someone is big then they are quiet. If Fiona is smart and Fiona is big then Fiona is not blue. Blue people are nice.
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Erin is quiet then Erin is not round.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "round" "-"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is smart and Fiona is big then Fiona is not blue.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "blue" "-"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Erin is quiet.
True
1
proof
[(triple1)]
("Erin" "is" "quiet" "+")
triple1
Fiona is quiet.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "quiet" "+")
triple2
Erin is kind.
True
2
proof
[(((triple1) -> rule1))]
("Erin" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "round" "+")
((triple1) -> (rule5 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule4))]
("Erin" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule4))]
("Erin" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule8) OR ((((((triple1) -> rule1)) -> rule4)) -> rule8))]
("Erin" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not nice.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule8) OR ((((((triple1) -> rule1)) -> rule4)) -> rule8))]
("Erin" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Erin is quiet.[(triple1)] Fiona is not quiet.[(triple2)] @1: Erin is kind.[(((triple1) -> rule1))] Erin is not round.[(((triple1) -> rule5))] @2: Erin is blue.[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule4))] @3: Erin is nice.[(((((((triple1) -> rule1)) -> rule3)) -> rule8) OR ((((((triple1) -> rule1)) -> rule4)) -> rule8))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not round.
("Erin" "is" "round" "-")
((triple1) -> (rule5 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3