Bob is blue. Bob is nice. Bob is quiet. Bob is round. Charlie is blue. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is round. Erin is blue. Erin is kind. Erin is round. Harry is blue. Harry is green. Harry is kind. All blue people are rough. Round people are blue. Kind people are blue. If someone is round then they are kind. Green people are quiet. All quiet people are blue. If someone is quiet then they are kind. If someone is green then they are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Charlie is rough.
True
1
proof
[(triple9 OR ((triple5) -> rule1) OR ((((triple10) -> rule2)) -> rule1) OR ((((triple6) -> rule8)) -> rule1) OR ((((triple8) -> rule6)) -> rule1) OR ((((((triple10) -> rule4)) -> rule3)) -> rule1) OR ((((((triple6) -> rule5)) -> rule6)) -> rule1) OR ((((((triple8) -> rule7)) -> rule3)) -> rule1) OR ((((((((triple6) -> rule5)) -> rule7)) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "+")
triple9
((triple5) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple8) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is not nice.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "nice" "-")
triple7
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1 OR ((triple3) -> rule6) OR ((triple4) -> rule2) OR ((((triple3) -> rule7)) -> rule3) OR ((((triple4) -> rule4)) -> rule3))] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is round.[(triple4)] Charlie is blue.[(triple5 OR ((triple10) -> rule2) OR ((triple6) -> rule8) OR ((triple8) -> rule6) OR ((((triple10) -> rule4)) -> rule3) OR ((((triple6) -> rule5)) -> rule6) OR ((((triple8) -> rule7)) -> rule3) OR ((((((triple6) -> rule5)) -> rule7)) -> rule3))] Charlie is green.[(triple6)] Charlie is nice.[(triple7)] Charlie is quiet.[(triple8 OR ((triple6) -> rule5))] Charlie is rough.[(triple9 OR ((triple5) -> rule1) OR ((((triple10) -> rule2)) -> rule1) OR ((((triple6) -> rule8)) -> rule1) OR ((((triple8) -> rule6)) -> rule1) OR ((((((triple10) -> rule4)) -> rule3)) -> rule1) OR ((((((triple6) -> rule5)) -> rule6)) -> rule1) OR ((((((triple8) -> rule7)) -> rule3)) -> rule1) OR ((((((((triple6) -> rule5)) -> rule7)) -> rule3)) -> rule1))] Charlie is round.[(triple10)] Erin is blue.[(triple11 OR ((triple12) -> rule3) OR ((triple13) -> rule2) OR ((((triple13) -> rule4)) -> rule3))] Erin is kind.[(triple12 OR ((triple13) -> rule4))] Erin is round.[(triple13)] Harry is blue.[(triple14 OR ((triple15) -> rule8) OR ((triple16) -> rule3) OR ((((triple15) -> rule5)) -> rule6) OR ((((((triple15) -> rule5)) -> rule7)) -> rule3))] Harry is green.[(triple15)] Harry is kind.[(triple16 OR ((((triple15) -> rule5)) -> rule7))] @1: Bob is kind.[(((triple3) -> rule7) OR ((triple4) -> rule4))] Bob is rough.[(((triple1) -> rule1) OR ((((triple3) -> rule6)) -> rule1) OR ((((triple4) -> rule2)) -> rule1) OR ((((((triple3) -> rule7)) -> rule3)) -> rule1) OR ((((((triple4) -> rule4)) -> rule3)) -> rule1))] Charlie is kind.[(((triple10) -> rule4) OR ((triple8) -> rule7) OR ((((triple6) -> rule5)) -> rule7))] Erin is rough.[(((triple11) -> rule1) OR ((((triple12) -> rule3)) -> rule1) OR ((((triple13) -> rule2)) -> rule1) OR ((((((triple13) -> rule4)) -> rule3)) -> rule1))] Harry is quiet.[(((triple15) -> rule5))] Harry is rough.[(((triple14) -> rule1) OR ((((triple15) -> rule8)) -> rule1) OR ((((triple16) -> rule3)) -> rule1) OR ((((((triple15) -> rule5)) -> rule6)) -> rule1) OR ((((((((triple15) -> rule5)) -> rule7)) -> rule3)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple3) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple4) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple10) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple6) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple8) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
((triple6) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
((triple5) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple8) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
((triple12) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple13) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple12
((triple13) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple14
((triple15) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple16) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule5 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple15) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple15
Harry is kind.
("Harry" "is" "kind" "+")
triple16
((((triple15) -> (rule5 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple10) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple8) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple11) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple13) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple15) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple15) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((((triple15) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4