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