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