Bob is big. Bob is furry. Bob is red. Charlie is quiet. Erin is blue. Erin is furry. Erin is red. Blue people are kind. If someone is blue and not kind then they are red.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and not kind then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
Erin is blue.
True
1
proof
[(triple5)]
("Erin" "is" "blue" "+")
triple5
Erin is not blue.
False
1
inv-proof
[(triple5)]
("Erin" "is" "blue" "-")
triple5
Erin is kind.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is red.[(triple3)] Charlie is quiet.[(triple4)] Erin is blue.[(triple5)] Erin is furry.[(triple6)] Erin is red.[(triple7)] @1: Erin is kind.[(((triple5) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1