Charlie is blue. Charlie is cold. Charlie is furry. Charlie is red. Charlie is not smart. Harry is furry. Harry is smart. If something is red and white then it is cold. Smart, white things are cold. If Harry is red and Harry is white then Harry is not blue. If Charlie is smart then Charlie is red. All smart things are white. If something is cold and not quiet then it is red. If Charlie is white then Charlie is not furry. If something is blue and not quiet then it is furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is red and white then it is cold.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Smart, white things are cold.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Harry is red and Harry is white then Harry is not blue.
((("Harry" "is" "red" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "blue" "-"))
If Charlie is smart then Charlie is red.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "red" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is cold and not quiet then it is red.
((("something" "is" "cold" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
If Charlie is white then Charlie is not furry.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "furry" "-"))
If something is blue and not quiet then it is furry.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "furry" "+"))
Charlie is not smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "-")
triple5
Harry is not furry.
False
1
inv-proof
[(triple6)]
("Harry" "is" "furry" "-")
triple6
Harry is white.
True
2
proof
[(((triple7) -> rule5))]
("Harry" "is" "white" "+")
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple7) -> rule5))]
("Harry" "is" "white" "-")
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
True
4
proof
[(((triple7 ((triple7) -> rule5)) -> rule2))]
("Harry" "is" "cold" "+")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((triple7 ((triple7) -> rule5)) -> rule2))]
("Harry" "is" "cold" "-")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3)] Charlie is not smart.[(triple5)] Charlie is red.[(triple4)] Harry is furry.[(triple6)] Harry is smart.[(triple7)] @1: Harry is white.[(((triple7) -> rule5))] @2: Harry is cold.[(((triple7 ((triple7) -> rule5)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2