Bob is big. Erin is big. Erin is nice. Erin is red. Gary is not cold. Gary is kind. Gary is not quiet. All kind people are nice. Red, kind people are big. Big people are blue. All red people are blue. If someone is cold and not nice then they are red. Nice people are red. If someone is big and not kind then they are red. If someone is blue and not cold then they are red.
Bob is big.
("Bob" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Red, kind people are big.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and not nice then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is big and not kind then they are red.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
If someone is blue and not cold then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "+"))
Gary is not quiet.
True
1
proof
[(triple7)]
("Gary" "is" "quiet" "-")
triple7
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Erin is blue.
True
2
proof
[(((triple2) -> rule3) OR ((triple4) -> rule4) OR ((((triple3) -> rule6)) -> rule4))]
("Erin" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple4) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is not nice.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "nice" "-")
((triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
True
3
proof
[(((((triple6) -> rule1)) -> rule6))]
("Gary" "is" "red" "+")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule6))]
("Gary" "is" "red" "-")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
True
5
proof
[(((((((triple6) -> rule1)) -> rule6) triple6) -> rule2))]
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule6)) -> rule4) OR ((((((((triple6) -> rule1)) -> rule6) triple6) -> rule2)) -> rule3))]
("Gary" "is" "blue" "-")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((((triple6) -> (rule1 % int4))) -> (rule6 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "red" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is big.[(triple1)] Erin is big.[(triple2)] Erin is nice.[(triple3)] Erin is red.[(triple4 OR ((triple3) -> rule6))] Gary is kind.[(triple6)] Gary is not cold.[(triple5)] Gary is not quiet.[(triple7)] @1: Bob is blue.[(((triple1) -> rule3))] Erin is blue.[(((triple2) -> rule3) OR ((triple4) -> rule4) OR ((((triple3) -> rule6)) -> rule4))] Gary is nice.[(((triple6) -> rule1))] @2: Gary is red.[(((((triple6) -> rule1)) -> rule6))] @3: Gary is big.[(((((((triple6) -> rule1)) -> rule6) triple6) -> rule2))] Gary is blue.[(((((((triple6) -> rule1)) -> rule6)) -> rule4) OR ((((((((triple6) -> rule1)) -> rule6) triple6) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple4) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((((triple6) -> (rule1 % int4))) -> (rule6 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4