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