Anne is big. Bob is big. Bob is kind. Bob is nice. Erin is big. Erin is kind. Erin is red. Fiona is big. Fiona is blue. Fiona is cold. Fiona is green. Fiona is kind. If Bob is big and Bob is blue then Bob is red. If something is red then it is not green. All red things are kind. All kind things are cold. If something is blue then it is cold. Nice things are cold. If something is cold and not red then it is nice. If something is cold then it is nice.
Anne is big.
("Anne" "is" "big" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If Bob is big and Bob is blue then Bob is red.
((("Bob" "is" "big" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
If something is red then it is not green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is cold and not red then it is nice.
((("something" "is" "cold" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Erin is big.
True
1
proof
[(triple5)]
("Erin" "is" "big" "+")
triple5
Erin is not kind.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule3))]
("Erin" "is" "kind" "-")
triple6
((triple7) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is nice.
True
2
proof
[(((triple10) -> rule8) OR ((((triple12) -> rule4)) -> rule8) OR ((((triple9) -> rule5)) -> rule8))]
("Fiona" "is" "nice" "+")
((triple10) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Erin is green.
False
2
inv-proof
[(((triple7) -> rule2))]
("Erin" "is" "green" "+")
((triple7) -> (rule2 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is nice.
True
3
proof
[(((((triple6) -> rule4)) -> rule8) OR ((((((triple7) -> rule3)) -> rule4)) -> rule8))]
("Erin" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not nice.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule8) OR ((((((triple7) -> rule3)) -> rule4)) -> rule8))]
("Erin" "is" "nice" "-")
((((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule3 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not cold.
Unknown
inv-rconc
[@4: Anne is cold.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule4 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Bob is big.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4 OR ((((triple3) -> rule4)) -> rule8))] Erin is big.[(triple5)] Erin is kind.[(triple6 OR ((triple7) -> rule3))] Erin is red.[(triple7)] Fiona is big.[(triple8)] Fiona is blue.[(triple9)] Fiona is cold.[(triple10 OR ((triple12) -> rule4) OR ((triple9) -> rule5))] Fiona is green.[(triple11)] Fiona is kind.[(triple12)] @1: Bob is cold.[(((triple3) -> rule4) OR ((triple4) -> rule6))] Erin is cold.[(((triple6) -> rule4) OR ((((triple7) -> rule3)) -> rule4))] Erin is not green.[(((triple7) -> rule2))] Fiona is nice.[(((triple10) -> rule8) OR ((((triple12) -> rule4)) -> rule8) OR ((((triple9) -> rule5)) -> rule8))] @2: Erin is nice.[(((((triple6) -> rule4)) -> rule8) OR ((((((triple7) -> rule3)) -> rule4)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple7) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
((triple12) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple9) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is kind.
("Fiona" "is" "kind" "+")
triple12
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((triple7) -> (rule2 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple10) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3