Bob is big. Bob is kind. Bob is quiet. Bob is red. Bob is white. Charlie is big. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is white. Erin is nice. Erin is white. If Bob is young and Bob is big then Bob is nice. All kind things are red. Kind, red things are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
If Bob is young and Bob is big then Bob is nice.
((("Bob" "is" "young" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "nice" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Kind, red things are quiet.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Erin is white.
True
1
proof
[(triple12)]
("Erin" "is" "white" "+")
triple12
Bob is not red.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule2))]
("Bob" "is" "red" "-")
triple4
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is quiet.[(triple3 OR ((triple2 triple4) -> rule3) OR ((triple2 ((triple2) -> rule2)) -> rule3))] Bob is red.[(triple4 OR ((triple2) -> rule2))] Bob is white.[(triple5)] Charlie is big.[(triple6)] Charlie is nice.[(triple7)] Charlie is quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is white.[(triple10)] Erin is nice.[(triple11)] Erin is white.[(triple12)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple2 triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12