Anne is big. Anne is furry. Anne is red. Anne is young. Bob is furry. Bob is kind. Bob is red. Bob is round. Bob is young. Charlie is big. Charlie is not furry. Harry is kind. Harry is not red. Harry is round. Harry is white. Harry is not young. If someone is red then they are kind. If someone is white then they are kind. If Charlie is young and Charlie is furry then Charlie is red. If someone is big then they are red. All young people are red. If Anne is big and Anne is round then Anne is red. If someone is white then they are not furry. If someone is red and not young then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is not young.
("Harry" "is" "young" "-")
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is young and Charlie is furry then Charlie is red.
((("Charlie" "is" "young" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "red" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Anne is big and Anne is round then Anne is red.
((("Anne" "is" "big" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "red" "+"))
If someone is white then they are not furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "-"))
If someone is red and not young then they are big.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "big" "+"))
Anne is red.
True
1
proof
[(triple3 OR ((triple1) -> rule4) OR ((triple4) -> rule5))]
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is not kind.
False
1
inv-proof
[(triple12 OR ((triple15) -> rule2))]
("Harry" "is" "kind" "-")
triple12
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is red.[(triple3 OR ((triple1) -> rule4) OR ((triple4) -> rule5))] Anne is young.[(triple4)] Bob is furry.[(triple5)] Bob is kind.[(triple6 OR ((triple7) -> rule1) OR ((((triple9) -> rule5)) -> rule1))] Bob is red.[(triple7 OR ((triple9) -> rule5))] Bob is round.[(triple8)] Bob is young.[(triple9)] Charlie is big.[(triple10)] Charlie is not furry.[(triple11)] Harry is kind.[(triple12 OR ((triple15) -> rule2))] Harry is not red.[(triple13)] Harry is not young.[(triple16)] Harry is round.[(triple14)] Harry is white.[(triple15)] @1: Anne is kind.[(((triple3) -> rule1) OR ((((triple1) -> rule4)) -> rule1) OR ((((triple4) -> rule5)) -> rule1))] Charlie is red.[(((triple10) -> rule4))] Harry is not furry.[(((triple15) -> rule7))] @2: Charlie is kind.[(((((triple10) -> rule4)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple4) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((triple7) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple7
((triple9) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
Charlie is big.
("Charlie" "is" "big" "+")
triple10
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
triple13
Harry is not young.
("Harry" "is" "young" "-")
triple16
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple10) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is not furry.
("Harry" "is" "furry" "-")
((triple15) -> (rule7 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2