Bob is cold. Bob is furry. Bob is red. Bob is not round. Bob is smart. Bob is young. Erin is big. Erin is furry. Erin is red. Erin is young. Harry is big. Harry is cold. Harry is furry. Harry is red. Harry is round. Harry is smart. If something is red and not round then it is smart. If something is big and not furry then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is red and not round then it is smart.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "smart" "+"))
If something is big and not furry then it is red.
((("something" "is" "big" "+") ("something" "is" "furry" "~")) -> ("something" "is" "red" "+"))
Bob is smart.
True
1
proof
[(triple5 OR ((triple3 triple4) -> rule1))]
("Bob" "is" "smart" "+")
triple5
((triple3 triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
1
inv-proof
[(triple5 OR ((triple3 triple4) -> rule1))]
("Bob" "is" "smart" "-")
triple5
((triple3 triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is not round.[(triple4)] Bob is red.[(triple3)] Bob is smart.[(triple5 OR ((triple3 triple4) -> rule1))] Bob is young.[(triple6)] Erin is big.[(triple7)] Erin is furry.[(triple8)] Erin is red.[(triple9)] Erin is young.[(triple10)] Harry is big.[(triple11)] Harry is cold.[(triple12)] Harry is furry.[(triple13)] Harry is red.[(triple14)] Harry is round.[(triple15)] Harry is smart.[(triple16)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not round.
("Bob" "is" "round" "-")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple3 triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16