Bob is green. Bob is quiet. Bob is not smart. Charlie is nice. Erin is cold. Erin is not kind. Harry is not smart. If something is cold and not quiet then it is green. If something is green and red then it is not kind. If Harry is red and Harry is kind then Harry is green. If Harry is not smart then Harry is nice. If something is quiet then it is red. If something is quiet and not red then it is nice.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Harry is not smart.
("Harry" "is" "smart" "-")
If something is cold and not quiet then it is green.
((("something" "is" "cold" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "+"))
If something is green and red then it is not kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
If Harry is red and Harry is kind then Harry is green.
((("Harry" "is" "red" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "green" "+"))
If Harry is not smart then Harry is nice.
((("Harry" "is" "smart" "~")) -> ("Harry" "is" "nice" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is quiet and not red then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
Erin is not kind.
True
1
proof
[(triple6)]
("Erin" "is" "kind" "-")
triple6
Harry is smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Harry is nice.
True
2
proof
[(((triple7) -> rule4))]
("Harry" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "red" "-")
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not kind.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule2))]
("Bob" "is" "kind" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
False
4
inv-proof
[(((triple1 ((triple2) -> rule5)) -> rule2))]
("Bob" "is" "kind" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is green.[(triple1)] Bob is not smart.[(triple3)] Bob is quiet.[(triple2)] Charlie is nice.[(triple4)] Erin is cold.[(triple5)] Erin is not kind.[(triple6)] Harry is not smart.[(triple7)] @1: Bob is red.[(((triple2) -> rule5))] Harry is nice.[(((triple7) -> rule4))] @2: Bob is not kind.[(((triple1 ((triple2) -> rule5)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is not kind.
("Erin" "is" "kind" "-")
triple6
Harry is not smart.
("Harry" "is" "smart" "-")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not kind.
("Bob" "is" "kind" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2