Bob is blue. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is round. Bob is young. Charlie is furry. Charlie is kind. Charlie is round. Blue people are young. If someone is round then they are green. Nice, young people are round. If someone is blue then they are nice. If Bob is furry then Bob is nice. Kind people are green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Nice, young people are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Bob is furry then Bob is nice.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Charlie is furry.
True
1
proof
[(triple8)]
("Charlie" "is" "furry" "+")
triple8
Bob is not round.
False
1
inv-proof
[(triple6 OR ((triple5 triple7) -> rule3) OR ((triple5 ((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule4) triple7) -> rule3) OR ((((triple2) -> rule5) triple7) -> rule3) OR ((((triple1) -> rule4) ((triple1) -> rule1)) -> rule3) OR ((((triple2) -> rule5) ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "round" "-")
triple6
((triple5 triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule4 % int2)) triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((triple2) -> (rule5 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Charlie is green.
True
2
proof
[(((triple10) -> rule2) OR ((triple9) -> rule6))]
("Charlie" "is" "green" "+")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple10) -> rule2) OR ((triple9) -> rule6))]
("Charlie" "is" "green" "-")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3 OR ((triple4) -> rule6) OR ((triple6) -> rule2) OR ((((triple5 triple7) -> rule3)) -> rule2) OR ((((triple5 ((triple1) -> rule1)) -> rule3)) -> rule2) OR ((((((triple1) -> rule4) triple7) -> rule3)) -> rule2) OR ((((((triple2) -> rule5) triple7) -> rule3)) -> rule2) OR ((((((triple1) -> rule4) ((triple1) -> rule1)) -> rule3)) -> rule2) OR ((((((triple2) -> rule5) ((triple1) -> rule1)) -> rule3)) -> rule2))] Bob is kind.[(triple4)] Bob is nice.[(triple5 OR ((triple1) -> rule4) OR ((triple2) -> rule5))] Bob is round.[(triple6 OR ((triple5 triple7) -> rule3) OR ((triple5 ((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule4) triple7) -> rule3) OR ((((triple2) -> rule5) triple7) -> rule3) OR ((((triple1) -> rule4) ((triple1) -> rule1)) -> rule3) OR ((((triple2) -> rule5) ((triple1) -> rule1)) -> rule3))] Bob is young.[(triple7 OR ((triple1) -> rule1))] Charlie is furry.[(triple8)] Charlie is kind.[(triple9)] Charlie is round.[(triple10)] @1: Charlie is green.[(((triple10) -> rule2) OR ((triple9) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple5 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple1) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple2) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int4)) ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((((triple2) -> (rule5 % int4)) ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple5 triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule4 % int2)) triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((triple2) -> (rule5 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1