Bob is kind. Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Dave is furry. Dave is kind. Harry is not furry. Harry is kind. Harry is rough. Harry is not smart. Harry is young. Blue, furry people are young. Rough people are young. If Harry is young and Harry is kind then Harry is not furry. Kind people are rough. If someone is furry and young then they are blue. All rough, blue people are smart. All smart people are green. All smart people are green. If someone is smart and not young then they are green.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is young.
("Harry" "is" "young" "+")
Blue, furry people are young.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Harry is young and Harry is kind then Harry is not furry.
((("Harry" "is" "young" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "furry" "-"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and young then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All rough, blue people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not young then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
Charlie is furry.
True
1
proof
[(triple3)]
("Charlie" "is" "furry" "+")
triple3
Dave is not furry.
False
1
inv-proof
[(triple6)]
("Dave" "is" "furry" "-")
triple6
Bob is rough.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple5) -> rule4))]
("Charlie" "is" "rough" "-")
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is young.
True
3
proof
[(((((triple7) -> rule4)) -> rule2))]
("Dave" "is" "young" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Charlie is not smart.
False
4
inv-proof
[(((((triple5) -> rule4) triple2) -> rule6) OR ((((triple5) -> rule4) ((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule5)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple5) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple5) -> (rule4 % int4)) ((triple3 ((((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Dave is blue.
True
5
proof
[(((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5))]
("Dave" "is" "blue" "+")
((triple6 ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5))]
("Dave" "is" "blue" "-")
((triple6 ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is smart.
True
8
proof
[(((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6))]
("Dave" "is" "smart" "+")
((((triple7) -> (rule4 % int4)) ((triple6 ((((triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is not smart.
False
8
inv-proof
[(((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple7) -> (rule4 % int4)) ((triple6 ((((triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is green.
True
9
proof
[(((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule7) OR ((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule8))]
("Dave" "is" "green" "+")
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Dave is not green.
False
9
inv-proof
[(((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule7) OR ((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule8))]
("Dave" "is" "green" "-")
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "green" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not green.
Unknown
inv-rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is kind.[(triple1)] Charlie is blue.[(triple2 OR ((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule5))] Charlie is furry.[(triple3)] Charlie is green.[(triple4 OR ((((((triple5) -> rule4) triple2) -> rule6)) -> rule7) OR ((((((triple5) -> rule4) triple2) -> rule6)) -> rule8) OR ((((((triple5) -> rule4) ((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule7) OR ((((((triple5) -> rule4) ((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule8))] Charlie is kind.[(triple5)] Dave is furry.[(triple6)] Dave is kind.[(triple7)] Harry is kind.[(triple9)] Harry is not furry.[(triple8 OR ((triple12 triple9) -> rule3) OR ((((triple10) -> rule2) triple9) -> rule3) OR ((((((triple9) -> rule4)) -> rule2) triple9) -> rule3))] Harry is not smart.[(triple11)] Harry is rough.[(triple10 OR ((triple9) -> rule4))] Harry is young.[(triple12 OR ((triple10) -> rule2) OR ((((triple9) -> rule4)) -> rule2))] @1: Bob is rough.[(((triple1) -> rule4))] Charlie is rough.[(((triple5) -> rule4))] Charlie is young.[(((triple2 triple3) -> rule1) OR ((((triple5) -> rule4)) -> rule2))] Dave is rough.[(((triple7) -> rule4))] @2: Bob is young.[(((((triple1) -> rule4)) -> rule2))] Charlie is smart.[(((((triple5) -> rule4) triple2) -> rule6) OR ((((triple5) -> rule4) ((triple3 ((((triple5) -> rule4)) -> rule2)) -> rule5)) -> rule6))] Dave is young.[(((((triple7) -> rule4)) -> rule2))] @3: Dave is blue.[(((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5))] @4: Dave is smart.[(((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6))] @5: Dave is green.[(((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule7) OR ((((((triple7) -> rule4) ((triple6 ((((triple7) -> rule4)) -> rule2)) -> rule5)) -> rule6)) -> rule8))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple3 ((((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((((((triple5) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple5) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple5) -> (rule4 % int5)) ((triple3 ((((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
((((((triple5) -> (rule4 % int5)) ((triple3 ((((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is not furry.
("Harry" "is" "furry" "-")
triple8
((triple12 triple9) -> (rule3 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
((((triple10) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not smart.
("Harry" "is" "smart" "-")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple10
((triple9) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple10) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2 triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple5) -> (rule4 % int4)) ((triple3 ((((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple6 ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((triple7) -> (rule4 % int4)) ((triple6 ((((triple7) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple7) -> (rule4 % int5)) ((triple6 ((((triple7) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5