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