Bob is kind. Charlie is round. Erin is young. Harry is quiet. If someone is kind and blue then they are not red. Kind people are blue.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is kind and blue then they are not red.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not red.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "red" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Charlie is round.[(triple2)] Erin is young.[(triple3)] Harry is quiet.[(triple4)] @1: Bob is blue.[(((triple1) -> rule2))] @2: Bob is not red.[(((triple1 ((triple1) -> rule2)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2