Anne is big. Anne is blue. Anne is furry. Anne is green. Anne is red. Bob is blue. Bob is cold. Bob is green. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is red. Harry is smart. If someone is green and blue then they are cold. Red, furry people are smart. Green, furry people are big. Green, smart people are furry. If someone is smart then they are furry. If someone is red then they are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is green and blue then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Red, furry people are smart.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Green, furry people are big.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Green, smart people are furry.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple8)]
("Bob" "is" "green" "+")
triple8
Harry is not cold.
False
1
inv-proof
[(triple11 OR ((triple13 triple10) -> rule1) OR ((((triple14) -> rule6) triple10) -> rule1))]
("Harry" "is" "cold" "-")
triple11
((triple13 triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple14) -> (rule6 % int2)) triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Anne is smart.
True
3
proof
[(((triple5 triple3) -> rule2))]
("Anne" "is" "smart" "+")
((triple5 triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not cold.
False
3
inv-proof
[(((triple4 triple2) -> rule1) OR ((((triple5) -> rule6) triple2) -> rule1))]
("Anne" "is" "cold" "-")
((triple4 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is big.
Unknown
rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is big.[(triple1 OR ((triple4 triple3) -> rule3) OR ((((triple5) -> rule6) triple3) -> rule3))] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is green.[(triple4 OR ((triple5) -> rule6))] Anne is red.[(triple5)] Bob is blue.[(triple6)] Bob is cold.[(triple7 OR ((triple8 triple6) -> rule1))] Bob is green.[(triple8)] Harry is big.[(triple9 OR ((triple13 triple12) -> rule3) OR ((triple13 ((triple15) -> rule5)) -> rule3) OR ((triple13 ((triple13 triple15) -> rule4)) -> rule3) OR ((((triple14) -> rule6) triple12) -> rule3) OR ((((triple14) -> rule6) ((triple15) -> rule5)) -> rule3) OR ((((triple14) -> rule6) ((triple13 triple15) -> rule4)) -> rule3) OR ((triple13 ((((triple14) -> rule6) triple15) -> rule4)) -> rule3) OR ((((triple14) -> rule6) ((((triple14) -> rule6) triple15) -> rule4)) -> rule3))] Harry is blue.[(triple10)] Harry is cold.[(triple11 OR ((triple13 triple10) -> rule1) OR ((((triple14) -> rule6) triple10) -> rule1))] Harry is furry.[(triple12 OR ((triple15) -> rule5) OR ((triple13 triple15) -> rule4) OR ((((triple14) -> rule6) triple15) -> rule4))] Harry is green.[(triple13 OR ((triple14) -> rule6))] Harry is red.[(triple14)] Harry is smart.[(triple15 OR ((triple14 triple12) -> rule2))] @1: Anne is cold.[(((triple4 triple2) -> rule1) OR ((((triple5) -> rule6) triple2) -> rule1))] Anne is smart.[(((triple5 triple3) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4 triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple5) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple5) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
((triple8 triple6) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
((triple13 triple12) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 ((triple15) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple13 ((triple13 triple15) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple14) -> (rule6 % int2)) triple12) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple14) -> (rule6 % int3)) ((triple15) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple14) -> (rule6 % int3)) ((triple13 triple15) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple13 ((((triple14) -> (rule6 % int3)) triple15) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple14) -> (rule6 % int3)) ((((triple14) -> (rule6 % int3)) triple15) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple13 triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple14) -> (rule6 % int2)) triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple15) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple13 triple15) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple14) -> (rule6 % int2)) triple15) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple14) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple14 triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple5 triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1