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