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