Erin is cold. Erin is nice. Erin is quiet. Gary is cold. Gary is not kind. Gary is nice. Gary is quiet. Gary is not round. Harry is kind. Harry is nice. Harry is red. Harry is not smart. If something is quiet then it is cold. All quiet, nice things are cold. If something is smart then it is not red. If something is nice and not round then it is quiet. If something is round and not smart then it is not nice. If Erin is cold then Erin is nice.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All quiet, nice things are cold.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is smart then it is not red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "-"))
If something is nice and not round then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "quiet" "+"))
If something is round and not smart then it is not nice.
((("something" "is" "round" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "-"))
If Erin is cold then Erin is nice.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "nice" "+"))
Erin is cold.
True
1
proof
[(triple1 OR ((triple3) -> rule1) OR ((triple3 triple2) -> rule2))]
("Erin" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is not quiet.
False
1
inv-proof
[(triple7 OR ((triple6 triple8) -> rule4))]
("Gary" "is" "quiet" "-")
triple7
((triple6 triple8) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Erin is cold.[(triple1 OR ((triple3) -> rule1) OR ((triple3 triple2) -> rule2))] Erin is nice.[(triple2 OR ((triple1) -> rule6) OR ((((triple3) -> rule1)) -> rule6))] Erin is quiet.[(triple3)] Gary is cold.[(triple4 OR ((triple7) -> rule1) OR ((triple7 triple6) -> rule2) OR ((((triple6 triple8) -> rule4)) -> rule1) OR ((((triple6 triple8) -> rule4) triple6) -> rule2))] Gary is nice.[(triple6)] Gary is not kind.[(triple5)] Gary is not round.[(triple8)] Gary is quiet.[(triple7 OR ((triple6 triple8) -> rule4))] Harry is kind.[(triple9)] Harry is nice.[(triple10)] Harry is not smart.[(triple12)] Harry is red.[(triple11)]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
((triple1) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((triple7) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple7 triple6) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple6 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple6 triple8) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not kind.
("Gary" "is" "kind" "-")
triple5
Gary is not round.
("Gary" "is" "round" "-")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
((triple6 triple8) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not smart.
("Harry" "is" "smart" "-")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple11