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