Anne is cold. Anne is furry. Bob is furry. Bob is nice. Bob is quiet. Bob is rough. Bob is white. Charlie is nice. Charlie is smart. Harry is rough. Smart things are nice. If Anne is white and Anne is nice then Anne is smart. Smart, white things are quiet. Smart things are white. If something is nice and rough then it is white. If Harry is cold and Harry is furry then Harry is nice. All rough, smart things are cold. Furry, white things are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Anne is white and Anne is nice then Anne is smart.
((("Anne" "is" "white" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "smart" "+"))
Smart, white things are quiet.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is nice and rough then it is white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Harry is cold and Harry is furry then Harry is nice.
((("Harry" "is" "cold" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "nice" "+"))
All rough, smart things are cold.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Furry, white things are cold.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule1))]
("Charlie" "is" "nice" "-")
triple8
((triple9) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Bob is furry.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5)] Bob is rough.[(triple6)] Bob is white.[(triple7 OR ((triple4 triple6) -> rule5))] Charlie is nice.[(triple8 OR ((triple9) -> rule1))] Charlie is smart.[(triple9)] Harry is rough.[(triple10)] @1: Bob is cold.[(((triple3 triple7) -> rule8) OR ((triple3 ((triple4 triple6) -> rule5)) -> rule8))] Charlie is white.[(((triple9) -> rule4))] @2: Charlie is quiet.[(((triple9 ((triple9) -> rule4)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple4 triple6) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
((triple9) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple3 triple7) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 ((triple4 triple6) -> (rule5 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple9) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple9 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2