Bob is big. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is white. Bob is young. Dave is big. Dave is kind. Dave is nice. Dave is red. Dave is young. Fiona is nice. Harry is kind. Harry is white. Harry is young. If someone is nice then they are big. If Dave is green and Dave is red then Dave is nice. If someone is big then they are white. Big, white people are red. All young people are green. Green, white people are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Dave is green and Dave is red then Dave is nice.
((("Dave" "is" "green" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Big, white people are red.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Green, white people are kind.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple3 OR ((triple2 triple6) -> rule6) OR ((triple2 ((triple1) -> rule3)) -> rule6) OR ((((triple7) -> rule5) triple6) -> rule6) OR ((((triple7) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((triple2 ((((triple4) -> rule1)) -> rule3)) -> rule6) OR ((((triple7) -> rule5) ((((triple4) -> rule1)) -> rule3)) -> rule6))]
("Bob" "is" "kind" "+")
triple3
((triple2 triple6) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple7) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple2 ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple7) -> (rule5 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Dave is not nice.
False
1
inv-proof
[(triple10 OR ((((triple12) -> rule5) triple11) -> rule2) OR ((((triple12) -> rule5) ((triple8 ((triple8) -> rule3)) -> rule4)) -> rule2))]
("Dave" "is" "nice" "-")
triple10
((((triple12) -> (rule5 % int2)) triple11) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple12) -> (rule5 % int4)) ((triple8 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is green.
True
2
proof
[(((triple12) -> rule5))]
("Dave" "is" "green" "+")
((triple12) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple12) -> rule5))]
("Dave" "is" "green" "-")
((triple12) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is white.
True
3
proof
[(((((triple13) -> rule1)) -> rule3))]
("Fiona" "is" "white" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not white.
False
3
inv-proof
[(((((triple13) -> rule1)) -> rule3))]
("Fiona" "is" "white" "-")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is big.[(triple1 OR ((triple4) -> rule1))] Bob is green.[(triple2 OR ((triple7) -> rule5))] Bob is kind.[(triple3 OR ((triple2 triple6) -> rule6) OR ((triple2 ((triple1) -> rule3)) -> rule6) OR ((((triple7) -> rule5) triple6) -> rule6) OR ((((triple7) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((triple2 ((((triple4) -> rule1)) -> rule3)) -> rule6) OR ((((triple7) -> rule5) ((((triple4) -> rule1)) -> rule3)) -> rule6))] Bob is nice.[(triple4)] Bob is red.[(triple5 OR ((triple1 triple6) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule4) OR ((((triple4) -> rule1) triple6) -> rule4) OR ((((triple4) -> rule1) ((triple1) -> rule3)) -> rule4) OR ((triple1 ((((triple4) -> rule1)) -> rule3)) -> rule4) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule4))] Bob is white.[(triple6 OR ((triple1) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Bob is young.[(triple7)] Dave is big.[(triple8 OR ((triple10) -> rule1) OR ((((((triple12) -> rule5) triple11) -> rule2)) -> rule1))] Dave is kind.[(triple9 OR ((((triple12) -> rule5) ((triple8) -> rule3)) -> rule6) OR ((((triple12) -> rule5) ((((triple10) -> rule1)) -> rule3)) -> rule6) OR ((((triple12) -> rule5) ((((((((triple12) -> rule5) triple11) -> rule2)) -> rule1)) -> rule3)) -> rule6))] Dave is nice.[(triple10 OR ((((triple12) -> rule5) triple11) -> rule2) OR ((((triple12) -> rule5) ((triple8 ((triple8) -> rule3)) -> rule4)) -> rule2))] Dave is red.[(triple11 OR ((triple8 ((triple8) -> rule3)) -> rule4) OR ((((triple10) -> rule1) ((triple8) -> rule3)) -> rule4) OR ((triple8 ((((triple10) -> rule1)) -> rule3)) -> rule4) OR ((((triple10) -> rule1) ((((triple10) -> rule1)) -> rule3)) -> rule4))] Dave is young.[(triple12)] Fiona is nice.[(triple13)] Harry is kind.[(triple14 OR ((((triple16) -> rule5) triple15) -> rule6))] Harry is white.[(triple15)] Harry is young.[(triple16)] @1: Dave is green.[(((triple12) -> rule5))] Dave is white.[(((triple8) -> rule3) OR ((((triple10) -> rule1)) -> rule3) OR ((((((((triple12) -> rule5) triple11) -> rule2)) -> rule1)) -> rule3))] Fiona is big.[(((triple13) -> rule1))] Harry is green.[(((triple16) -> rule5))] @2: Fiona is white.[(((((triple13) -> rule1)) -> rule3))] @3: Fiona is red.[(((((triple13) -> rule1) ((((triple13) -> rule1)) -> rule3)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple7) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2 triple6) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple7) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple2 ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple7) -> (rule5 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple1 triple6) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple1 ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple10) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple12) -> (rule5 % int3)) triple11) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple9
((((triple12) -> (rule5 % int3)) ((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple12) -> (rule5 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
((((triple12) -> (rule5 % int5)) ((((((((triple12) -> (rule5 % int5)) triple11) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((((triple12) -> (rule5 % int2)) triple11) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple12) -> (rule5 % int4)) ((triple8 ((triple8) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple11
((triple8 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple8 ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((triple10) -> (rule1 % int3)) ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple12
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((((triple16) -> (rule5 % int2)) triple15) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Dave is green.
("Dave" "is" "green" "+")
((triple12) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((((triple12) -> (rule5 % int4)) triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((triple13) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple16) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple13) -> (rule1 % int3)) ((((triple13) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3