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