Anne is quiet. Erin is blue. Fiona is big. Blue, smart people are big. Blue people are kind. Blue, nice people are big. All blue, big people are smart. All kind, nice people are smart. If someone is kind then they are nice.
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Blue, smart people are big.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Blue, nice people are big.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All blue, big people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All kind, nice people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Erin is not blue.
False
1
inv-proof
[(triple2)]
("Erin" "is" "blue" "-")
triple2
Erin is kind.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Erin" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("Erin" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule6)) -> rule5) OR ((triple2 ((triple2 ((((triple2) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("Erin" "is" "smart" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((triple2 ((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not big.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule6)) -> rule3) OR ((triple2 ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule6)) -> rule5)) -> rule1))]
("Erin" "is" "big" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "big" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is quiet.[(triple1)] Erin is blue.[(triple2)] Fiona is big.[(triple3)] @1: Erin is kind.[(((triple2) -> rule2))] @2: Erin is nice.[(((((triple2) -> rule2)) -> rule6))] @3: Erin is big.[(((triple2 ((((triple2) -> rule2)) -> rule6)) -> rule3) OR ((triple2 ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule6)) -> rule5)) -> rule1))] Erin is smart.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule6)) -> rule5) OR ((triple2 ((triple2 ((((triple2) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple2 ((triple2 ((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4