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