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