Bob is blue. Bob is green. Bob is kind. Bob is red. Dave is white. Erin is white. Harry is green. If something is red and kind then it is white. White things are young. If Harry is green and Harry is blue then Harry is nice. Green, young things are blue. If Bob is white then Bob is young. If something is young and blue then it is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is red and kind then it is white.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Harry is green and Harry is blue then Harry is nice.
((("Harry" "is" "green" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
Green, young things are blue.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Bob is white then Bob is young.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "young" "+"))
If something is young and blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Dave is white.
True
1
proof
[(triple5)]
("Dave" "is" "white" "+")
triple5
Dave is not white.
False
1
inv-proof
[(triple5)]
("Dave" "is" "white" "-")
triple5
Erin is young.
True
2
proof
[(((triple6) -> rule2))]
("Erin" "is" "young" "+")
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple6) -> rule2))]
("Erin" "is" "young" "-")
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is young.
True
4
proof
[(((((triple4 triple3) -> rule1)) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule5))]
("Bob" "is" "young" "+")
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not young.
False
4
inv-proof
[(((((triple4 triple3) -> rule1)) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule5))]
("Bob" "is" "young" "-")
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
True
6
proof
[(((((((triple4 triple3) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6))]
("Bob" "is" "nice" "+")
((((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not nice.
False
6
inv-proof
[(((((((triple4 triple3) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6))]
("Bob" "is" "nice" "-")
((((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is blue.[(triple1 OR ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4) OR ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4))] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Dave is white.[(triple5)] Erin is white.[(triple6)] Harry is green.[(triple7)] @1: Bob is white.[(((triple4 triple3) -> rule1))] Dave is young.[(((triple5) -> rule2))] Erin is young.[(((triple6) -> rule2))] @2: Bob is young.[(((((triple4 triple3) -> rule1)) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule5))] @3: Bob is nice.[(((((((triple4 triple3) -> rule1)) -> rule2) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) triple1) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule2) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule1)) -> rule5) ((triple2 ((((triple4 triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2 ((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple2 ((((triple4 triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple4 triple3) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((((triple4 triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4