Anne is big. Anne is cold. Anne is furry. Anne is green. Anne is smart. Dave is furry. Dave is green. Erin is cold. Erin is furry. Erin is green. Erin is smart. Erin is white. Harry is cold. Harry is furry. Harry is green. Cold, white things are big. If Harry is white then Harry is smart. Furry things are smart. If Dave is cold and Dave is smart then Dave is big. All green, big things are furry. If something is smart and green then it is young. If something is smart then it is furry. If something is big then it is white.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Cold, white things are big.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Harry is white then Harry is smart.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "smart" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Dave is cold and Dave is smart then Dave is big.
((("Dave" "is" "cold" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "big" "+"))
All green, big things are furry.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is smart and green then it is young.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Anne is smart.
True
1
proof
[(triple5 OR ((triple3) -> rule3) OR ((((triple4 triple1) -> rule5)) -> rule3))]
("Anne" "is" "smart" "+")
triple5
((triple3) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple4 triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Harry is not furry.
False
1
inv-proof
[(triple14)]
("Harry" "is" "furry" "-")
triple14
Erin is young.
True
3
proof
[(((triple11 triple10) -> rule6) OR ((((triple9) -> rule3) triple10) -> rule6) OR ((((((triple10 ((triple8 triple12) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6))]
("Erin" "is" "young" "+")
((triple11 triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9) -> (rule3 % int2)) triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple10 ((triple8 triple12) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Harry is not smart.
False
2
inv-proof
[(((triple14) -> rule3))]
("Harry" "is" "smart" "-")
((triple14) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3 OR ((triple5) -> rule7) OR ((triple4 triple1) -> rule5))] Anne is green.[(triple4)] Anne is smart.[(triple5 OR ((triple3) -> rule3) OR ((((triple4 triple1) -> rule5)) -> rule3))] Dave is furry.[(triple6)] Dave is green.[(triple7)] Erin is cold.[(triple8)] Erin is furry.[(triple9 OR ((triple11) -> rule7) OR ((triple10 ((triple8 triple12) -> rule1)) -> rule5))] Erin is green.[(triple10)] Erin is smart.[(triple11 OR ((triple9) -> rule3) OR ((((triple10 ((triple8 triple12) -> rule1)) -> rule5)) -> rule3))] Erin is white.[(triple12)] Harry is cold.[(triple13)] Harry is furry.[(triple14)] Harry is green.[(triple15)] @1: Anne is white.[(((triple1) -> rule8))] Anne is young.[(((triple5 triple4) -> rule6) OR ((((triple3) -> rule3) triple4) -> rule6) OR ((((((triple4 triple1) -> rule5)) -> rule3) triple4) -> rule6))] Dave is smart.[(((triple6) -> rule3))] Erin is big.[(((triple8 triple12) -> rule1))] Erin is young.[(((triple11 triple10) -> rule6) OR ((((triple9) -> rule3) triple10) -> rule6) OR ((((((triple10 ((triple8 triple12) -> rule1)) -> rule5)) -> rule3) triple10) -> rule6))] Harry is smart.[(((triple14) -> rule3))] @2: Dave is young.[(((((triple6) -> rule3) triple7) -> rule6))] Harry is young.[(((((triple14) -> rule3) triple15) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple5) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple3) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple4 triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is green.
("Dave" "is" "green" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple11) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple10 ((triple8 triple12) -> (rule1 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
((triple9) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple10 ((triple8 triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is green.
("Harry" "is" "green" "+")
triple15
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple5 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple4 triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple8 triple12) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple11 triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9) -> (rule3 % int2)) triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple10 ((triple8 triple12) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
((triple14) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple6) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple14) -> (rule3 % int2)) triple15) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2