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