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