Bob is big. Bob is blue. Charlie is blue. Erin is big. Erin is green. Erin is kind. Erin is rough. All kind, green people are big. All rough, blue people are kind. If someone is big then they are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All kind, green people are big.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All rough, blue people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple4 OR ((triple6 triple5) -> rule1))]
("Erin" "is" "big" "-")
triple4
((triple6 triple5) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Charlie is blue.[(triple3)] Erin is big.[(triple4 OR ((triple6 triple5) -> rule1))] Erin is green.[(triple5)] Erin is kind.[(triple6)] Erin is rough.[(triple7 OR ((triple4) -> rule3) OR ((((triple6 triple5) -> rule1)) -> rule3))] @1: Bob is rough.[(((triple1) -> rule3))] @2: Bob is kind.[(((((triple1) -> rule3) triple2) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple6 triple5) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2