Bob is big. Bob is furry. Bob is round. All big, furry things are kind. All blue things are round. Kind, red things are furry. If something is kind and furry then it is blue. Round things are blue. If Bob is furry then Bob is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
All big, furry things are kind.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Kind, red things are furry.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is kind and furry then it is blue.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Bob is furry then Bob is big.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "big" "+"))
Bob is round.
True
1
proof
[(triple3 OR ((((((triple1 triple2) -> rule1) triple2) -> rule4)) -> rule2) OR ((((((((triple2) -> rule6) triple2) -> rule1) triple2) -> rule4)) -> rule2))]
("Bob" "is" "round" "+")
triple3
((((((triple1 triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple2) -> (rule6 % int4)) triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "-")
triple2
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule6))] Bob is furry.[(triple2)] Bob is round.[(triple3 OR ((((((triple1 triple2) -> rule1) triple2) -> rule4)) -> rule2) OR ((((((((triple2) -> rule6) triple2) -> rule1) triple2) -> rule4)) -> rule2))] @1: Bob is blue.[(((triple3) -> rule5) OR ((((triple1 triple2) -> rule1) triple2) -> rule4) OR ((((((triple2) -> rule6) triple2) -> rule1) triple2) -> rule4))] Bob is kind.[(((triple1 triple2) -> rule1) OR ((((triple2) -> rule6) triple2) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((((((triple1 triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple2) -> (rule6 % int4)) triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1 triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2