Anne is furry. Anne is nice. Anne is smart. Charlie is nice. Gary is big. Gary is furry. Harry is big. Harry is furry. Harry is red. Harry is smart. If someone is nice then they are green. All smart people are furry. If Charlie is green then Charlie is furry. If Gary is smart and Gary is big then Gary is rough. If Charlie is big then Charlie is green. All furry, nice people are red. If Anne is smart then Anne is nice. If someone is green then they are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is green then Charlie is furry.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "furry" "+"))
If Gary is smart and Gary is big then Gary is rough.
((("Gary" "is" "smart" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "rough" "+"))
If Charlie is big then Charlie is green.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
All furry, nice people are red.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Anne is smart then Anne is nice.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "nice" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Harry is red.
True
1
proof
[(triple9)]
("Harry" "is" "red" "+")
triple9
Anne is not furry.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule2))]
("Anne" "is" "furry" "-")
triple1
((triple3) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is furry.[(triple1 OR ((triple3) -> rule2))] Anne is nice.[(triple2 OR ((triple3) -> rule7))] Anne is smart.[(triple3)] Charlie is nice.[(triple4)] Gary is big.[(triple5)] Gary is furry.[(triple6)] Harry is big.[(triple7)] Harry is furry.[(triple8 OR ((triple10) -> rule2))] Harry is red.[(triple9)] Harry is smart.[(triple10)] @1: Anne is green.[(((triple2) -> rule1) OR ((((triple3) -> rule7)) -> rule1))] Anne is red.[(((triple1 triple2) -> rule6) OR ((triple1 ((triple3) -> rule7)) -> rule6) OR ((((triple3) -> rule2) triple2) -> rule6) OR ((((triple3) -> rule2) ((triple3) -> rule7)) -> rule6))] Charlie is green.[(((triple4) -> rule1))] @2: Charlie is furry.[(((((triple4) -> rule1)) -> rule3))] @3: Charlie is red.[(((((((triple4) -> rule1)) -> rule3) triple4) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple3) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 ((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple3) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3