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