Bob is green. Bob is kind. Bob is white. Bob is young. Charlie is not kind. Charlie is rough. Dave is not green. Dave is kind. Dave is not nice. Dave is young. Erin is green. Erin is nice. Erin is smart. Erin is white. Erin is young. If Bob is green then Bob is rough. If someone is young and green then they are nice. All green people are young. If someone is kind and white then they are young. If someone is smart then they are kind. Young, smart people are kind.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If Bob is green then Bob is rough.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "rough" "+"))
If someone is young and green then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and white then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Young, smart people are kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Bob is young.
True
1
proof
[(triple4 OR ((triple1) -> rule3) OR ((triple2 triple3) -> rule4))]
("Bob" "is" "young" "+")
triple4
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple2 triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is green.
False
1
inv-proof
[(triple7)]
("Dave" "is" "green" "+")
triple7
Bob is nice.
True
3
proof
[(((triple4 triple1) -> rule2) OR ((((triple1) -> rule3) triple1) -> rule2) OR ((((triple2 triple3) -> rule4) triple1) -> rule2))]
("Bob" "is" "nice" "+")
((triple4 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple2 triple3) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple13) -> rule5) OR ((triple15 triple13) -> rule6) OR ((((triple11) -> rule3) triple13) -> rule6))]
("Erin" "is" "kind" "-")
((triple13) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple15 triple13) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple11) -> (rule3 % int2)) triple13) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is white.[(triple3)] Bob is young.[(triple4 OR ((triple1) -> rule3) OR ((triple2 triple3) -> rule4))] Charlie is not kind.[(triple5)] Charlie is rough.[(triple6)] Dave is kind.[(triple8)] Dave is not green.[(triple7)] Dave is not nice.[(triple9)] Dave is young.[(triple10)] Erin is green.[(triple11)] Erin is nice.[(triple12 OR ((triple15 triple11) -> rule2) OR ((((triple11) -> rule3) triple11) -> rule2) OR ((((((triple13) -> rule5) triple14) -> rule4) triple11) -> rule2))] Erin is smart.[(triple13)] Erin is white.[(triple14)] Erin is young.[(triple15 OR ((triple11) -> rule3) OR ((((triple13) -> rule5) triple14) -> rule4))] @1: Bob is nice.[(((triple4 triple1) -> rule2) OR ((((triple1) -> rule3) triple1) -> rule2) OR ((((triple2 triple3) -> rule4) triple1) -> rule2))] Bob is rough.[(((triple1) -> rule1))] Erin is kind.[(((triple13) -> rule5) OR ((triple15 triple13) -> rule6) OR ((((triple11) -> rule3) triple13) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple2 triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is not green.
("Dave" "is" "green" "-")
triple7
Dave is not nice.
("Dave" "is" "nice" "-")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
triple11
Erin is nice.
("Erin" "is" "nice" "+")
triple12
((triple15 triple11) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple13) -> (rule5 % int3)) triple14) -> (rule4 % int2)) triple11) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple13
Erin is white.
("Erin" "is" "white" "+")
triple14
Erin is young.
("Erin" "is" "young" "+")
triple15
((triple11) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple13) -> (rule5 % int2)) triple14) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple4 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple2 triple3) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple13) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple15 triple13) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple11) -> (rule3 % int2)) triple13) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2