Anne is nice. Charlie is not kind. Erin is big. Erin is green. Fiona is not cold. Fiona is nice. Fiona is smart. Green people are cold. If Anne is cold and Anne is not big then Anne is smart. Green people are nice. Big people are nice. Big, kind people are smart. If Charlie is cold then Charlie is white. If Anne is big then Anne is nice. If Erin is big and Erin is cold then Erin is kind.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Anne is cold and Anne is not big then Anne is smart.
((("Anne" "is" "cold" "+") ("Anne" "is" "big" "~")) -> ("Anne" "is" "smart" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Big, kind people are smart.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If Anne is big then Anne is nice.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "nice" "+"))
If Erin is big and Erin is cold then Erin is kind.
((("Erin" "is" "big" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "kind" "+"))
Fiona is nice.
True
1
proof
[(triple6)]
("Fiona" "is" "nice" "+")
triple6
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Erin is nice.
True
2
proof
[(((triple3) -> rule4) OR ((triple4) -> rule3))]
("Erin" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple4) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple4) -> rule3))]
("Erin" "is" "nice" "-")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple4) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
True
4
proof
[(((triple3 ((triple4) -> rule1)) -> rule8))]
("Erin" "is" "kind" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((triple3 ((triple4) -> rule1)) -> rule8))]
("Erin" "is" "kind" "-")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
True
6
proof
[(((triple3 ((triple3 ((triple4) -> rule1)) -> rule8)) -> rule5))]
("Erin" "is" "smart" "+")
((triple3 ((triple3 ((triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((triple3 ((triple3 ((triple4) -> rule1)) -> rule8)) -> rule5))]
("Erin" "is" "smart" "-")
((triple3 ((triple3 ((triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Charlie is not kind.[(triple2)] Erin is big.[(triple3)] Erin is green.[(triple4)] Fiona is nice.[(triple6)] Fiona is not cold.[(triple5)] Fiona is smart.[(triple7)] @1: Erin is cold.[(((triple4) -> rule1))] Erin is nice.[(((triple3) -> rule4) OR ((triple4) -> rule3))] @2: Erin is kind.[(((triple3 ((triple4) -> rule1)) -> rule8))] @3: Erin is smart.[(((triple3 ((triple3 ((triple4) -> rule1)) -> rule8)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple4) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple3 ((triple3 ((triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3