Erin is quiet. Gary is smart. Harry is white. If something is smart then it is cold. Nice, cold things are smart. Smart, kind things are nice. Smart things are quiet. Smart, quiet things are white. If something is quiet then it is white.
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Nice, cold things are smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Smart, kind things are nice.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Smart, quiet things are white.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Harry is white.
True
1
proof
[(triple3)]
("Harry" "is" "white" "+")
triple3
Erin is not quiet.
False
1
inv-proof
[(triple1)]
("Erin" "is" "quiet" "-")
triple1
Gary is cold.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "quiet" "-")
((triple2) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule5))]
("Gary" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule5))]
("Gary" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "+")
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is quiet.[(triple1)] Gary is smart.[(triple2)] Harry is white.[(triple3)] @1: Erin is white.[(((triple1) -> rule6))] Gary is cold.[(((triple2) -> rule1))] Gary is quiet.[(((triple2) -> rule4))] @2: Gary is white.[(((((triple2) -> rule4)) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule5))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2